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: |
|---|---|---|
| Divdef | ⊦ n ≠ 0 → m / n * n ≤ m ∧ m < (m / n)+1 * n | An Axiom |
| Moddef | ⊦ n ≠ 0 → m = m / n * n + m % n | An Axiom |
| add | n ≠ 0 ⊦ (n0 + n) / n = n0 / n + 1 | A User Theorem |
| cond | n ≠ 0 ⊦ m / n * n ≤ m | A User Theorem |
| cond-01 | n ≠ 0 ⊦ ¬ m < m / n * n | A User Theorem |
| div-add | ⊦ m0 % n = 0 ∧ 0 ≠ n → (m + m0) / n = m / n + m0 / n | A User Theorem |
| div-elim | n ≠ 0 ⊦ m0 = m / n ∧ n0 = m % n ↔ m = m0 * n + n0 ∧ n0 < n | A User Theorem |
| div-le | ⊦ 1 < n → (m ≤ m / n ↔ m = 0) | A User Theorem |
| div-le-01 | 1 < n ⊦ m ≤ m / (* n) ↔ m = 0 | A User Theorem |
| div-mult | ⊦ m ≠ 0 → (m * m0) / m = m0 | A User Theorem |
| div-one | ⊦ m ≠ 0 → 1 / (m + 1) = 0 | A User Theorem |
| div-succ | n ≠ 0 ⊦ m % n + 1 = n → (m + 1) / n = m / n + 1 | A User Theorem |
| div-succ-01 | n ≠ 0 ⊦ m % n + 1 ≠ n → (m + 1) / n = m / n | A User Theorem |
| div-two-add | ⊦ m / 2 + n = (m + 2 * n) / 2 | A User Theorem |
| div-two-mult | ⊦ m % 2 = 1 → 2 * m / 2 = m - 1 | A User Theorem |
| exmult | ⊦ m % n = 0 ∧ n ≠ 0 → (∃ n0. m = n * n0) | A User Theorem |
| le | n ≠ 0 ⊦ m ≤ m0 → m / n ≤ m0 / n | A User Theorem |
| le-01 | n ≠ 0 ⊦ ¬ (n0 + n) / n ≤ n0 / n | A User Theorem |
| le-div-to-mult | m0 ≠ 0 ⊦ n ≤ m / m0 ↔ n * m0 ≤ m | A User Theorem |
| le-succ | n ≠ 0 ⊦ m / (n + 1) ≤ m / n | A User Theorem |
| ls | n ≠ 0, m / n < m / n0 ⊦ n0 < n | A User Theorem |
| ls-01 | n ≠ 0, m0 ≤ m, n ≤ n0 ⊦ m0 / n0 ≤ m / n | A User Theorem |
| ls-02 | n ≠ 0 ⊦ m / n < m0 / n → m < m0 | A User Theorem |
| ls-03 | n ≠ 0 ⊦ ¬ n0 / n + 1 < (n0 + n) / n | A User Theorem |
| ls-even | ⊦ m % 2 = 0 ∧ n % 2 = 0 → (m / 2 < n / 2 ↔ m < n) | A User Theorem |
| ls-succ | n ≠ 0 ⊦ ¬ m / n < m / (n + 1) | A User Theorem |
| mod-add | ⊦ m0 % n = 0 ∧ 0 ≠ n → (m + m0) % n = m % n | A User Theorem |
| mod-by6 | ⊦ (n * (n + 1) * (2 * n + 1)) % 6 = 0 | A User Theorem |
| mod-eq | ⊦ m < n → m % n = m | A User Theorem |
| mod-eq-01 | ⊦ m0 < n ∧ n ≠ 0 → ((m + m0) % n = m0 ↔ m % n = 0) | A User Theorem |
| mod-eq-02 | m0 < n, n ≠ 0 ⊦ (m + (* m0)) % (* n) = m0 ↔ m % n = 0 | A User Theorem |
| mod-le | n ≠ 0 ⊦ m % n ≤ m | A User Theorem |
| mod-le-01 | n ≠ 0 ⊦ m % n ≤ m + m0 | A User Theorem |
| mod-le-02 | n ≠ 0 ⊦ m % n ≤ n | A User Theorem |
| mod-le-03 | n ≠ 0 ⊦ ¬ n ≤ m % n | A User Theorem |
| mod-le-04 | ⊦ n ≠ 0 → (m ≤ m % n ↔ m < n) | A User Theorem |
| mod-ls | n ≠ 0 ⊦ m % n < n | A User Theorem |
| mod-ls-01 | n ≠ 0 ⊦ ¬ m < m % n | A User Theorem |
| mod-ls-02 | n ≠ 0 ⊦ ¬ m + m0 < m % n | A User Theorem |
| mod-ls-03 | n ≠ 0 ⊦ ¬ n < m % n | A User Theorem |
| mod-mod | ⊦ m % n = 0 ∧ n % n0 = 0 ∧ n ≠ 0 ∧ n0 ≠ 0 → m % n0 = 0 | A User Theorem |
| mod-mod-01 | ⊦ m % (n + 1) = 0 ∧ (n + 1) % n0 = 0 ∧ n0 ≠ 0 → m % n0 = 0 | A User Theorem |
| mod-mult | n ≠ 0 ⊦ (m + n0 * n) % n = m % n | A User Theorem |
| mod-mult-01 | n ≠ 0 ⊦ (m * n) % n = 0 | A User Theorem |
| mod-neq | n ≠ 0 ⊦ m % n < (m + 1) % n ↔ (m + 1) % n ≠ 0 | A User Theorem |
| mod-nls | ⊦ n ≠ 0 ∧ n ≤ n0 + 1 → ¬ n0 < m % n | A User Theorem |
| mod-once | n ≠ 0 ⊦ (m + n) % n = m % n | A User Theorem |
| mod-one | ⊦ m % 1 = 0 | A User Theorem |
| mod-one-01 | ⊦ n ≠ 0 ∧ n ≠ 1 → 1 % n = 1 | A User Theorem |
| mod-rec | n ≠ 0 ⊦ n ≤ m → m % n = (m - n) % n | A User Theorem |
| mod-rew | ⊦ n ≠ 0 → m % n = m - m / n * n | A User Theorem |
| mod-same | n ≠ 0 ⊦ m % n ≠ n | A User Theorem |
| mod-succ | ⊦ m % n + 1 = n → (m + 1) % n = 0 | A User Theorem |
| mod-succ-01 | n ≠ 0 ⊦ m % n + 1 ≠ n → (m + 1) % n = m % n + 1 | A User Theorem |
| mod-succ-02 | n ≠ 0 ⊦ (m + 1) % n = 0 → m % n = n - 1 | A User Theorem |
| mod-succ-03 | ⊦ 1 ≠ n ∧ n ≠ 0 → (n + 1) % n = 1 | A User Theorem |
| mod-succ-04 | n ≠ 0 ⊦ (m + 1) % n < m % n ↔ (m + 1) % n = 0 ∧ n ≠ 1 | A User Theorem |
| mod-succ-05 | n ≠ 0 ⊦ m % n < m0 → ¬ m0 < (m + 1) % n | A User Theorem |
| mod-succ-06 | n ≠ 0 ⊦ (m + 1) % n ≠ 0 → (m + 1) % n = m % n + 1 | A User Theorem |
| mod-zero | n ≠ 0 ⊦ n % n = 0 | A User Theorem |
| mod-zero-01 | ⊦ m ≠ 0 → 0 % m = 0 | A User Theorem |
| mod2-succ | ⊦ (m + 1) % 2 ≠ 0 ↔ m % 2 = 0 | A User Theorem |
| modex | ⊦ n ≠ 0 → (m % n = 0 ↔ (∃ n0. m = n0 * n)) | A User Theorem |
| mult | n ≠ 0 ⊦ (n0 + m * n) / n = n0 / n + m | A User Theorem |
| mult-01 | n ≠ 0 ⊦ (m * n) / n = m | A User Theorem |
| mult-02 | n ≠ 0 ⊦ m % n = 0 → m / n * n = m | A User Theorem |
| mult-div | ⊦ n % m = 0 ∧ m ≠ 0 → m * n / m = n | A User Theorem |
| mult-ls | n ≠ 0 ⊦ m / n < n0 → m < n0 * n | A User Theorem |
| mult-ls-01 | n ≠ 0 ⊦ n0 < m / n → n0 * n < m | A User Theorem |
| nummult-eq | n ≠ 0 ⊦ (* m) * m0 = (* n) ↔ n % m = 0 ∧ m0 = n / m ∧ m ≠ 0 | A User Theorem |
| nummult-le-01 | 0 < m, n < 0 ⊦ (* m) * m0 ≤ (* n) ↔ m0 ≤ (n + 1 - m) / m | A User Theorem |
| nummult-le-03 | 0 < m, n < 0 ⊦ (* n) ≤ (* m) * m0 ↔ n / m ≤ m0 | A User Theorem |
| nummult-ls-01 | 0 < m, n < 0 ⊦ (* m) * m0 < (* n) ↔ m0 < n / m | A User Theorem |
| nummult-ls-03 | 0 < m, n < 0 ⊦ (* n) < (* m) * m0 ↔ (n + 1 - m) / m < m0 | A User Theorem |
| one | n ≠ 0 ⊦ n / n = 1 | A User Theorem |
| one-01 | ⊦ m / 1 = m | A User Theorem |
| rax | n ≠ 0, m / n * n ≤ m ⊦ m % n = m - m / n * n | A User Theorem |
| rec | n ≠ 0 ⊦ n ≤ m → m / n = (m - n) / n + 1 | A User Theorem |
| square-even | ⊦ (m * (m + 1)) % 2 = 0 | A User Theorem |
| square-even-01 | ⊦ ((m + 1) * (m + 2)) % 2 = 0 | A User Theorem |
| square-even-02 | ⊦ (m * m + m) % 2 = 0 | A User Theorem |
| square-even-03 | ⊦ ((n + 2) * n + n) % 2 = 0 | A User Theorem |
| square-inj | ⊦ ((m + n) * ((m + n) + 1)) / 2 + n = ((m0 + n0) * ((m0 + n0) + 1)) / 2 + n0 ↔ m = m0 ∧ n = n0 | A User Theorem |
| square-inject | ⊦ ((m + n) * (m + n + 1)) / 2 + n = ((m0 + n0) * (m0 + n0 + 1)) / 2 + n0 ↔ m = m0 ∧ n = n0 | A User Theorem |
| square-interval | (m * (m + 1)) / 2 ≤ (n * (n + 1)) / 2 + n0, (n * (n + 1)) / 2 + n0 < ((m + 1) * (m + 2)) / 2, n0 ≤ n ⊦ m = n | A User Theorem |
| square-ls | ⊦ ((m + 1) * (m + 2)) / 2 < ((n + 1) * (n + 2)) / 2 ↔ m < n | A User Theorem |
| square-ls-01 | ⊦ (m * (m + 1)) / 2 < ((n + 1) * (n + 2)) / 2 ↔ m < n + 1 | A User Theorem |
| square-ls-02 | ⊦ (m * (m + 1)) / 2 < (n * (n + 1)) / 2 ↔ m < n | A User Theorem |
| square-ls-03 | ⊦ m0 ≤ m ∧ m ≤ n → (m * (m + 1)) / 2 + m0 < ((n + 1) * (n + 2)) / 2 | A User Theorem |
| square-nle-01 | ⊦ (n * (n + 1)) / 2 ≤ n ↔ n < 2 | A User Theorem |
| square-nle-01-01 | ⊦ ¬ ((n + 1) * (n + 2)) / 2 ≤ n | A User Theorem |
| square-nls | ⊦ ¬ (n * (n + 1)) / 2 < n | A User Theorem |
| two-eq | ⊦ m = m / 2 ↔ m = 0 | A User Theorem |
| two-le | ⊦ m / 2 ≤ m | A User Theorem |
| two-le-01 | ⊦ m ≤ m / 2 ↔ m = 0 | A User Theorem |
| two-le-02 | ⊦ m % 2 = 0 ∧ n % 2 = 0 → (m / 2 ≤ n / 2 ↔ m ≤ n) | A User Theorem |
| two-le-03 | ⊦ m % 2 = 0 → (m / 2 ≤ n ↔ m ≤ n * 2) | A User Theorem |
| two-le-04 | ⊦ m % 2 = 0 → (n ≤ m / 2 ↔ n * 2 ≤ m) | A User Theorem |
| two-loup | ⊦ m < n → ¬ (m + n) / 2 < m | A User Theorem |
| two-loup-01 | ⊦ m < n ∧ m + 1 ≠ n → ((m + n) / 2 - 1) + 1 = (m + n) / 2 | A User Theorem |
| two-loup-02 | ⊦ m < n ∧ m + 1 ≠ n → ¬ (m + n) / 2 - 1 < m | A User Theorem |
| two-loup-03 | ⊦ m < n ∧ m + 1 ≠ n ∧ n < m → (m + n) / 2 - 1 < m | A User Theorem |
| two-loup-04 | ⊦ m < n ∧ m + 1 ≠ n → ¬ n < (m + n) / 2 - 1 | A User Theorem |
| two-loup-05 | ⊦ m < n → ¬ (m + n) / 2 + 1 < m | A User Theorem |
| two-loup-06 | ⊦ m < n → ¬ n < (m + n) / 2 | A User Theorem |
| two-loup-07 | ⊦ m < n → ¬ n + 1 < (m + n) / 2 | A User Theorem |
| two-loup-08 | ⊦ m < n ∧ n < n0 → (m + n) / 2 < n0 | A User Theorem |
| two-loup-09 | ⊦ (m + n) / 2 ≠ m ↔ ¬ ¬(m ≠ n ∧ m + 1 ≠ n) | A User Theorem |
| two-loup-10 | ⊦ m < n → ((m + n) / 2 = m ↔ m + 1 = n) | A User Theorem |
| two-loup-11 | ⊦ m < n → ((m + n) / 2 < m + 1 ↔ m + 1 = n) | A User Theorem |
| two-loup-12 | ⊦ (m + n) / 2 < n ↔ m < n | A User Theorem |
| two-loup-13 | ⊦ (m + n) / 2 < m → ¬ (m + n) / 2 < n | A User Theorem |
| two-ls | ⊦ ¬ m + 1 < m / 2 | A User Theorem |
| two-ls-01 | ⊦ m / 2 ≤ m + 1 | A User Theorem |
| two-ls-02 | ⊦ ¬ m < m / 2 | A User Theorem |
| two-ls-03 | ⊦ ¬ m / 2 < m ↔ m = 0 | A User Theorem |
| two-ls-04 | ⊦ m % 2 = 0 → (m / 2 < n ↔ m < n * 2) | A User Theorem |
| two-ls-05 | ⊦ m % 2 = 0 → (n < m / 2 ↔ n * 2 < m) | A User Theorem |
| two-mdiv2-02 | ⊦ (2 * m) / 2 = m | A User Theorem |
| two-mdiv2-03 | ⊦ (2 * m + 1) / 2 = m | A User Theorem |
| two-neq | ⊦ n ≠ 0 → m + n ≠ m / 2 | A User Theorem |
| two-neq-01 | ⊦ m / 2 ≠ m + 1 | A User Theorem |
| two-neq-02 | ⊦ m / 2 ≠ m + n + 1 | A User Theorem |
| two-odd | ⊦ (2 * m + 1) % 2 = 1 | A User Theorem |
| two-odd-01 | ⊦ m % 2 ≠ 1 ↔ m % 2 = 0 | A User Theorem |
| two-one | ⊦ 1 / 2 = 0 | A User Theorem |
| two-one-01 | ⊦ m = 1 → m / 2 = 0 | A User Theorem |
| two-padd | m < n ⊦ (m + n) / 2 < n | A User Theorem |
| two-peq | (m + n) / 2 = m, n < m ⊦ | A User Theorem |
| two-ppred | m ≠ 0 ∧ m ≠ 1 ⊦ m / 2 = (m - 2) / 2 + 1 | A User Theorem |
| two-rec | ⊦ (m + 2) / 2 = m / 2 + 1 | A User Theorem |
| two-succ | ⊦ ¬ m + 1 < (m + 1) / 2 | A User Theorem |
| two-three | ⊦ 3 / 2 = 1 | A User Theorem |
| two-two-01 | ⊦ (2 * m + n) / 2 = m + n / 2 | A User Theorem |
| two-two-02 | ⊦ 2 / 2 = 1 | A User Theorem |
| two-twosucc-02 | ⊦ (2 * m + n + 1) / 2 = m + (n + 1) / 2 | A User Theorem |
| two-zero | ⊦ 0 / 2 = 0 | A User Theorem |
| two-zero-01 | ⊦ m = 0 → m / 2 = 0 | A User Theorem |
| two-zero-01-01 | ⊦ m / 2 = 0 ↔ ¬ ¬(m = 0 ∨ m = 1) | A User Theorem |
| zero | n ≠ 0 ⊦ 0 / n = 0 | A User Theorem |
| zero-01 | ⊦ m < n → m / n = 0 | A User Theorem |