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: |
|---|---|---|
| prefixn | ⊦ prefixn(n, x) = (n ≤ # x ⊃ firstn(n, x);x) | An Axiom |
| dropn | ⊦ dropn(n, x) = (n ≤ # x ⊃ restn(n, x);[]) | An Axiom |
| slice | ⊦ slice(n0, n1, x) = (n0 ≤ n1 ⊃ prefixn(n1 - n0, dropn(n0, x));[]) | An Axiom |
| dropn-0 | ⊦ dropn(0, x) = x | A User Theorem |
| dropn-empty | ⊦ dropn(n, []) = [] | A User Theorem |
| dropn-first | ⊦ n ≠ 0 → dropn(n, x) = (x = [] ⊃ [];dropn(n - 1, x.rest)) | A User Theorem |
| in-prefixn-at-smaller | ⊦ m < n ∧ m < # x → prefixn(n, x)[m] = x[m] | A User Theorem |
| in-prefixn-in-shorter-prefix | ⊦ a ∈ prefixn(n0, x) ∧ n0 ≤ n1 → a ∈ prefixn(n1, x) | A User Theorem |
| in-prefixn-pos-smaller | ⊦ a ∈ prefixn(n, x) → (¬ pos(a, x) < n ↔ false) | A User Theorem |
| in-prefixn-pos-smaller0 | ⊦ a ∈ prefixn(n, x) ∧ m ≤ pos(a, x) → m ≤ n | A User Theorem |
| in-prefixn-samepos | ⊦ a ∈ prefixn(n, x) → pos(a, prefixn(n, x)) = pos(a, x) | A User Theorem |
| prefix-append-one-sizeeq | # x0 = # x1 + 1 ⊦ x0 ⊑ x1 + a ' ↔ x0 = x1 + a ' | A User Theorem |
| prefix-prefixn-exact | n = # x0 ⊦ x0 ⊑ x1 → prefixn(n, x1) = x0 | A User Theorem |
| prefix-prefixn-not-shorter | ⊦ prefixn(n, x0) ⊑ x1 ∧ n < # x0 → (# x1 < n ↔ false) | A User Theorem |
| prefix-prefixn-same | ⊦ prefixn(n, x) ⊑ x | A User Theorem |
| prefixn-0 | ⊦ prefixn(0, x) = [] | A User Theorem |
| prefixn-append-left | ⊦ n ≤ # x → prefixn(n, x + y) = prefixn(n, x) | A User Theorem |
| prefixn-append-prefix | ⊦ x0 ⊑ prefixn(n, x0 + x1) ↔ n ≥ # x0 | A User Theorem |
| prefixn-append-slice | ⊦ n ≤ n0 → prefixn(n, x) + slice(n, n0, x) = prefixn(n0, x) | A User Theorem |
| prefixn-butlast | ⊦ n ≠ 0 ∧ n ≤ # x → prefixn(n, x).butlast = prefixn(n - 1, x) | A User Theorem |
| prefixn-empty | ⊦ prefixn(n, []) = [] | A User Theorem |
| prefixn-eq-append | y ≠ [] ⊦ prefixn(n, x) = prefixn(n, x + y) ↔ n ≤ # x | A User Theorem |
| prefixn-full | ⊦ prefixn(# x, x) = x | A User Theorem |
| prefixn-full-eq | ⊦ prefixn(n, x) ≠ x ↔ ¬ n ≥ # x | A User Theorem |
| prefixn-fulln | ⊦ # x ≤ m → prefixn(m, x) = x | A User Theorem |
| prefixn-in | ⊦ a ∈ prefixn(n, x) → (¬ a ∈ x ↔ false) | A User Theorem |
| prefixn-le-size | ⊦ # x ≤ # prefixn(n, x) ↔ prefixn(n, x) = x ∧ n ≥ # x | A User Theorem |
| prefixn-len-le-n | ⊦ # prefixn(n, x) ≤ n | A User Theorem |
| prefixn-len-n | n ≤ # x ⊦ # prefixn(n, x) = n | A User Theorem |
| prefixn-neq-empty-plusone | ⊦ prefixn(n + 1, x) ≠ [] ↔ x ≠ [] | A User Theorem |
| prefixn-nodups | ⊦ ¬ dups(x) → ¬ dups(prefixn(n, x)) | A User Theorem |
| prefixn-notin | ⊦ ¬ a ∈ x → ¬ a ∈ prefixn(n, x) | A User Theorem |
| prefixn-prefixn | ⊦ prefixn(n, prefixn(m, x)) = prefixn((n < m ⊃ n;m), x) | A User Theorem |
| prefixn-single-1 | ⊦ prefixn(1, a ') = a ' | A User Theorem |
| prefixn-size-eq | ⊦ # x0 = # x1 → (# prefixn(n, x0) = # prefixn(n, x1) ↔ true) | A User Theorem |
| prefixn-size-prefixn | ⊦ prefixn(# prefixn(n, x), x) = prefixn(n, x) | A User Theorem |
| prefixn-split-dropn | ⊦ n = n0 + n1 → prefixn(n, x) = prefixn(n0, x) + prefixn(n1, dropn(n0, x)) | A User Theorem |
| prefixn-split-sublist | ⊦ n0 + n1 = n ∧ n ≤ # x → prefixn(n, x) = prefixn(n0, x) + sublist(n0, n1, x) | A User Theorem |
| slice-range0 | ⊦ slice(n, n, x) = [] | A User Theorem |