This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| count-def | ⊦ cnt(a, σ) = # filter(λ b. b = a, σ) | An Axiom |
| filter-base | ⊦ filter(p, []) = [] | An Axiom |
| filter-rec | ⊦ filter(p, ⌜a '⌝ + ⌜x⌝ ) = (p(a) ⊃ ⌜a '⌝ ;[]) + filter(p, ⌜x⌝ ) | An Axiom |
| filter-inf | ⊦ filter(p, ⌜nf⌝ ) = lim(λ n. filter(p, ⌜nf to n⌝ )) | An Axiom |
| prefix-def | ⊦ σ ⊑ σ0 ↔ (∃ σ1. σ + σ1 = σ0) | An Axiom |
| mon-def | ⊦ mon(σf) ↔ (∀ n. σf(n) ⊑ σf(n + 1)) | An Axiom |
| lim-def | ⊦ mon(σf) → (∀ n. σf(n) ⊑ lim(σf)) ∧ (∀ m. ¬ # lim(σf) < ⌜m⌝ → (∃ n. lim(σf) to m ⊑ σf(n))) | An Axiom |
| lastoc-inf | ⊦ lastoc(a, σ) ≠ ∞ ↔ (∃ n. ⌜n⌝ < # σ ∧ σ[n] = a ∧ (∀ n0. n < n0 ∧ ⌜n0⌝ < # σ → σ[n0] ≠ a)) | An Axiom |
| lastoc-fin | ⊦ lastoc(a, σ) = ⌜n⌝ ↔ ⌜n⌝ < # σ ∧ σ[n] = a ∧ (∀ n0. n < n0 ∧ ⌜n0⌝ < # σ → σ[n0] ≠ a) | An Axiom |
| rem-inf | ⊦ rem(⌜nf⌝ , np) = lim(λ n. rem(⌜nf to n⌝ , np)) | An Axiom |
| rem-rec | ⊦ rem(⌜x⌝ + ⌜a '⌝ , np) = rem(⌜x⌝ , np) + (np(# x) ⊃ [];⌜a '⌝ ) | An Axiom |
| rem-base | ⊦ rem([], np) = [] | An Axiom |
| cnt-appendfromto | ⊦ ¬ # σ < ⌜n⌝ → cnt(a, σ) = cnt(a, σ to n) + cnt(a, σ from n) | A User Theorem |
| cnt-inf | ⊦ cnt(a, σ) = ∞ ↔ # σ = ∞ ∧ (∀ m. ∃ n. m < n ∧ σ[n] = a) | A User Theorem |
| cnt-is-succ | ⊦ cnt(a, σ) = ⌜n⌝ + ⌜1⌝ ↔ (∃ m. ⌜m⌝ < # σ ∧ cnt(a, σ to m + 1) = ⌜n⌝ + ⌜1⌝ ∧ σ[m] = a ∧ (∀ m0. m < m0 ∧ ⌜m0⌝ < # σ → σ[m0] ≠ a)) | A User Theorem |
| cnt-is-zero | ⊦ cnt(a, σ) = ⌜0⌝ ↔ (∀ n. ⌜n⌝ < # σ → σ[n] ≠ a) | A User Theorem |
| cnt-leq | ⊦ ¬ # σ < cnt(a, σ) | A User Theorem |
| cnt-one | ⊦ cnt(a, ⌜b '⌝ ) = ⌜(a = b ⊃ 1;0)⌝ | A User Theorem |
| cnt-rec-end | ⊦ cnt(a, σ + ⌜b '⌝ ) = ⌜(a = b ∧ # σ ≠ ∞ ⊃ 1;0)⌝ + cnt(a, σ) | A User Theorem |
| cnt-rec-gen | ⊦ cnt(a, ⌜b '⌝ + σ) = ⌜(a = b ⊃ 1;0)⌝ + cnt(a, σ) | A User Theorem |
| cnt-zero | ⊦ cnt(a, []) = ⌜0⌝ | A User Theorem |
| cntfin-append | ⊦ cnt(a, ⌜x⌝ + σ) = cnt(a, ⌜x⌝ ) + cnt(a, σ) | A User Theorem |
| cntfin-eqlen | ⊦ # σ ≠ ∞ → (cnt(a, σ) = # σ ↔ (∀ n. ⌜n⌝ < # σ → σ[n] = a)) | A User Theorem |
| cntfin-notinf | ⊦ cnt(a, ⌜x⌝ ) ≠ ∞ | A User Theorem |
| cntfin-rec-end | ⊦ cnt(a, ⌜x⌝ + ⌜b '⌝ ) = ⌜(a = b ⊃ 1;0)⌝ + cnt(a, ⌜x⌝ ) | A User Theorem |
| cntinf-fin-succ | ⊦ cnt(a, ⌜nf⌝ ) = ⌜n⌝ + ⌜1⌝ ↔ (∃ m. cnt(a, ⌜nf to m + 1⌝ ) = ⌜n⌝ + ⌜1⌝ ∧ nf(m) = a ∧ (∀ m0. m < m0 → nf(m0) ≠ a)) | A User Theorem |
| cntinf-fin-weak | ⊦ cnt(a, ⌜nf⌝ ) = ⌜n⌝ ↔ (∃ m. cnt(a, ⌜nf to m⌝ ) = ⌜n⌝ ∧ (∀ m0. m ≤ m0 → nf(m0) ≠ a)) | A User Theorem |
| cntinf-fin-zero | ⊦ cnt(a, ⌜nf⌝ ) = ⌜0⌝ ↔ (∀ m. nf(m) ≠ a) | A User Theorem |
| cntinf-infmany | ⊦ cnt(a, σ) = ∞ ↔ # σ = ∞ ∧ (∀ n. ∃ m. n < m ∧ σ[m] = a) | A User Theorem |
| cntinf-lastocinf | ⊦ cnt(a, σ) = ∞ → lastoc(a, σ) = ∞ | A User Theorem |
| cntinf-tocntsurj | ⊦ cnt(a, σ) = ∞ ↔ # σ = ∞ ∧ (∀ n. ∃ m. cnt(a, σ to m) = ⌜n⌝ ) | A User Theorem |
| cntnotinf-lastocinf | ⊦ cnt(a, σ) ≠ ∞ → (lastoc(a, σ) = ∞ ↔ (∀ n. ⌜n⌝ < # σ → σ[n] ≠ a)) | A User Theorem |
| cntrem-is-inf | ⊦ cnt(a, rem(σ, np)) = ∞ ↔ # σ = ∞ ∧ (∀ m. ∃ n. m ≤ n ∧ ¬ np(n) ∧ σ[n] = a) | A User Theorem |
| cntto-notinf | ⊦ cnt(a, σ to n) ≠ ∞ | A User Theorem |
| filter-appendfromto | ⊦ ¬ # σ < ⌜n⌝ → filter(p, σ) = filter(p, σ to n) + filter(p, σ from n) | A User Theorem |
| filter-evconst | ⊦ (∀ n. m ≤ n → ¬ p(nf(n))) → filter(p, ⌜nf⌝ ) = filter(p, ⌜nf to m⌝ ) | A User Theorem |
| filter-inf-finsize | ⊦ # filter(p, ⌜nf⌝ ) = ⌜n⌝ ↔ (∃ m. (∀ n. m ≤ n → ¬ p(nf(n))) ∧ # filter(p, ⌜nf to m⌝ ) = ⌜n⌝ ) | A User Theorem |
| filter-inf-finsize-strong | ⊦ # filter(p, ⌜nf⌝ ) = ⌜n⌝ ↔ (∃ m. (∀ n. m ≤ n → ¬ p(nf(n))) ∧ # filter(p, ⌜nf to m⌝ ) = ⌜n⌝ ∧ filter(p, ⌜nf⌝ ) = filter(p, ⌜nf to m⌝ )) | A User Theorem |
| filter-infsize | ⊦ # filter(p, σ) = ∞ ↔ # σ = ∞ ∧ (∀ m. ∃ n. m ≤ n ∧ p(σ[n])) | A User Theorem |
| filter-lb | ⊦ ⌜n⌝ < # σ → filter(p, σ to n) ⊑ filter(p, σ) | A User Theorem |
| filter-one | ⊦ filter(p, ⌜a '⌝ ) = (p(a) ⊃ ⌜a '⌝ ;[]) | A User Theorem |
| filter-rec-expand | ⊦ filter(p, σ) = (σ = [] ⊃ [];(p(hd(σ)) ⊃ ⌜hd(σ) '⌝ ;[]) + filter(p, tl(σ))) | A User Theorem |
| filter-rec-gen | ⊦ filter(p, ⌜a '⌝ + σ) = (p(a) ⊃ ⌜a '⌝ ;[]) + filter(p, σ) | A User Theorem |
| filter-ub | ⊦ ⌜n⌝ < # filter(p, σ) → (∃ m. ⌜m⌝ < # σ ∧ filter(p, σ) to n ⊑ filter(p, σ to m)) | A User Theorem |
| filterfin-append | ⊦ filter(p, ⌜x⌝ + σ) = filter(p, ⌜x⌝ ) + filter(p, σ) | A User Theorem |
| filterfin-rec-end | ⊦ filter(p, ⌜x⌝ + ⌜a '⌝ ) = filter(p, ⌜x⌝ ) + (p(a) ⊃ ⌜a '⌝ ;[]) | A User Theorem |
| finfilter-notinf | ⊦ # filter(p, ⌜x⌝ ) ≠ ∞ | A User Theorem |
| getfilter-sat-p | ⊦ ⌜n⌝ < # filter(p, σ) → p(filter(p, σ)[n]) | A User Theorem |
| lastoc-empty | ⊦ lastoc(a, []) = ∞ | A User Theorem |
| lastoc-finrec-end | ⊦ lastoc(a, ⌜x⌝ + ⌜b '⌝ ) = (a = b ⊃ ⌜# x⌝ ;lastoc(a, ⌜x⌝ )) | A User Theorem |
| lastoc-finrec-end-expand | ⊦ lastoc(a, ⌜x⌝ ) = (⌜x⌝ = [] ⊃ ∞;(a = x.last ⊃ ⌜# x - 1⌝ ;lastoc(a, ⌜x.butlast⌝ ))) | A User Theorem |
| lastoc-inf-ant | ⊦ ¬ lastoc(a, σ) ≠ ∞ ↔ (∀ n. ⌜n⌝ < # σ → σ[n] ≠ a) ∨ # σ = ∞ ∧ (∀ n. ∃ n0. n ≤ n0 ∧ σ[n0] = a) | A User Theorem |
| lastoc-less-size | ⊦ # σ < lastoc(a, σ) ↔ ¬ ¬(# σ ≠ ∞ ∧ (∀ n. ⌜n⌝ < # σ → σ[n] ≠ a)) | A User Theorem |
| lastoc-less-succsize | ⊦ # σ < lastoc(a, σ) + ⌜1⌝ ↔ ¬ ¬(# σ ≠ ∞ ∧ (∀ n. ⌜n⌝ < # σ → σ[n] ≠ a)) | A User Theorem |
| lastoc-rw-inf | ⊦ (∀ n. ⌜n⌝ < # σ → σ[n] ≠ a) ∨ # σ = ∞ ∧ (∀ n. ∃ n0. n ≤ n0 ∧ σ[n0] = a) → lastoc(a, σ) = ∞ | A User Theorem |
| lastocfin-cnteqcntto | ⊦ ⌜n⌝ = lastoc(a, σ) + ⌜1⌝ → cnt(a, σ) = cnt(a, σ to n) | A User Theorem |
| lim-evconst | ⊦ mon(σf) ∧ (∀ n. m < n → σf(m) = σf(n)) → lim(σf) = σf(m) | A User Theorem |
| lim-exists | mon(σf) ⊦ ∃ σ. (∀ n. σf(n) ⊑ σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n. σ to m ⊑ σf(n))) | A User Theorem |
| lim-finsize | mon(σf) ⊦ # lim(σf) ≠ ∞ ↔ (∃ m. lim(σf) = σf(m) ∧ # σf(m) ≠ ∞ ∧ (∀ m0. m < m0 → σf(m0) = σf(m))) | A User Theorem |
| lim-infsize | mon(σf) ⊦ # lim(σf) = ∞ ↔ (∃ n. # σf(n) = ∞ ∨ (∀ m. ∃ n. m < n ∧ σf(m) ≠ σf(n))) | A User Theorem |
| lim-infsize-strong | mon(σf) ⊦ # lim(σf) = ∞ ↔ (∃ n. # σf(n) = ∞ ∨ (∀ m. ∃ n. ¬ # σf(n) < ⌜m⌝ )) | A User Theorem |
| lim-unique | mon(σf), ∀ n. σf(n) ⊑ σ, ∀ n. σf(n) ⊑ σ0, ∀ m. ¬ # σ < ⌜m⌝ → (∃ n. σ to m ⊑ σf(n)), ∀ m. ¬ # σ0 < ⌜m⌝ → (∃ n. σ0 to m ⊑ σf(n)) ⊦ σ = σ0 | A User Theorem |
| mon-bd-or-unbound | mon(σf) ⊦ (∃ m. ∀ m0. m < m0 → σf(m0) = σf(m)) ∨ (∀ n. ∃ m. ¬ # σf(m) < ⌜n⌝ ) | A User Theorem |
| mon-cntprefix | ⊦ σ ⊑ σ0 → ¬ cnt(a, σ0) < cnt(a, σ) | A User Theorem |
| mon-cntto | ⊦ ¬ # σ < ⌜n⌝ → ¬ cnt(a, σ) < cnt(a, σ to n) | A User Theorem |
| mon-cnttoinf | ⊦ ¬ # σ < n∞ → ¬ cnt(a, σ) < cnt(a, σ to∞ n∞) | A User Theorem |
| mon-filterfun | ⊦ mon(λ n. filter(p, ⌜nf to n⌝ )) | A User Theorem |
| mon-filterprefix | ⊦ σ ⊑ σ0 → (¬ filter(p, σ) ⊑ filter(p, σ0) ↔ false) | A User Theorem |
| mon-filterto | ⊦ ⌜n⌝ < # σ → (¬ filter(p, σ to n) ⊑ filter(p, σ) ↔ false) | A User Theorem |
| mon-filtertoinf | ⊦ n∞ < # σ → (¬ filter(p, σ to∞ n∞) ⊑ filter(p, σ) ↔ false) | A User Theorem |
| mon-lem | mon(σf), m ≤ n ⊦ σf(m) ⊑ σf(n) | A User Theorem |
| mon-remfun | ⊦ mon(λ n. rem(⌜nf to n⌝ , np)) | A User Theorem |
| prefix-antisymm | ⊦ σ ⊑ σ0 → (σ0 ⊑ σ ↔ σ = σ0) | A User Theorem |
| prefix-append | ⊦ σ ⊑ σ + σ0 | A User Theorem |
| prefix-empty1 | ⊦ [] ⊑ σ | A User Theorem |
| prefix-empty2 | ⊦ σ ⊑ [] ↔ σ = [] | A User Theorem |
| prefix-notsmallersize | ⊦ σ ⊑ σ0 → (¬ ¬ # σ0 < # σ ↔ false) | A User Theorem |
| prefix-refl | ⊦ σ ⊑ σ | A User Theorem |
| prefix-trans | ⊦ σ ⊑ σ0 ∧ σ0 ⊑ σ1 → σ ⊑ σ1 | A User Theorem |
| prefixself-equal | ⊦ σ + σ0 ⊑ σ ↔ ¬ ¬(σ0 = [] ∨ # σ = ∞) | A User Theorem |
| rem-cntequal-fin | ⊦ cnt(a, rem(⌜x⌝ , np)) ≠ cnt(a, ⌜x⌝ ) ↔ (∃ n. n < # x ∧ np(n) ∧ x[n] = a) | A User Theorem |
| rem-cntleq | ⊦ ¬ ¬ cnt(a, σ) < cnt(a, rem(σ, np)) ↔ false | A User Theorem |
| rem-equal-fin | ⊦ rem(⌜x⌝ , np) = ⌜x⌝ ↔ (∀ m. m < # x → ¬ np(m)) | A User Theorem |
| rem-equal-inf | ⊦ (∀ m. ¬ np(m)) → rem(⌜nf⌝ , np) = ⌜nf⌝ | A User Theorem |
| rem-member1 | ⊦ ⌜m⌝ < # rem(σ, np) → (∃ m0. ⌜m0⌝ < # σ ∧ σ[m0] = rem(σ, np)[m] ∧ ¬ np(m0)) | A User Theorem |
| rem-member1-fin | ⊦ ⌜m⌝ < # rem(⌜x⌝ , np) → (∃ m0. m0 < # x ∧ x[m0] = rem(⌜x⌝ , np)[m] ∧ ¬ np(m0)) | A User Theorem |
| rem-member2 | ⊦ ⌜m0⌝ < # σ ∧ ¬ np(m0) → (∃ m. ⌜m⌝ < # rem(σ, np) ∧ rem(σ, np)[m] = σ[m0]) | A User Theorem |
| rem-member2-fin | ⊦ m0 < # x ∧ ¬ np(m0) → (∃ m. ⌜m⌝ < # rem(⌜x⌝ , np) ∧ rem(⌜x⌝ , np)[m] = x[m0]) | A User Theorem |
| rem-one | ⊦ rem(⌜a '⌝ , np) = (np(0) ⊃ [];⌜a '⌝ ) | A User Theorem |
| rem-rec-finsize | ⊦ # σ = ⌜n⌝ → rem(σ + ⌜a '⌝ , np) = rem(σ, np) + (np(n) ⊃ [];⌜a '⌝ ) | A User Theorem |
| rem-rec-gen | ⊦ # σ ≠ ∞ → rem(σ + ⌜a '⌝ , np) = rem(σ, np) + (np((# σ).n) ⊃ [];⌜a '⌝ ) | A User Theorem |
| rem-rec-rev | ⊦ rem(⌜a '⌝ + σ, np) = (np(0) ⊃ [];⌜a '⌝ ) + rem(σ, λ n. np(n + 1)) | A User Theorem |
| rem-rec-rev-fin | ⊦ rem(⌜a '⌝ + ⌜x⌝ , np) = (np(0) ⊃ [];⌜a '⌝ ) + rem(⌜x⌝ , λ n. np(n + 1)) | A User Theorem |
| rem-reminv-cnt-add | ⊦ cnt(a, rem(σ, np)) + cnt(a, rem(σ, λ n. ¬ np(n))) = cnt(a, σ) | A User Theorem |
| rem-reminv-size-add | ⊦ # rem(σ, np) + # rem(σ, λ n. ¬ np(n)) = # σ | A User Theorem |
| rem-shortens | ⊦ ¬ ¬ # σ < # rem(σ, np) ↔ false | A User Theorem |
| remfin-append | ⊦ rem(⌜x⌝ + σ, np) = rem(⌜x⌝ , np) + rem(σ, λ n. np(n + # x)) | A User Theorem |
| remfin-fin | ⊦ finp(rem(⌜x⌝ , np)) | A User Theorem |
| remfin-fin2 | ⊦ # rem(⌜x⌝ , np) ≠ ∞ | A User Theorem |
| reminf-finsize | ⊦ # rem(⌜nf⌝ , np) ≠ ∞ ↔ (∃ n. rem(⌜nf⌝ , np) = rem(⌜nf to n⌝ , np) ∧ (∀ n0. n < n0 → np(n0))) | A User Theorem |
| reminf-infsize | ⊦ # rem(⌜nf⌝ , np) = ∞ ↔ (∀ n. ∃ n0. n ≤ n0 ∧ ¬ np(n0)) | A User Theorem |
| reminf-infsize-strong | ⊦ # rem(⌜nf⌝ , np) = ∞ ↔ (∀ m. ∃ n. # rem(⌜nf to n⌝ , np) = ⌜m⌝ ) | A User Theorem |
| remnone-cntequal | ⊦ (∀ n. ⌜n⌝ < # σ ∧ np(n) → σ[n] ≠ a) → cnt(a, rem(σ, np)) = cnt(a, σ) | A User Theorem |
| remto-fin | ⊦ # rem(σ to n, np) ≠ ∞ | A User Theorem |
| to-is-prefix | ⊦ ⌜n⌝ < # σ → σ to n ⊑ σ | A User Theorem |