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: |
|---|---|---|
| Ordered | ⊦ ordered≤(sort(x)) | An Axiom |
| Perm | ⊦ perm(x, sort(x)) | An Axiom |
| appins | ⊦ sort(x + ins≤(a, y)) = ins≤(a, sort(x + y)) | A User Theorem |
| combine-ordered-sublists | ⊦ ordered≤(x1) ∧ (x0 ≠ [] ∧ x1 ≠ [] → ¬ x1.first < sort(x0).last) → sort(x0) + x1 = sort(x0 + x1) | A User Theorem |
| del1 | ⊦ sort(x -1l a) = sort(x) -1l a | A User Theorem |
| empty | ⊦ sort([]) = [] | A User Theorem |
| emptyp | ⊦ sort(x) = [] ↔ x = [] | A User Theorem |
| eq | ⊦ ordered≤(x) → sort(x) = x | A User Theorem |
| in | ⊦ a ∈ sort(x) ↔ a ∈ x | A User Theorem |
| ins | ⊦ sort(ins≤(a, x)) = ins≤(a, sort(x)) | A User Theorem |
| ins-01 | ⊦ sort(ins≤(a, x) + y) = ins≤(a, sort(x + y)) | A User Theorem |
| ins-02 | ⊦ ordered≤(x + a ' + y) → ins≤(a, sort(x + y)) = x + a ' + y | A User Theorem |
| insdel | ⊦ ins≤(a, sort(x)) = y → sort(x) = y -1l a | A User Theorem |
| ole | ⊦ ordered≤(x + a ' + y) → sort(x + ins≤(a, y)) = x + a ' + y | A User Theorem |
| one | ⊦ sort(a ') = a ' | A User Theorem |
| ordered-perm-sort | ⊦ ordered≤(x) ∧ perm(x, x0) → sort(x0) = x | A User Theorem |
| perm | ⊦ perm(sort(x), y) ↔ perm(x, y) | A User Theorem |
| perm-01 | ⊦ perm(ins≤(a, sort(x)), y) ↔ perm(a ' + x, y) | A User Theorem |
| rec | ⊦ sort(a ' + x) = ins≤(a, sort(x)) | A User Theorem |
| size | ⊦ # sort(x) = # x | A User Theorem |
| size-01 | ⊦ # sort(a ' + x) = # x + 1 | A User Theorem |
| sort | ⊦ sort(sort(x)) = sort(x) | A User Theorem |
| sort-01 | ⊦ sort(sort(x) + y) = sort(x + y) | A User Theorem |
| sort-02 | ⊦ sort(x + sort(y)) = sort(x + y) | A User Theorem |
| sort-append | ⊦ sort(x + y) = sort(y + x) | A User Theorem |
| sort-append-three | ⊦ sort(x + x0 + x1) = sort(x0 + x + x1) | A User Theorem |
| sperm | ⊦ sort(x) = sort(y) ↔ perm(x, y) | A User Theorem |
| two | ⊦ b < a → sort(a ' + b ') = b ' + a ' | A User Theorem |
| two-01 | ⊦ ¬ b < a → sort(a ' + b ') = a ' + b ' | A User Theorem |