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: |
|---|---|---|
| push-rec | ⊦ push(a, x ' + xs) = (¬ x.first < a ⊃ (a + x) + xs;x + push(a, xs)) | An Axiom |
| push-base | ⊦ push(a, []) = (a + []) + [] | An Axiom |
| solitaireh-rec | ⊦ solitaireh(a ' + x, xs) = solitaireh(x, push(a, xs)) | An Axiom |
| solitaireh-base | ⊦ solitaireh([], xs) = xs | An Axiom |
| solitaire-def | ⊦ solitaire(x) = solitaireh(x, []) | An Axiom |
| pushx-rec | ⊦ pushx(n, ix ' + ixs, x) = (¬ x[ix.first] < x[n] ⊃ (n + ix) + ixs;ix + pushx(n, ixs, x)) | An Axiom |
| pushx-base | ⊦ pushx(n, [], x) = (n + []) + [] | An Axiom |
| solixh-rec | ⊦ n < # x → solixh(x, n, ixs) = solixh(x, n + 1, pushx(n, ixs, x)) | An Axiom |
| solixh-base | ⊦ n = # x → solixh(x, n, ixs) = ixs | An Axiom |
| solix-def | ⊦ solix(x) = solixh(x, 0, []) | An Axiom |
| allls-rec | ⊦ all<(n0 ' + ix, n) ↔ n0 < n ∧ all<(ix, n) | An Axiom |
| allls-base | ⊦ all<([], n) | An Axiom |
| tolist-rec | ⊦ (n ' + ix).tolist(x) = x[n] + ix.tolist(x) | An Axiom |
| tolist-base-02 | ⊦ ([]).tolist(x) = [] | An Axiom |
| tolistl-rec | ⊦ (ix ' + ixs).tolist(x) = ix.tolist(x) + ixs.tolist(x) | An Axiom |
| tolistl-base | ⊦ ([]).tolist(x) = [] | An Axiom |
| precedes-def | ⊦ precedes(n, m, x) ↔ n < m ∧ m < # x ∧ x[n] < x[m] | An Axiom |
| inv-rec | ⊦ inv(ix ' + ixs, n) ↔ ix ≠ [] ∧ all<(ix, n) ∧ inv(ixs, n) | An Axiom |
| inv-base | ⊦ inv([], n) | An Axiom |
| ascsubseq-rec | ⊦ ascsubseq(n ' + m ' + ix, x) ↔ precedes(n, m, x) ∧ ascsubseq(m + ix, x) | An Axiom |
| ascsubseq-single | ⊦ ascsubseq(n ', x) ↔ n < # x | An Axiom |
| ascsubseq-base | ⊦ ascsubseq([], x) | An Axiom |
| precedesex-rec1 | ⊦ precedes∃(ix0 ' + ix1 ' + ixs, x) ↔ precedes∃(ix1 ' + ixs, x) ∧ (∀ n1. n1 ∈ ix1 → (∃ n0. n0 ∈ ix0 ∧ precedes(n0, n1, x))) | An Axiom |
| precedesex-rec0 | ⊦ precedes∃(ix ', x) | An Axiom |
| precedesex-base | ⊦ precedes∃([], x) | An Axiom |
| maxincseqno-def | ⊦ maxincseq#(x) = n ↔ (∃ ix. ascsubseq(ix, x) ∧ # ix = n ∧ (∀ ix. ascsubseq(ix, x) → # ix ≤ n)) | An Axiom |
| ordered-rec2 | ⊦ ordered(n0 ' + n1 ' + ix, x) ↔ ordered(n1 ' + ix, x) ∧ n0 > n1 ∧ ¬ x[n1] < x[n0] | An Axiom |
| ordered-rec1 | ⊦ ordered(n ', x) | An Axiom |
| ordered-base | ⊦ ordered([], x) | An Axiom |
| orderedl-rec | ⊦ ordered(ix ' + ixs, x) ↔ ordered(ix, x) ∧ ordered(ixs, x) | An Axiom |
| orderedl-base | ⊦ ordered([], x) | An Axiom |
| covers-def | ⊦ covers(ixs, n) ↔ (∀ n0. n0 < n → (∃ m. m < # ixs ∧ n0 ∈ ixs[m])) | An Axiom |
| coversi-def | ⊦ covers(ixs, ix) ↔ (∀ n. n ∈ ix → (∃ m. m < # ixs ∧ n ∈ ixs[m])) | An Axiom |
| allls-in | ⊦ n ∈ ix ∧ all<(ix, n0) → (n0 ≤ n ↔ false) | A User Theorem |
| allls-incbound | ⊦ all<(ix, n) → (¬ all<(ix, n + m) ↔ false) | A User Theorem |
| allls-single | ⊦ all<(m ', n) ↔ m < n | A User Theorem |
| ascsubseq-2 | ⊦ ascsubseq(n0 ' + n1 ', x) ↔ precedes(n0, n1, x) | A User Theorem |
| ascsubseq-append | ⊦ ascsubseq(ix + n0 ', x) → (¬ ascsubseq((ix + n0 ') + n ', x) ↔ ¬ precedes(n0, n, x)) | A User Theorem |
| ascsubseq-empty | ⊦ ascsubseq(ix, []) ↔ ix = [] | A User Theorem |
| ascsubseq-first-notin-rest | ⊦ ascsubseq(n ' + ix, x) → (n ∈ ix ↔ false) | A User Theorem |
| ascsubseq-in-size | ⊦ n ∈ ix ∧ ascsubseq(ix, x) → (# x ≤ n ↔ false) | A User Theorem |
| ascsubseq-nodups | ⊦ n ∈ ix0 ∧ ascsubseq(ix0 + ix1, x) → (n ∈ ix1 ↔ false) | A User Theorem |
| ascsubseq-prepend | ⊦ ascsubseq(n ' + ix, x) → (¬ ascsubseq(ix, x) ↔ false) | A User Theorem |
| ascsubseq-rem | ⊦ ascsubseq(ix0 + n ' + ix1, x) → (¬ ascsubseq(ix0 + ix1, x) ↔ false) | A User Theorem |
| ascsubseq-rest-notprec-first | ⊦ ascsubseq(n ' + ix, x) ∧ m ∈ ix → (precedes(m, n, x) ↔ false) | A User Theorem |
| covers-ascsubseq | ⊦ covers(ixs, # x) ∧ ascsubseq(ix, x) → (¬ covers(ixs, ix) ↔ false) | A User Theorem |
| covers-empty | ⊦ covers([], n) ↔ n = 0 | A User Theorem |
| covers-rem | ⊦ covers(ix ' + ixs, ix0 + n ' + ix1) ∧ ¬ covers(ixs, ix0 + ix1) → (∃ n. n ∈ ix ∧ (n ∈ ix0 ∨ n ∈ ix1)) | A User Theorem |
| coversi-append | ⊦ covers(ix0 ' + ixs, ix) ∧ ¬ covers(ixs, ix) → (∃ n. n ∈ ix0 ∧ n ∈ ix) | A User Theorem |
| coversi-empty | ⊦ covers([], ix) ↔ ix = [] | A User Theorem |
| inv-butlast | ⊦ inv(ixs + ix ', n) → (¬ inv(ixs, n) ↔ false) | A User Theorem |
| inv-incbound | ⊦ inv(ixs, n) → (¬ inv(ixs, n + m) ↔ false) | A User Theorem |
| inv-last-nonempty | ⊦ ixs ≠ [] ∧ inv(ixs, n) → ixs.last ≠ [] | A User Theorem |
| inv-single | ⊦ inv(ix ', n) ↔ ix ≠ [] ∧ all<(ix, n) | A User Theorem |
| ordered-precedes | ⊦ ordered(ix, x) ∧ n0 ∈ ix ∧ n1 ∈ ix → (precedes(n0, n1, x) ↔ false) | A User Theorem |
| ordered-precedes-h | ⊦ ordered(ix0 + n0 ' + ix1 + n1 ' + ix2, x) → n1 < n0 ∧ ¬ x[n1] < x[n0] | A User Theorem |
| ordered-single | ⊦ ordered(ix ', x) ↔ ordered(ix, x) | A User Theorem |
| orderedl-at | ⊦ n < # ixs ∧ ordered(ixs, x) → ordered(ixs[n], x) | A User Theorem |
| precedes-append | ⊦ precedes(n0, n1, x) → (¬ precedes(n0, n1, x + a ') ↔ false) | A User Theorem |
| precedes-ascsubseq-2 | ⊦ n0 ∈ ix ∧ n1 ∈ ix ∧ n0 ≠ n1 ∧ ascsubseq(ix, x) → precedes(n0, n1, x) ∨ precedes(n1, n0, x) | A User Theorem |
| precedes-ascsubseq-2-h | ⊦ ascsubseq(ix0 + n0 ' + ix1 + n1 ' + ix2, x) → (¬ precedes(n0, n1, x) ↔ false) | A User Theorem |
| precedes-irrefl | ⊦ precedes(n, m, x) → (precedes(m, n, x) ↔ false) | A User Theorem |
| precedes-notsame | ⊦ ¬ precedes(n, n, x) | A User Theorem |
| precedes-trans | ⊦ precedes(n, n0, x) ∧ precedes(n0, n1, x) → (¬ precedes(n, n1, x) ↔ false) | A User Theorem |
| precedesex-2 | ⊦ precedes∃(ix0 ' + ix1 ', x) ↔ (∀ n1. n1 ∈ ix1 → (∃ n0. n0 ∈ ix0 ∧ precedes(n0, n1, x))) | A User Theorem |
| precedesex-append | ⊦ inv(ixs, # x) ∧ precedes∃(ixs, x) → (¬ precedes∃(ixs, x + a ') ↔ false) | A User Theorem |
| precedesex-prepend | ⊦ precedes∃(ix ' + ixs, x) → (¬ precedes∃(ixs, x) ↔ false) | A User Theorem |
| precedesex-pushix | ⊦ precedes∃(ixs, x) ∧ inv(ixs, n) ∧ n < # x → (¬ precedes∃(pushx(n, ixs, x), x) ↔ false) | A User Theorem |
| precedesex-rev-rec1 | ⊦ precedes∃(ixs + ix0 ' + ix1 ', x) ↔ precedes∃(ixs + ix0, x) ∧ (∀ n1. n1 ∈ ix1 → (∃ n0. n0 ∈ ix0 ∧ precedes(n0, n1, x))) | A User Theorem |
| precedesex-solix | ⊦ precedes∃(solix(x), x) | A User Theorem |
| precedesex-solixh | ⊦ inv(ixs, n) ∧ n ≤ # x ∧ precedes∃(ixs, x) → precedes∃(solixh(x, n, ixs), x) | A User Theorem |
| pushix-to-push | ⊦ inv(ixs, # x0) → push(a, ixs.tolist(x0)) = pushx(# x0, ixs, x0 + a).tolist(x0 + a) | A User Theorem |
| pushx-covers | ⊦ covers(ixs, n) ∧ n < # x → (¬ covers(pushx(n, ixs, x), n + 1) ↔ false) | A User Theorem |
| pushx-cut-seq | ⊦ inv(ixs, # x) → pushx(# x, ixs, x + a ' + x0) = pushx(# x, ixs, x + a ') | A User Theorem |
| pushx-inv | ⊦ inv(ixs, # x) → (¬ inv(pushx(# x, ixs, x + a '), # x + 1) ↔ false) | A User Theorem |
| pushx-inv-gen | ⊦ inv(ixs, n) ∧ n < # x → (¬ inv(pushx(n, ixs, x), n + 1) ↔ false) | A User Theorem |
| pushx-nonrec | ⊦ n < # x ∧ ixs = pushx(n, ixs0, x) → ixs = ixs0 + n ' ' ∨ (∃ m. m < # ixs0 ∧ ixs = ixs0[m, n + ixs0[m]]) | A User Theorem |
| pushx-ordered | ⊦ ordered(ixs, x) ∧ inv(ixs, n) ∧ n < # x → (¬ ordered(pushx(n, ixs, x), x) ↔ false) | A User Theorem |
| solix-covers | ⊦ covers(solix(x), # x) | A User Theorem |
| solix-inv | ⊦ inv(solix(x), # x) | A User Theorem |
| solix-ordered | ⊦ ordered(solix(x), x) | A User Theorem |
| solix-to-solitaire | ⊦ solitaire(x) = solix(x).tolist(x) | A User Theorem |
| solixh-covers | ⊦ covers(ixs, n) ∧ n ≤ # x → covers(solixh(x, n, ixs), # x) | A User Theorem |
| solixh-inv | ⊦ inv(ixs, n) ∧ n ≤ # x → inv(solixh(x, n, ixs), # x) | A User Theorem |
| solixh-ordered | ⊦ ordered(ixs, x) ∧ inv(ixs, n) ∧ n ≤ # x → ordered(solixh(x, n, ixs), x) | A User Theorem |
| solixh-to-solitaireh | ⊦ inv(ixs, # x0) → solitaireh(x, ixs.tolist(x0)) = solixh(x0 + x, # x0, ixs).tolist(x0 + x) | A User Theorem |
| theorem | ⊦ # solitaire(x) = maxincseq#(x) | A User Theorem |
| theoremx | ⊦ # solix(x) = maxincseq#(x) | A User Theorem |
| theoremx-atleast | ⊦ ∃ ix. # ix = # solix(x) ∧ ascsubseq(ix, x) | A User Theorem |
| theoremx-atleast-ind | ⊦ inv(ixs + ix ', # x) ∧ precedes∃(ixs + ix ', x) → (∀ n. n ∈ ix → (∃ ix0. # ix0 = # ixs ∧ ascsubseq(ix0 + n, x))) | A User Theorem |
| theoremx-atmost-h | ⊦ ascsubseq(ix, x) ∧ # ixs < # ix ∧ covers(ixs, ix) → (∃ n0, n1, n. n0 ∈ ix ∧ n1 ∈ ix ∧ precedes(n0, n1, x) ∧ n < # ixs ∧ n0 ∈ ixs[n] ∧ n1 ∈ ixs[n]) | A User Theorem |
| tolist-cut-seq | ⊦ all<(ix, # x) → ix.tolist(x + a ') = ix.tolist(x) | A User Theorem |
| tolist-single | ⊦ ((# x)').tolist(x + a ') = a ' | A User Theorem |
| tolist-size | ⊦ # ixs.tolist(x) = # ixs | A User Theorem |
| tolistl-cut-seq | ⊦ inv(ixs, # x) → ixs.tolist(x + a ') = ixs.tolist(x) | A User Theorem |
| tolistl-single | ⊦ (ix ').tolist(x) = (ix.tolist(x))' | A User Theorem |