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 | ⊦ min(n, m) = (n < m ⊃ n;m) | An Axiom |
| max | ⊦ max(n, m) = (n < m ⊃ m;n) | An Axiom |
| max-0-left | ⊦ max(0, n) = n | A User Theorem |
| max-0-right | ⊦ max(n, 0) = n | A User Theorem |
| max-eq-0 | ⊦ max(n, m) = 0 ↔ n = 0 ∧ m = 0 | A User Theorem |
| max-first-le | ⊦ n ≤ m → max(n, m) = m | A User Theorem |
| max-first-ls | ⊦ n < m → max(n, m) = m | A User Theorem |
| max-le1 | ⊦ n ≤ max(n, m) | A User Theorem |
| max-le2 | ⊦ m ≤ max(n, m) | A User Theorem |
| max-notls1 | ⊦ ¬ max(n, m) < n | A User Theorem |
| max-notls2 | ⊦ ¬ max(n, m) < m | A User Theorem |
| max-same | ⊦ max(n, n) = n | A User Theorem |
| max-second-le | ⊦ m ≤ n → max(n, m) = n | A User Theorem |
| max-second-ls | ⊦ m < n → max(n, m) = n | A User Theorem |
| min-0-left | ⊦ min(0, n) = 0 | A User Theorem |
| min-0-right | ⊦ min(n, 0) = 0 | A User Theorem |
| min-le-left | ⊦ n0 ≤ n1 → min(n0, n1) = n0 | A User Theorem |
| min-le-leftn | ⊦ n0 ≤ n1 → min(n0, n1 + n) = n0 | A User Theorem |
| min-ls-right | ⊦ n1 < n0 → min(n0, n1) = n1 | A User Theorem |
| min-ls1-right | ⊦ n1 < n0 → min(n0, n1 + 1) = n1 + 1 | A User Theorem |
| min-notls1 | ⊦ ¬ n < min(n, m) | A User Theorem |
| min-notls2 | ⊦ ¬ m < min(n, m) | A User Theorem |
| min-same | ⊦ min(n, n) = n | A User Theorem |