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: |
|---|---|---|
| totality | ⊦ a < b ∨ a = b ∨ b < a | An Axiom |
| transitivity | ⊦ a < b ∧ b < c → a < c | An Axiom |
| irreflexivity | ⊦ ¬ a < a | An Axiom |
| lel | ⊦ a < b ∧ a = c → c < b | A User Theorem |
| loc | ⊦ ¬ a < b ↔ ¬ ¬(a = b ∨ b < a) | A User Theorem |
| ls-le | ⊦ a < b → (¬ b < a ↔ true) | A User Theorem |
| nen | ⊦ ¬ b < a ∧ a = c → ¬ b < c | A User Theorem |
| nll | ⊦ ¬ b < a ∧ b < c → a < c | A User Theorem |
| nnn | ⊦ ¬ c < b ∧ ¬ a < c → ¬ a < b | A User Theorem |
| seq | ⊦ ¬ b < a → (¬ a < b ↔ a = b) | A User Theorem |
| sls | ⊦ a ≠ b → (¬ a < b ↔ b < a) | A User Theorem |