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: |
|---|---|---|
| ex-notin | ⊦ ∃ n. ¬ n ∈ ns | A User Theorem |
| ex-smallest-notin | ⊦ ∃ n. ¬ n ∈ ns ∧ (∀ m. ¬ m ∈ ns → n ≤ m) | A User Theorem |
| le-add-bound | ⊦ ns < n ∧ n ≤ m → (¬ ns < m ↔ false) | A User Theorem |
| ls-add-1 | ⊦ ns ++ n < n + 1 ↔ ns < n + 1 | A User Theorem |
| ls-add-bound | ⊦ ns < n → ns < n + 1 | A User Theorem |
| max-plus-one | ⊦ ns ≠ ∅ → (ns.max + 1 ∈ ns ↔ false) | A User Theorem |