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: |
|---|---|---|
| Even | ⊦ even(n) ↔ (∃ m. m + m = n) | An Axiom |
| Odd | ⊦ odd(n) ↔ ¬ even(n) | An Axiom |
| Min-right | ⊦ ¬ m < n → min(m, n) = n | An Axiom |
| Min-left | ⊦ m < n → min(m, n) = m | An Axiom |
| Max-right | ⊦ ¬ m < n → max(m, n) = m | An Axiom |
| Max-left | ⊦ m < n → max(m, n) = n | An Axiom |
| div2-elim | ⊦ odd(n) → (m = n / 2 ↔ n = m + m + 1) | A User Theorem |
| div2-elim-01 | ⊦ even(n) → (m = n / 2 ↔ n = m + m) | A User Theorem |
| div2-even | ⊦ n / 2 + n / 2 = n ↔ even(n) | A User Theorem |
| div2-odd | ⊦ n / 2 + n / 2 + 1 = n ↔ odd(n) | A User Theorem |
| div2-odd-01 | ⊦ n / 2 + n / 2 ≠ n ↔ odd(n) | A User Theorem |
| eo | ⊦ even(n) → ¬ odd(n) | A User Theorem |
| eo-01 | ⊦ ¬ even(n) ↔ odd(n) | A User Theorem |
| eo-02 | ⊦ even(n + 1) ↔ odd(n) | A User Theorem |
| even-add | ⊦ even(m + n) ↔ even(m) ∧ even(n) ∨ odd(m) ∧ odd(n) | A User Theorem |
| even-div2 | ⊦ even(n) → (n + 1) / 2 = n / 2 | A User Theorem |
| even-mult | ⊦ even(m * n) ↔ even(m) ∨ even(n) | A User Theorem |
| max-a | ⊦ max(m, max(n, n0)) = max(max(m, n), n0) | A User Theorem |
| max-c | ⊦ max(m, n) = max(n, m) | A User Theorem |
| max-distr | ⊦ max(m + 1, n + 1) = max(m, n) + 1 | A User Theorem |
| max-i | ⊦ max(m, m) = m | A User Theorem |
| meven-02 | ⊦ even(2 * m) | A User Theorem |
| meven-03 | ⊦ ¬ even(2 * m + 1) | A User Theorem |
| min-a | ⊦ min(m, min(n, n0)) = min(min(m, n), n0) | A User Theorem |
| min-c | ⊦ min(m, n) = min(n, m) | A User Theorem |
| min-distr | ⊦ min(m + 1, n + 1) = min(m, n) + 1 | A User Theorem |
| min-i | ⊦ min(m, m) = m | A User Theorem |
| min-ls-both | ⊦ min(m, n) < m → (min(m, n) < n ↔ false) | A User Theorem |
| min-ls-self1 | ⊦ ¬ m < min(m, n) | A User Theorem |
| min-ls-self2 | ⊦ ¬ n < min(m, n) | A User Theorem |
| min-neq1 | ⊦ m ≠ m0 → min(m, n) = m0 → n = m0 | A User Theorem |
| min-neq2 | ⊦ n ≠ m0 → min(m, n) = m0 → m = m0 | A User Theorem |
| min-zero1 | ⊦ min(0, m) = 0 | A User Theorem |
| min-zero2 | ⊦ min(m, 0) = 0 | A User Theorem |
| modd-02 | ⊦ odd(2 * m + 1) | A User Theorem |
| modd-03 | ⊦ ¬ odd(2 * m) | A User Theorem |
| odd | ⊦ n ≤ 1 → (odd(n) ↔ n = 1) | A User Theorem |
| odd-add | ⊦ odd(m + n) ↔ odd(m) ∧ even(n) ∨ even(m) ∧ odd(n) | A User Theorem |
| odd-div2 | ⊦ odd(n) → (n + 1) / 2 = n / 2 + 1 | A User Theorem |
| odd-mult | ⊦ odd(m * n) ↔ odd(m) ∧ odd(n) | A User Theorem |
| oe | ⊦ ¬ odd(n) ↔ even(n) | A User Theorem |
| oe-01 | ⊦ odd(n) → ¬ even(n) | A User Theorem |
| oe-02 | ⊦ odd(n + 1) ↔ even(n) | A User Theorem |
| oex | ⊦ odd(n) ↔ (∃ m. n = m + m + 1) | A User Theorem |
| one | ⊦ ¬ even(1) | A User Theorem |
| oone | ⊦ odd(1) | A User Theorem |
| otwo-02 | ⊦ odd(m + 2) ↔ odd(m) | A User Theorem |
| otwo-03 | ⊦ ¬ odd(2) | A User Theorem |
| ozero | ⊦ ¬ odd(0) | A User Theorem |
| plus | ⊦ even(m) → (even(m + n) ↔ even(n)) | A User Theorem |
| pot2-even-02 | ⊦ n / 2 * 2 = n ↔ even(n) | A User Theorem |
| pot2-odd-02 | ⊦ n / 2 * 2 + 1 = n ↔ odd(n) | A User Theorem |
| two-02 | ⊦ even(m + 2) ↔ even(m) | A User Theorem |
| two-03 | ⊦ n ≤ 2 ∧ n ≠ 0 → (even(n) ↔ n = 2) | A User Theorem |
| zero | ⊦ even(0) | A User Theorem |
| zero-01 | ⊦ n < 2 → (even(n) ↔ n = 0) | A User Theorem |
| zero-02 | ⊦ n ≤ 1 → (even(n) ↔ n = 0) | A User Theorem |