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: |
|---|---|---|
| ls-base | ⊦ [] < n | An Axiom |
| ls-rec | ⊦ m ' + nx < n ↔ m < n ∧ nx < n | An Axiom |
| ls-add | ⊦ nx < m → (¬ nx < m + n ↔ false) | A User Theorem |
| ls-bound-notin | ⊦ nx < m → ¬ m ∈ nx | A User Theorem |
| ls-ext | ⊦ nx < m ↔ (∀ n. n ∈ nx → n < m) | A User Theorem |
| ls-prepend-bound-add1 | ⊦ nx < m → (¬ m ' + nx < m + 1 ↔ false) | A User Theorem |