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: |
|---|---|---|
| min-base | ⊦ min(a ') = a | An Axiom |
| min-rec | ⊦ x ≠ [] → min(a ' + x) = (a < min(x) ⊃ a;min(x)) | An Axiom |
| max-base | ⊦ max(a ') = a | An Axiom |
| max-rec | ⊦ x ≠ [] → max(a ' + x) = (max(x) < a ⊃ a;max(x)) | An Axiom |
| ins-max | ⊦ ordered≤(x0) ∧ ¬ a < max(x0) → ins≤(a, x0) = x0 + a ' | A User Theorem |
| max-append | ⊦ x + x0 ≠ [] → max(x + x0) = max(x) ∨ max(x + x0) = max(x0) | A User Theorem |
| max-com | ⊦ x + x0 ≠ [] → (¬ max(x + x0) ≠ max(x0 + x) ↔ true) | A User Theorem |
| max-com-01 | ⊦ ¬ max(x + x0) < max(x0 + x) | A User Theorem |
| max-ge | ⊦ x ≠ [] → (¬ ¬ max(x + x0) < max(x) ↔ false) | A User Theorem |
| max-ge-01 | ⊦ x ≠ [] → ¬ max(a ' + x) < max(x) | A User Theorem |
| max-ge-every | ⊦ a ∈ x → (¬ ¬ max(x) < a ↔ false) | A User Theorem |
| max-ge-first | ⊦ ¬ ¬ max(a ' + x) < a ↔ false | A User Theorem |
| max-in | ⊦ max(a ' + x) = a ∨ max(a ' + x) = max(x) | A User Theorem |
| max-in-01 | ⊦ x ≠ [] → max(x) ∈ x | A User Theorem |
| max-ins | ⊦ ¬ max(x) < a ∧ x ≠ [] → max(ins≤(a, x)) = max(x) | A User Theorem |
| max-ins-last | ⊦ max(x) < a → ins≤(a, x).last = a | A User Theorem |
| max-ins-max | ⊦ ¬ a < max(x) → max(ins≤(a, x)) = a | A User Theorem |
| max-ins-max-last | ⊦ ¬ a < max(x0) ∧ ordered≤(x0) → ins≤(a, x0) = x0 + a ' | A User Theorem |
| max-ins-max-last-sort | ⊦ ¬ a < max(x0) → ins≤(a, sort(x0)) = sort(x0) + a ' | A User Theorem |
| max-ordered | ⊦ x ≠ [] ∧ max(x + x0) = max(x) ∧ ordered≤(x0) ∧ x1 ⊑ x0 → (max(x + x1) ≠ max(x + x0) ↔ false) | A User Theorem |
| max-sort-sublist | ⊦ x + x0 ≠ [] → max(sort(x + x0)) = max(x) ∨ max(sort(x + x0)) = max(x0) | A User Theorem |
| min-com | ⊦ x + x0 ≠ [] → (¬ min(x + x0) ≠ min(x0 + x) ↔ true) | A User Theorem |
| ordered-app-max | ⊦ x0 ≠ [] ∧ ¬ a < max(x0) ∧ ordered≤(x0) → (¬ ordered≤(x0 + a ') ↔ false) | A User Theorem |
| ordered-max | ⊦ x ≠ [] ∧ ordered≤(x) → max(x) = x.last | A User Theorem |
| sort-max | ⊦ x ≠ [] → max(sort(x)) = sort(x).last | A User Theorem |
| sort-max-append-1 | ⊦ ¬ a < max(x0) → sort(x0 + a ') = sort(x0) + a ' | A User Theorem |
| sort-max-last | ⊦ ¬ a < max(x + x0) → sort(x + a ' + x0) = sort(x + x0) + a ' | A User Theorem |
| sort-max-last-01 | ⊦ ¬ a < max(x + x0) → sort(x + x0 + a ') = sort(x + x0) + a ' | A User Theorem |
| sort-max-max-list | ⊦ x ≠ [] → max(sort(x)) = max(x) | A User Theorem |