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: |
|---|---|---|
| maxinf-def | ⊦ (max∞(np) = ∞ ⊃ (∀ n. ∃ n0. n < n0 ∧ np(n0)) ∨ (∀ n. ¬ np(n));(∃ n. np(max∞(np).n)) ∧ (∀ m. np(m) → ¬ max∞(np) < ⌜m⌝ )) | An Axiom |
| stutf-def | ⊦ stutf(nσ) ↔ nσ ≠ [] ∧ nσ[0] = 0 ∧ (∀ n. ⌜n⌝ + ⌜1⌝ < # nσ → nσ[n + 1] = nσ[n] ∨ nσ[n + 1] = nσ[n] + 1) | An Axiom |
| monle-def | ⊦ mon≤(nσ) ↔ (∀ n. ⌜n⌝ + ⌜1⌝ < # nσ → nσ[n] ≤ nσ[n + 1]) | An Axiom |
| monls-def | ⊦ mon<(nσ) ↔ (∀ n. ⌜n⌝ + ⌜1⌝ < # nσ → nσ[n] < nσ[n + 1]) | An Axiom |
| inv-def | ⊦ stutf(nσ) → inv(nσ) = (leninv(nσ) = ∞ ⊃ ⌜λ m. max∞(λ n. ⌜n⌝ < # nσ ∧ nσ[n] = m).n⌝ ;⌜λ m. max∞(λ n. ⌜n⌝ < # nσ ∧ nσ[n] = m).n⌝ to leninv(nσ).n) | An Axiom |
| leninv-def | ⊦ leninv(nσ) = max∞(λ n. n ≠ 0 → (∃ m. ⌜m⌝ < # nσ ∧ nσ[m] = n - 1 ∧ ¬(# nσ = ∞ ∧ (∀ m0. m < m0 → nσ[m0] = n - 1)))) | An Axiom |
| min-def | ⊦ mon<(nσ) → (nσ = [] ⊃ min(nσ, n) = 0 ;(# nσ ≠ ∞ ∧ nσ[(# nσ).n - 1] < n ⊃ min(nσ, n) = (# nσ).n ;⌜min(nσ, n)⌝ < # nσ ∧ n ≤ nσ[min(nσ, n)] ∧ (∀ m. ⌜m⌝ < # nσ ∧ n ≤ nσ[m] → min(nσ, n) ≤ m) ) ) | An Axiom |
| eq-leninv | ⊦ ⌜n⌝ < # nσ ∧ stutf(nσ) → (⌜nσ[n]⌝ = leninv(nσ) ↔ # nσ = ∞ ∧ (∀ m. n < m ∧ ⌜m⌝ < # nσ → nσ[m] = nσ[n])) | A User Theorem |
| inv-get-inverse | ⊦ stutf(nσ) ∧ ⌜n⌝ < leninv(nσ) → nσ[inv(nσ)[n]] = n | A User Theorem |
| inv-get-inverse-between | ⊦ stutf(nσ) ∧ ⌜n⌝ + ⌜1⌝ < leninv(nσ) ∧ inv(nσ)[n] + m + 1 < inv(nσ)[n + 1] → nσ[inv(nσ)[n] + m + 1] = n + 1 | A User Theorem |
| inv-get-inverse-last | ⊦ stutf(nσ) ∧ ⌜n⌝ + ⌜1⌝ = leninv(nσ) ∧ ⌜inv(nσ)[n]⌝ + ⌜m⌝ + ⌜1⌝ < # nσ → nσ[inv(nσ)[n] + m + 1] = n + 1 | A User Theorem |
| inv-get-inverse-succ | ⊦ stutf(nσ) ∧ ⌜n⌝ < leninv(nσ) ∧ ⌜inv(nσ)[n]⌝ + ⌜1⌝ < # nσ → nσ[inv(nσ)[n] + 1] = n + 1 | A User Theorem |
| inv-get-inverse-succ-inf | ⊦ stutf(nσ) ∧ ⌜n⌝ < leninv(nσ) ∧ # nσ = ∞ → nσ[inv(nσ)[n] + 1] = n + 1 | A User Theorem |
| inv-get-lslen | ⊦ stutf(nσ) ∧ ⌜n⌝ < leninv(nσ) → (¬ ⌜inv(nσ)[n]⌝ < # nσ ↔ false) | A User Theorem |
| inv-inverts | ⊦ stutf(nσ) ∧ nσ[n + 1] = nσ[n] + 1 ∧ ⌜n⌝ + ⌜1⌝ < # nσ → inv(nσ)[nσ[n]] = n | A User Theorem |
| inv-inverts-last | ⊦ stutf(nσ) ∧ # nσ = ⌜n⌝ + ⌜1⌝ → inv(nσ)[nσ[n]] = n | A User Theorem |
| inv-inverts-leq | ⊦ stutf(nσ) ∧ ⌜n⌝ < # nσ ∧ ⌜nσ[n]⌝ < leninv(nσ) → (¬ ¬ inv(nσ)[nσ[n]] < n ↔ false) | A User Theorem |
| inv-ls-notleq | ⊦ stutf(nσ) ∧ ⌜n⌝ + ⌜1⌝ < leninv(nσ) → (inv(nσ)[n + 1] ≤ inv(nσ)[n] ↔ false) | A User Theorem |
| inv-ls-succ | ⊦ stutf(nσ) ∧ ⌜n⌝ + ⌜1⌝ < leninv(nσ) → inv(nσ)[n] < inv(nσ)[n + 1] | A User Theorem |
| leninv-inf | ⊦ stutf(nσ) → (leninv(nσ) = ∞ ↔ # nσ = ∞ ∧ (∀ m. ∃ m0. m < m0 ∧ nσ[m] < nσ[m0])) | A User Theorem |
| leninv-inf-strong | ⊦ stutf(nσ) → (¬ leninv(nσ) ≠ ∞ ↔ # nσ = ∞ ∧ (∀ m. ∃ m0. m < m0 ∧ nσ[m] < nσ[m0]) ∧ (∀ m. ∃ m0. m < nσ[m0])) | A User Theorem |
| leninv-invlast | ⊦ # nσ = ⌜m⌝ + ⌜1⌝ ∧ leninv(nσ) = ⌜n⌝ + ⌜1⌝ ∧ stutf(nσ) → nσ[m] = n | A User Theorem |
| leninv-invlast-2 | ⊦ leninv(nσ) = ⌜n⌝ + ⌜1⌝ ∧ # nσ = # nσ0 ∧ # nσ0 = ⌜m⌝ + ⌜1⌝ ∧ stutf(nσ) → nσ[m] = n | A User Theorem |
| leninv-invlast-inv | ⊦ # nσ = ⌜m⌝ + ⌜1⌝ ∧ leninv(nσ) = ⌜n⌝ + ⌜1⌝ ∧ stutf(nσ) → inv(nσ)[n] = m | A User Theorem |
| leninv-invlast-inv-2 | ⊦ leninv(nσ) = ⌜n⌝ + ⌜1⌝ ∧ # nσ = # nσ0 ∧ # nσ0 = ⌜m⌝ + ⌜1⌝ ∧ stutf(nσ) → inv(nσ)[n] = m | A User Theorem |
| leninv-is-len-inv | ⊦ stutf(nσ) → # inv(nσ) = leninv(nσ) | A User Theorem |
| leninv-less | ⊦ leninv(nσ) < n∞ ↔ (∃ n. leninv(nσ) = ⌜n⌝ ∧ ⌜n⌝ < n∞) | A User Theorem |
| leninv-succ | ⊦ stutf(nσ) → (leninv(nσ) = ⌜n⌝ + ⌜1⌝ ↔ (# nσ = ∞ ⊃ ∃ m. nσ[m] = n ∧ (∀ m0. m < m0 → nσ[m0] = n + 1);nσ[(# nσ).n - 1] = n)) | A User Theorem |
| leninv-zero | ⊦ stutf(nσ) → (leninv(nσ) = ⌜0⌝ ↔ nσ = ⌜λ n. 0⌝ ) | A User Theorem |
| leq-leninv | ⊦ ⌜n⌝ < # nσ ∧ stutf(nσ) → (leninv(nσ) < ⌜nσ[n]⌝ ↔ false) | A User Theorem |
| less-leninv | ⊦ stutf(nσ) ∧ # nσ = ∞ ∧ nσ[n + 1] = nσ[n] + 1 → (¬ ⌜nσ[n]⌝ < leninv(nσ) ↔ false) | A User Theorem |
| lsleninv-1 | ⊦ stutf(nσ) ∧ ⌜m⌝ < # nσ ∧ n < nσ[m] → (¬ ⌜n⌝ < leninv(nσ) ↔ false) | A User Theorem |
| lsleninv-2 | ⊦ n < nσ[m] ∧ # nσ = ⌜m⌝ + ⌜1⌝ ∧ stutf(nσ) → (¬ ⌜n⌝ < leninv(nσ) ↔ false) | A User Theorem |
| lsleninv-3 | ⊦ n < nσ[m] ∧ # nσ = # nσ0 ∧ # nσ0 = ⌜m⌝ + ⌜1⌝ ∧ stutf(nσ) → (¬ ⌜n⌝ < leninv(nσ) ↔ false) | A User Theorem |
| maxinf-fin | ⊦ max∞(np) = ⌜n⌝ ↔ np(n) ∧ (∀ m. np(m) → ¬ n < m) | A User Theorem |
| maxinf-inf | ⊦ max∞(np) = ∞ ↔ (∀ n. ∃ n0. n < n0 ∧ np(n0)) ∨ (∀ n. ¬ np(n)) | A User Theorem |
| maxinf-skolemf | ⊦ ∃ n∞. (n∞ = ∞ ⊃ (∀ n. ∃ n0. n < n0 ∧ np(n0)) ∨ (∀ n. ¬ np(n));(∃ n. np(n∞.n)) ∧ (∀ m. np(m) → ¬ n∞ < ⌜m⌝ )) | A User Theorem |
| min-empty | ⊦ min([], n) = 0 | A User Theorem |
| min-skolemf | ⊦ mon<(nσ) → (∃ m0. (nσ = [] ⊃ m0 = 0 ;(# nσ ≠ ∞ ∧ nσ[(# nσ).n - 1] < n ⊃ m0 = (# nσ).n;⌜m0⌝ < # nσ ∧ n ≤ nσ[m0] ∧ (∀ m. ⌜m⌝ < # nσ ∧ n ≤ nσ[m] → m0 ≤ m)) )) | A User Theorem |
| min-stutters | mon<(nσ) ⊦ min(nσ, n + 1) = 1 + min(nσ, n) ∨ min(nσ, n + 1) = min(nσ, n) | A User Theorem |
| min-zero | ⊦ mon<(nσ) → min(nσ, 0) = 0 | A User Theorem |
| mininv-inverts | ⊦ mon<(nσ) ∧ min(nσ, n + 1) = 1 + min(nσ, n) → nσ[min(nσ, n)] = n | A User Theorem |
| mininv-inverts-inner | ⊦ mon<(nσ) ∧ ⌜n⌝ < # nσ → min(nσ, nσ[n]) = n | A User Theorem |
| mininv-inverts-inner-succ | ⊦ mon<(nσ) ∧ ⌜n⌝ < # nσ → min(nσ, nσ[n] + 1) = n + 1 | A User Theorem |
| mininv-inverts-weak | ⊦ mon<(nσ) ∧ ⌜min(nσ, n)⌝ < # nσ → (¬ ¬ nσ[min(nσ, n)] < n ↔ false) | A User Theorem |
| mininv-inverts-weak2 | ⊦ mon<(nσ) ∧ ⌜min(nσ, n)⌝ < # nσ → (¬ n ≤ nσ[min(nσ, n)] ↔ false) | A User Theorem |
| mininv-stays-if-not-taken | mon<(nσ), ∀ m. ⌜m⌝ < # nσ → nσ[m] ≠ n ⊦ min(nσ, n + 1) = min(nσ, n) | A User Theorem |
| mon-eq | ⊦ mon<(nσ) ∧ ⌜n⌝ < # nσ ∧ ⌜n0⌝ < # nσ → (nσ[n] = nσ[n0] ↔ n = n0) | A User Theorem |
| monle-leq | ⊦ mon≤(nσ) ∧ m ≤ n ∧ ⌜n⌝ < # nσ → nσ[m] ≤ nσ[n] | A User Theorem |
| monls-append1 | ⊦ mon<(⌜nl⌝ + ⌜nl0⌝ ) → (¬ mon<(⌜nl⌝ ) ↔ false) | A User Theorem |
| monls-append2 | ⊦ mon<(⌜nl⌝ + ⌜nl0⌝ ) → (¬ mon<(⌜nl0⌝ ) ↔ false) | A User Theorem |
| monls-exists-maxleq | mon<(nσ), nσ[0] < n, n ≤ nσ[m], ⌜m⌝ < # nσ ⊦ ∃ m0. nσ[m0] < n ∧ n ≤ nσ[m0 + 1] ∧ m0 ≤ m | A User Theorem |
| monls-exists-maxls | mon<(nσ), nσ[0] ≤ n, n < nσ[m], ⌜m⌝ < # nσ ⊦ ∃ m0. nσ[m0] ≤ n ∧ n < nσ[m0 + 1] ∧ m0 ≤ m | A User Theorem |
| monls-from | ⊦ mon<(⌜nnf⌝ ) → (¬ mon<(⌜nnf from n⌝ ) ↔ false) | A User Theorem |
| monls-ls | ⊦ mon<(nσ) ∧ m < n ∧ ⌜n⌝ < # nσ → nσ[m] < nσ[n] | A User Theorem |
| monls-mon-implies-monls | ⊦ (∀ n. mon<(nσf(n))) ∧ mon(nσf) → (¬ mon<(lim(λ n. nσf(n))) ↔ false) | A User Theorem |
| monls-notsmall | ⊦ mon<(nσ) ∧ nσ[0] = 0 ∧ ⌜n + 1⌝ < # nσ → (¬ n < nσ[n + 1] ↔ false) | A User Theorem |
| monls-to | ⊦ mon<(⌜nnf⌝ ) → (¬ mon<(⌜nnf to n⌝ ) ↔ false) | A User Theorem |
| monlsinf-notsmall | ⊦ mon<(⌜nnf⌝ ) ∧ nnf(0) = 0 → (¬ n < nnf(n + 1) ↔ false) | A User Theorem |
| not-ls-leninv | ⊦ ⌜n⌝ < # nσ ∧ stutf(nσ) → (¬ ⌜nσ[n]⌝ < leninv(nσ) ↔ ⌜nσ[n]⌝ = leninv(nσ)) | A User Theorem |
| not-stutf-empty | ⊦ ¬ stutf([]) | A User Theorem |
| rem-preserves-monls | ⊦ mon<(nσ) → (¬ mon<(rem(nσ, np)) ↔ false) | A User Theorem |
| stutf-alltaken | ⊦ stutf(nσ) ∧ ⌜m⌝ < # nσ ∧ n ≤ nσ[m] → (∃ m0. m0 ≤ m ∧ nσ[m0] = n) | A User Theorem |
| stutf-alltakenmax | ⊦ stutf(nσ) ∧ ⌜m⌝ < # nσ ∧ n < nσ[m] → (∃ m0. m0 < m ∧ nσ[m0] = n ∧ nσ[m0 + 1] = n + 1) | A User Theorem |
| stutf-invmonls | ⊦ stutf(nσ) → (¬ mon<(inv(nσ)) ↔ false) | A User Theorem |
| stutf-maxinf-is-fin | ⊦ stutf(nσ) → (max∞(λ n. ⌜n⌝ < # nσ ∧ nσ[n] = m) = ∞ ↔ # nσ = ∞ ∧ (∃ n. ∀ n0. ¬ n0 < n → nσ[n0] = m) ∨ (∀ n. ⌜n⌝ < # nσ → nσ[n] < m)) | A User Theorem |
| stutf-monle | ⊦ stutf(nσ) → (¬ mon≤(nσ) ↔ false) | A User Theorem |
| stutf-nonempty | ⊦ stutf(nσ) → (¬ nσ ≠ [] ↔ false) | A User Theorem |
| stutf-notbig | ⊦ stutf(nσ) ∧ ⌜n⌝ < # nσ → (n < nσ[n] ↔ false) | A User Theorem |
| stutf-slowincrease | ⊦ stutf(nσ) ∧ ⌜m⌝ + ⌜n⌝ < # nσ → nσ[m + n] ≤ nσ[m] + n | A User Theorem |
| stutf-zero | ⊦ stutf(nσ) → nσ[0] = 0 | A User Theorem |
| succlessleninv-invsize | ⊦ ⌜n⌝ + ⌜1⌝ < leninv(nσ) ∧ stutf(nσ) → (¬ # nσ ≠ ⌜inv(nσ)[n]⌝ + ⌜1⌝ ↔ false) | A User Theorem |