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: |
|---|---|---|
| le-e | ⊦ ordered≤([]) | An Axiom |
| le-o | ⊦ ordered≤(a ') | An Axiom |
| le-r | ⊦ ordered≤(a ' + b ' + x) ↔ ¬ b < a ∧ ordered≤(b + x) | An Axiom |
| ls-e | ⊦ ordered<([]) | An Axiom |
| ls-o | ⊦ ordered<(a ') | An Axiom |
| ls-r | ⊦ ordered<(a ' + b ' + x) ↔ a < b ∧ ordered<(b + x) | An Axiom |
| ins-e | ⊦ ins≤(a, []) = a ' | An Axiom |
| ins-y | ⊦ ¬ b < a → ins≤(a, b ' + x) = a + b + x | An Axiom |
| ins-n | ⊦ b < a → ins≤(a, b ' + x) = b + ins≤(a, x) | An Axiom |
| app | ⊦ ordered≤(x + y) → ordered≤(x) | A User Theorem |
| app-01 | ⊦ ordered≤(x + y) → ordered≤(y) | A User Theorem |
| app-02 | ⊦ ordered≤(x + y + z) → ordered≤(y) | A User Theorem |
| cons | ⊦ ordered<(a ' + x) → ordered<(x) | A User Theorem |
| cons-02 | ⊦ ordered≤(a ' + x) → ordered≤(x) | A User Theorem |
| cons-03 | ⊦ ordered≤(a ' + x) → ins≤(a, x) = a ' + x | A User Theorem |
| del1 | ⊦ ordered<(x) → ordered<(x -1l a) | A User Theorem |
| del1-01 | ⊦ ordered≤(x) → ordered≤(x -1l a) | A User Theorem |
| del1-01-01 | ⊦ ordered≤(a ' + (x -1l a)) ∧ ordered≤(x) ∧ a ∈ x → a ' + (x -1l a) = x | A User Theorem |
| del1-01-02 | ⊦ a ≠ b ∧ ordered≤(x) → ins≤(a, x -1l b) = ins≤(a, x) -1l b | A User Theorem |
| del1-02 | ⊦ ins≤(a, x) -1l a = x | A User Theorem |
| empty | ⊦ ins≤(a, x) ≠ [] | A User Theorem |
| eq | ⊦ ins≤(a, x) = ins≤(a, y) ↔ x = y | A User Theorem |
| eqdef | perm(x, y), ordered≤(x), ordered≤(y) ⊦ x = y | A User Theorem |
| ex | ⊦ ∃ y, z. ins≤(a, x) = y + a ' + z ∧ x = y + z | A User Theorem |
| in-01-02 | ⊦ a ≠ b → (a ∈ ins≤(b, x) ↔ a ∈ x) | A User Theorem |
| in-04 | ⊦ a ∈ ins≤(a, x) | A User Theorem |
| ins-less-first | ⊦ ordered≤(x) ∧ x ≠ [] ∧ ¬ a < x.first → ins≤(a, x) = x.first + ins≤(a, x.rest) | A User Theorem |
| ins-less-last | ⊦ ¬ a0 < a → ins≤(a, x + a0 ') = ins≤(a, x) + a0 ' | A User Theorem |
| ins-one | ⊦ b < a → ins≤(a, b ') = b ' + a ' | A User Theorem |
| ins-one-01 | ⊦ ¬ b < a → ins≤(a, b ') = a ' + b ' | A User Theorem |
| ins-one-02 | ⊦ a < b → ins≤(a, b ') = a ' + b ' | A User Theorem |
| ins-rec | ⊦ x ≠ [] ∧ x.first < a → ins≤(a, x) = x.first + ins≤(a, x.rest) | A User Theorem |
| ins-y-01 | ⊦ a < b → ins≤(a, b ' + x) = a + b + x | A User Theorem |
| ins-yes | ⊦ x ≠ [] ∧ ¬ x.first < a → ins≤(a, x) = a + x | A User Theorem |
| ins2 | ⊦ ins≤(a, ins≤(b, x)) = ins≤(b, ins≤(a, x)) ↔ true | A User Theorem |
| insperm | ⊦ perm(a ' + x, ins≤(a, x)) | A User Theorem |
| insperm-01 | ⊦ perm(ins≤(a, x), ins≤(a, y)) ↔ perm(x, y) | A User Theorem |
| insperm-02 | ⊦ perm(ins≤(a, x + y), ins≤(a, x) + y) | A User Theorem |
| insperm-03 | ⊦ perm(ins≤(a, x), y) ↔ perm(a + x, y) | A User Theorem |
| k-le-r | ⊦ ordered≤(y) ↔ # y ≤ 1 ∨ ¬ y.rest.first < y.first ∧ ordered≤(y.rest) | A User Theorem |
| k-ls-r | ⊦ ordered<(y) ↔ # y ≤ 1 ∨ y.first < y.rest.first ∧ ordered<(y.rest) | A User Theorem |
| len | ⊦ # ins≤(a, x) = # x + 1 | A User Theorem |
| ole | ⊦ ordered≤(x) → ordered≤(ins≤(a, x)) | A User Theorem |
| ole-01 | ⊦ ordered≤(ins≤(a, x)) ↔ ordered≤(x) | A User Theorem |
| ole-in | ⊦ ordered≤(a ' + x) ∧ b ∈ x → ¬ b < a | A User Theorem |
| ole-last | ⊦ ordered≤(x + a ') → (ordered≤(x + a ' + b ') ↔ ¬ b < a) | A User Theorem |
| ole-last-01 | ⊦ ordered≤(x) ∧ x ≠ [] → (ordered≤(x + a ') ↔ ¬ a < x.last) | A User Theorem |
| ole-rec | ⊦ x ≠ [] ∧ x.rest ≠ [] → (ordered≤(x) ↔ ¬ x.rest.first < x.first ∧ ordered≤(x.rest)) | A User Theorem |
| ole-two | ⊦ ordered≤(a ' + b ') ↔ ¬ b < a | A User Theorem |
| ols-rec | ⊦ x ≠ [] ∧ x.rest ≠ [] → (ordered<(x) ↔ x.first < x.rest.first ∧ ordered<(x.rest)) | A User Theorem |
| one-02 | ⊦ ins≤(a, a ') = a ' + a ' | A User Theorem |
| ordered-append | ⊦ ordered≤(x) ∧ ordered≤(x0) ∧ (x ≠ [] ∧ x0 ≠ [] → ¬ x0.first < x.last) → ordered≤(x + x0) | A User Theorem |
| ordered-ex-divide-lels | ordered≤(x) ⊦ ∃ y, z. x = y + z ∧ (∀ b. b ∈ y → b < a ∨ b = a) ∧ (∀ b. b ∈ z → a < b) | A User Theorem |
| ordered-ex-divide-lsle | ordered≤(x) ⊦ ∃ y, z. x = y + z ∧ (∀ b. b ∈ y → b < a) ∧ (∀ b. b ∈ z → b = a ∨ a < b) | A User Theorem |
| ordered-postfix | ⊦ x ⊒ x0 ∧ ordered≤(x0) → (¬ ¬ ordered≤(x) ↔ true) | A User Theorem |
| ordered-prefix | ⊦ x ⊑ x0 ∧ ordered≤(x0) → (¬ ¬ ordered≤(x) ↔ true) | A User Theorem |
| ordered-shorter-sublist | ⊦ ordered≤(sublist(m0, n1 + 1, x)) ∧ n2 < n1 ∧ n1 + m0 < # x → (¬ ordered≤(sublist(m0, n2 + 1, x)) ↔ false) | A User Theorem |
| orderedle-all | ⊦ ordered≤(x) ↔ (∀ m, n. m ≤ n ∧ n < # x → ¬ x[n] < x[m]) | A User Theorem |
| orderedle-ls | ⊦ b < a ∧ b ∈ x → ¬ ordered≤(a ' + x) | A User Theorem |
| orderedls-all | ⊦ ordered<(x) ↔ (∀ m, n. m < n ∧ n < # x → x[m] < x[n]) | A User Theorem |
| orderedls-ls | ⊦ b < a ∧ b ∈ x → ¬ ordered<(a ' + x) | A User Theorem |
| perm-ins | ⊦ perm((x + ins≤(a, y)) -1l a, z) ↔ perm(x + y, z) | A User Theorem |
| rest | ⊦ ordered<(x) ∧ x ≠ [] → ordered<(x.rest) | A User Theorem |
| rest-01 | ⊦ ordered≤(x) ∧ x ≠ [] → ordered≤(x.rest) | A User Theorem |
| same | ⊦ ins≤(a, a ' + x) = a ' + a ' + x | A User Theorem |
| sw | ⊦ ins≤(a, ins≤(b, x)) = ins≤(b, ins≤(a, x)) | A User Theorem |