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: |
|---|---|---|
| diag-theorem-butlast | ∀ n, a. nextl(n, a) ≠ [] ∧ nextl(n, a).first = a ⊦ ∃ σ, ii. ii(0) = 0 ∧ σ[0] = a ∧ σ ≠ [] ∧ (∀ n. ii(n + 1) = ii(n) + # nextl(n, σ[ii(n)]) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # nextl(n, σ[ii(n)]) = ⌜nextl(n, σ[ii(n)])⌝ ) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n) + 1⌝ ∧ (∀ m. n ≤ m → nextl(m, σ[ii(m)]) = σ[ii(m)] ' ∧ ii(n) = ii(m));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) | A User Theorem |
| infinite-append | ⊦ ∃ σ, ii. ii(0) = 0 ∧ (∀ n. ii(n + 1) = ii(n) + # lf(n) ∧ ¬ # σ < ⌜ii(n + 1)⌝ ∧ (σ from ii(n)) to # lf(n) = ⌜lf(n)⌝ ) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n)⌝ ∧ (∀ m. n ≤ m → lf(m) = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) | A User Theorem |
| infinite-append-butlast | ∀ n. lf(n).last = lf(n + 1).first ∧ lf(n) ≠ [] ⊦ ∃ σ, ii. ii(0) = 0 ∧ (∀ n. ii(n + 1) = ii(n) + # lf(n) - 1 ∧ ⌜ii(n + 1)⌝ < # σ ∧ (σ from ii(n)) to # lf(n) = ⌜lf(n)⌝ ) ∧ (∀ m, n. m ≤ n → ii(m) ≤ ii(n)) ∧ (finp(σ) ⊃ ∃ n. # σ = ⌜ii(n) + 1⌝ ∧ (∀ m. n ≤ m → lf(m).rest = [] ∧ ii(m) = ii(n));∀ n. ∃ m. ii(m) ≤ n ∧ n < ii(m + 1)) | A User Theorem |
| infinite-append-lem | ⊦ ∀ n. ∃ nf, ii. ii(0) = 0 ∧ (∀ m. m < n → ii(m + 1) = ii(m) + # lf(m) ∧ (nf from ii(m)) to # lf(m) = lf(m) ∧ (∀ m0. m0 ≤ m → ii(m0) ≤ ii(m))) | A User Theorem |
| nextl-lemma | ⊦ ∃ lf. lf(0) = nextl(0, a) ∧ (∀ n. lf(n + 1) = nextl(n + 1, lf(n).last)) | A User Theorem |
| nextl-lemma-butlast | ⊦ ∃ lf. lf(0) = a ' ∧ (∀ n. lf(n + 1) = nextl(n, lf(n).last)) | A User Theorem |
| nextl-lemma-butlast-nonempty | ∀ n, a. nextl(n, a) ≠ [] ⊦ ∃ lf. lf(0) = a ' ∧ (∀ n. lf(n + 1) = nextl(n, lf(n).last) ∧ lf(n) ≠ []) | A User Theorem |
| nextl-nextj-lemma-butlast | ⊦ ∃ lf, jj. lf(0) = a ' ∧ jj(0) = n0 ∧ (∀ n. lf(n + 1) = nextl(jj(n), lf(n).last) ∧ jj(n + 1) = nextj(jj(n), lf(n).last)) | A User Theorem |
| weakmon-lem | ∀ n. ii(n) ≤ ii(n + 1) ⊦ (∀ n. ∃ m. ii(m) ≥ n) ∨ (∃ n. ∀ m. m ≥ n → ii(m) = ii(n)) | A User Theorem |