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: |
|---|---|---|
| mult-base | ⊦ m * 0 = 0 | An Axiom |
| mult-rec | ⊦ m * n +1 = m * n + m | An Axiom |
| addle | ⊦ m * n1 = m * m0 + n0 ∧ m ≠ 0 → m0 ≤ n1 | A User Theorem |
| addle-01 | ⊦ m * n1 = m * m0 + n0 ∧ m ≠ 0 → ¬ n1 < m0 | A User Theorem |
| coef-01 | ⊦ m * n + m0 * n = m1 * n + m2 * n ↔ ¬ ¬(m + m0 = m1 + m2 ∨ n = 0) | A User Theorem |
| coef-02 | ⊦ m * n + m0 * n ≤ m1 * n + m2 * n ↔ ¬ ¬(m + m0 ≤ m1 + m2 ∨ n = 0) | A User Theorem |
| coef-03 | ⊦ m * n + m0 * n < m1 * n + m2 * n ↔ ¬ ¬(m + m0 < m1 + m2 ∧ n ≠ 0) | A User Theorem |
| coef-04 | ⊦ m * n + m0 * n = m1 * n ↔ ¬ ¬(m + m0 = m1 ∨ n = 0) | A User Theorem |
| coef-05 | ⊦ m * n + m0 * n ≤ m1 * n ↔ ¬ ¬(m + m0 ≤ m1 ∨ n = 0) | A User Theorem |
| coef-06 | ⊦ m * n + m0 * n < m1 * n ↔ ¬ ¬(m + m0 < m1 ∧ n ≠ 0) | A User Theorem |
| coef-07 | ⊦ m * n ≤ m1 * n + m2 * n ↔ ¬ ¬(m ≤ m1 + m2 ∨ n = 0) | A User Theorem |
| coef-08 | ⊦ m * n < m1 * n + m2 * n ↔ ¬ ¬(m < m1 + m2 ∧ n ≠ 0) | A User Theorem |
| coef-09 | ⊦ m * n + m0 * n = m1 * n + n ↔ ¬ ¬(m + m0 = m1 + 1 ∨ n = 0) | A User Theorem |
| coef-10 | ⊦ m * n + m0 * n ≤ m1 * n + n ↔ ¬ ¬(m + m0 ≤ m1 + 1 ∨ n = 0) | A User Theorem |
| coef-11 | ⊦ m * n + m0 * n < m1 * n + n ↔ ¬ ¬(m + m0 < m1 + 1 ∧ n ≠ 0) | A User Theorem |
| coef-12 | ⊦ m * n + n ≤ m1 * n + m2 * n ↔ ¬ ¬(m + 1 ≤ m1 + m2 ∨ n = 0) | A User Theorem |
| coef-13 | ⊦ m * n + n < m1 * n + m2 * n ↔ ¬ ¬(m + 1 < m1 + m2 ∧ n ≠ 0) | A User Theorem |
| coef-14 | ⊦ m * n + m0 * n = n ↔ ¬ ¬(m + m0 = 1 ∨ n = 0) | A User Theorem |
| coef-15 | ⊦ m * n + m0 * n ≤ n ↔ ¬ ¬(m + m0 ≤ 1 ∨ n = 0) | A User Theorem |
| coef-16 | ⊦ m * n + m0 * n < n ↔ ¬ ¬(m + m0 = 0 ∧ n ≠ 0) | A User Theorem |
| coef-17 | ⊦ m * n + n = m1 * n ↔ ¬ ¬(m + 1 = m1 ∨ n = 0) | A User Theorem |
| coef-18 | ⊦ m * n + n ≤ m1 * n ↔ ¬ ¬(m + 1 ≤ m1 ∨ n = 0) | A User Theorem |
| coef-19 | ⊦ m * n + n < m1 * n ↔ ¬ ¬(m + 1 < m1 ∧ n ≠ 0) | A User Theorem |
| coef-20 | ⊦ m * n ≤ m1 * n + n ↔ ¬ ¬(m ≤ m1 + 1 ∨ n = 0) | A User Theorem |
| coef-21 | ⊦ m * n < m1 * n + n ↔ ¬ ¬(m < m1 + 1 ∧ n ≠ 0) | A User Theorem |
| coef-22 | ⊦ n ≤ m1 * n + m2 * n ↔ ¬ ¬(1 ≤ m1 + m2 ∨ n = 0) | A User Theorem |
| coef-23 | ⊦ n < m1 * n + m2 * n ↔ ¬ ¬(1 < m1 + m2 ∧ n ≠ 0) | A User Theorem |
| dist | ⊦ m0 * (m + n) = m0 * m + m0 * n | A User Theorem |
| dist-merge | ⊦ m0 * m + m0 * n = m0 * (m + n) | A User Theorem |
| dist-sub | ⊦ m0 ≤ m → (m - m0) * n = m * n - m0 * n | A User Theorem |
| dist-sub-01 | ⊦ m ≠ 0 → m * n - n = (m - 1) * n | A User Theorem |
| dist-sub-02 | ⊦ n * n0 ≤ m + n ∧ n0 ≠ 0 → m + n - n * n0 = m - (n0 - 1) * n | A User Theorem |
| dist-sub-03 | ⊦ n0 < n → n * m - n0 * m = (n - n0) * m | A User Theorem |
| dist-sub-04 | ⊦ n0 ≤ n → n * m - n0 * m = (n - n0) * m | A User Theorem |
| eq | ⊦ m0 ≠ 0 → (m * m0 = n * m0 ↔ m = n) | A User Theorem |
| eq-01 | ⊦ m * n + n = m * n0 + n0 ↔ n = n0 | A User Theorem |
| eq-same | ⊦ m * n = m ↔ ¬ ¬(m = 0 ∨ n = 1) | A User Theorem |
| ex-two | ⊦ (∃ n. m = 2 * n) ∨ (∃ n. m = 2 * n + 1) | A User Theorem |
| four | ⊦ m ≠ 3 ∧ m ≠ 2 ∧ m ≠ 1 ∧ m ≠ 0 → (m ≤ 4 ↔ m = 4) | A User Theorem |
| four-01 | ⊦ m ≠ 2 ∧ m ≠ 1 ∧ m ≠ 0 → (m < 4 ↔ m = 3) | A User Theorem |
| le | ⊦ m0 ≠ 0 → (m0 * m ≤ m0 * n ↔ m ≤ n) | A User Theorem |
| le-01 | ⊦ m0 ≠ 0 → m ≤ m * m0 + n | A User Theorem |
| le-02 | ⊦ m0 ≠ 0 → m ≤ m * m0 | A User Theorem |
| le-03 | ⊦ m * n + n ≤ m * n0 + n0 ↔ n ≤ n0 | A User Theorem |
| le-04 | ⊦ m ≤ n → (n * n0 ≤ m ↔ n0 = 0 ∨ n0 = 1 ∧ m = n ∨ n = 0) | A User Theorem |
| le-05 | ⊦ m < n → (n * n0 ≤ m ↔ n0 = 0) | A User Theorem |
| le-num | 0 ≠ m ⊦ (* m) * n ≤ m * n0 ↔ n ≤ n0 | A User Theorem |
| le-rew | ⊦ n * m ≤ m * n0 ↔ m = 0 ∨ n ≤ n0 | A User Theorem |
| le-same | ⊦ m * n + n0 ≤ m ↔ n = 0 ∧ n0 ≤ m ∨ m = 0 ∧ n0 = 0 ∨ n = 1 ∧ n0 = 0 | A User Theorem |
| le-succ | ⊦ m * n ≤ m + 1 ↔ m = 0 ∨ m = 1 ∧ n ≤ 2 ∨ 2 ≤ m ∧ n < 2 | A User Theorem |
| le2-02 | ⊦ 2 * n ≤ 1 ↔ n = 0 | A User Theorem |
| le2-03 | ⊦ 1 ≤ 2 * n ↔ n ≠ 0 | A User Theorem |
| le2-04 | ⊦ 2 * n ≤ 2 * m + 1 ↔ n ≤ m | A User Theorem |
| leone | ⊦ n ≠ 0 → (m * n ≤ n ↔ m ≤ 1) | A User Theorem |
| ls | ⊦ m0 * m < m0 * n ↔ m0 ≠ 0 ∧ m < n | A User Theorem |
| ls-01 | ⊦ m0 * m < m ↔ m0 = 0 ∧ m ≠ 0 | A User Theorem |
| ls-02 | ⊦ m0 ≠ 0 → (m0 * m < m0 * n ↔ m < n) | A User Theorem |
| ls-03 | ⊦ m ≤ n ∧ m ≠ 0 → (n * n0 < m ↔ n0 = 0) | A User Theorem |
| ls-03-num | m ≤ n, m ≠ 0 ⊦ (* n) * n0 < (* m) ↔ n0 = 0 | A User Theorem |
| ls-04 | ⊦ m0 ≠ 0 → (m0 < m0 * m ↔ 1 < m) | A User Theorem |
| ls-05 | ⊦ m0 ≠ 0 ∧ m < n → m < n * m0 | A User Theorem |
| ls-06 | ⊦ m < m0 ∧ n < n0 → m * n < m0 * n0 | A User Theorem |
| ls-07 | ⊦ n0 < n → (n < m * n ↔ 1 < m) | A User Theorem |
| ls-08 | ⊦ m * n + n0 < n ↔ m = 0 ∧ n0 < n | A User Theorem |
| ls-09 | ⊦ m ≤ n ∧ m ≠ 0 → (m ≤ n * n0 ↔ n0 ≠ 0) | A User Theorem |
| ls-10 | ⊦ m ≤ n ∧ n0 ≠ 0 → ¬ n * n0 < m | A User Theorem |
| ls2-02 | ⊦ 2 * n < 1 ↔ n = 0 | A User Theorem |
| ls2-03 | ⊦ 1 < 2 * n ↔ n ≠ 0 | A User Theorem |
| lssucc | ⊦ (m + 1) * n < m * n + n0 ↔ n < n0 | A User Theorem |
| lssucc-01 | ⊦ m + n < (m0 + 1) * n ↔ m < m0 * n | A User Theorem |
| mod-ls | ⊦ m0 < m ∧ n ≤ n0 ∧ n2 < n0 ∧ n1 < n → m0 * n + n1 < m * n0 + n2 | A User Theorem |
| mod-neq | ⊦ m0 < m ∧ n0 < n ∧ n1 ≤ n → m0 * n + n0 ≠ m * n + m + n1 | A User Theorem |
| mod-neq-01 | ⊦ m0 < m ∧ n ≤ n0 ∧ n2 < n0 ∧ n1 < n → m0 * n + n1 ≠ m * n0 + n2 | A User Theorem |
| mod-neq-02 | ⊦ n0 < n ∧ n0 ≠ 0 → m * n ≠ m0 * n + n0 | A User Theorem |
| mod-neq-03 | ⊦ n1 < n0 ∧ n0 < n ∧ n1 ≠ 0 → m0 * n + n0 + 1 ≠ m * n + n1 | A User Theorem |
| mod-neq-04 | ⊦ n1 < n ∧ n0 < n ∧ n0 ≠ n1 → m0 * n + n0 ≠ m * n + n1 | A User Theorem |
| mod-neq-05 | ⊦ n ≠ 0 → m * n + m ≠ m0 * n + m0 + n | A User Theorem |
| mod-nle | ⊦ m0 < m ∧ n ≤ n0 ∧ n2 < n0 ∧ n1 < n → ¬ m * n0 + n2 ≤ m0 * n + n1 | A User Theorem |
| mod-nle-01 | ⊦ n0 < m0 ∧ n ≤ m ∧ n0 ≠ 0 → ¬ m0 * m + n0 ≤ m0 * n | A User Theorem |
| mod-nls | ⊦ m0 < m ∧ n ≤ n0 ∧ n2 < n0 ∧ n1 < n → ¬ m * n0 + n2 < m0 * n + n1 | A User Theorem |
| modeq | ⊦ n0 < n ∧ n1 < n → (m * n + n0 = m0 * n + n1 ↔ m = m0 ∧ n0 = n1) | A User Theorem |
| modeq-01 | ⊦ n0 < n → (m * n + n0 = m0 * n ↔ m = m0 ∧ n0 = 0) | A User Theorem |
| modls | ⊦ n0 < m0 → (m0 * m + n0 < m0 * n ↔ m < n) | A User Theorem |
| modls-01 | ⊦ n ≤ n0 ∧ n2 < n0 ∧ m1 < m ∧ n1 < n → m1 * n + n1 < m * n0 + n2 | A User Theorem |
| modls-02 | ⊦ n < n0 ∧ n2 < n0 ∧ m1 < m ∧ n1 < n → m1 * n + n1 < m * n0 + n2 | A User Theorem |
| modls-03 | ⊦ n2 < n ∧ m1 < m ∧ n1 < n → m1 * n + n1 < m * n + n2 | A User Theorem |
| modp | n0 < m0, m0 * n ≤ m0 * m + n0 ⊦ n ≤ m | A User Theorem |
| mult-a | ⊦ m0 * m * n = (m0 * m) * n | A User Theorem |
| mult-c | ⊦ m * n = n * m | A User Theorem |
| mult-eq-succ | ⊦ m < m1 → (m + 1 = m1 * m0 ↔ m0 = 1 ∧ m1 = m + 1) | A User Theorem |
| mult-eq-succ-01 | ⊦ m ≤ m1 → (m + 1 = m1 * m0 ↔ m0 = 1 ∧ m1 = m + 1 ∨ m = 1 ∧ m0 = 2 ∧ m1 = 1) | A User Theorem |
| mult-eq-succ-02 | ⊦ m1 + 1 = m1 * m0 ↔ m1 = 1 ∧ m0 = 2 | A User Theorem |
| mult-ineq-le | ⊦ n0 ≠ 0 → (n ≤ m ↔ n * n0 ≤ m * n0) | A User Theorem |
| mult-ineq-lt | ⊦ n0 ≠ 0 → (n < m ↔ n * n0 < m * n0) | A User Theorem |
| mult-le | ⊦ m1 * m0 ≤ m1 ↔ m1 = 0 ∨ m0 ≤ 1 | A User Theorem |
| mult-le-01 | ⊦ m ≤ n → (n * n ≤ m + 1 ↔ n ≤ 1 ∧ m ≤ 1) | A User Theorem |
| mult-sub-less | ⊦ m ≤ n0 → n * (n0 - m) = n0 * n - m * n | A User Theorem |
| neqone | ⊦ 1 < n → (m = m * n ↔ m = 0) | A User Theorem |
| nonumsimp-addls-01 | ⊦ m * m0 + n0 < m * (n + m0) ↔ n0 < m * n | A User Theorem |
| nonumsimp-eqsucc | ⊦ m + n = m0 + (n0 + 1) * n ↔ m = m0 + n0 * n | A User Theorem |
| nonumsimp-lstwo | ⊦ n0 + n < (m + 2) * n ↔ n0 < (m + 1) * n | A User Theorem |
| nonumsimp-mod-neq | ⊦ m0 < m ∧ n0 < n ∧ n1 ≤ n → m0 * n + n0 ≠ m * (n + 1) + n1 | A User Theorem |
| nonumsimp-mod-neq-05 | ⊦ n ≠ 0 → m * (n + 1) ≠ m0 * (n + 1) + n | A User Theorem |
| nonumsimp-succ | ⊦ m0 * m + m = (m0 + 1) * m | A User Theorem |
| nonumsimp-twoeq | ⊦ 2 * m + n = m + n0 ↔ m + n = n0 | A User Theorem |
| nonumsimp-twoeq-01 | ⊦ 2 * m + n = m ↔ m + n = 0 | A User Theorem |
| nonumsimp-twole | ⊦ 2 * m + n ≤ m ↔ m = 0 ∧ n = 0 | A User Theorem |
| nonumsimp-twols | ⊦ 2 * (m + 1) + n < 2 * m + n0 ↔ n + 2 < n0 | A User Theorem |
| nonumsimp-twonle | ⊦ m < n ∧ m0 ≤ n → ¬ 2 * n ≤ m + m0 | A User Theorem |
| numeral-01 | m1 < m2 ⊦ (* m2) * m + n = (* m1) * m + n0 ↔ (m2 - m1) * m + n = n0 | A User Theorem |
| numeral-03 | m1 < m2 ⊦ (* m2) * m + n ≤ (* m1) * m + n0 ↔ (m2 - m1) * m + n ≤ n0 | A User Theorem |
| numeral-04 | m2 < m1 ⊦ (* m2) * m + n ≤ (* m1) * m + n0 ↔ n ≤ (m1 - m2) * m + n0 | A User Theorem |
| numeral-05 | m1 < m2 ⊦ (* m2) * m + n < (* m1) * m + n0 ↔ (m2 - m1) * m + n < n0 | A User Theorem |
| numeral-06 | m2 < m1 ⊦ (* m2) * m + n < (* m1) * m + n0 ↔ n < (m1 - m2) * m + n0 | A User Theorem |
| numeral-07 | m1 < m2 ⊦ (* m2) * m = (* m1) * m + n0 ↔ (m2 - m1) * m = n0 | A User Theorem |
| numeral-08 | m2 < m1 ⊦ (* m2) * m = (* m1) * m + n0 ↔ (m1 - m2) * m + n0 = 0 | A User Theorem |
| numeral-09 | m1 < m2 ⊦ (* m2) * m ≤ (* m1) * m + n0 ↔ (m2 - m1) * m ≤ n0 | A User Theorem |
| numeral-10 | m2 < m1 ⊦ (* m2) * m ≤ (* m1) * m + n0 | A User Theorem |
| numeral-11 | m1 < m2 ⊦ (* m2) * m < (* m1) * m + n0 ↔ (m2 - m1) * m < n0 | A User Theorem |
| numeral-12 | m2 < m1 ⊦ (* m2) * m < (* m1) * m + n0 ↔ (m1 - m2) * m + n0 ≠ 0 | A User Theorem |
| numeral-15 | m1 < m2 ⊦ (* m2) * m + n ≤ (* m1) * m ↔ (m2 - m1) * m + n ≤ 0 | A User Theorem |
| numeral-16 | m2 < m1 ⊦ (* m2) * m + n ≤ (* m1) * m ↔ n ≤ (m1 - m2) * m | A User Theorem |
| numeral-17 | m1 < m2 ⊦ ¬ (* m2) * m + n < (* m1) * m | A User Theorem |
| numeral-18 | m2 < m1 ⊦ (* m2) * m + n < (* m1) * m ↔ n < (m1 - m2) * m | A User Theorem |
| numeral-19 | m2 ≠ 0 ⊦ (* m2) * m + n = m + n0 ↔ (m2 - 1) * m + n = n0 | A User Theorem |
| numeral-20 | m2 ≠ 0 ⊦ (* m2) * m + n ≤ m + n0 ↔ (m2 - 1) * m + n ≤ n0 | A User Theorem |
| numeral-21 | m2 ≠ 0 ⊦ (* m2) * m + n < m + n0 ↔ (m2 - 1) * m + n < n0 | A User Theorem |
| numeral-23 | m1 ≠ 0 ⊦ m + n ≤ (* m1) * m + n0 ↔ n ≤ (m1 - 1) * m + n0 | A User Theorem |
| numeral-24 | m1 ≠ 0 ⊦ m + n < (* m1) * m + n0 ↔ n < (m1 - 1) * m + n0 | A User Theorem |
| numeral-25 | m2 ≠ 0 ⊦ (* m2) * m = m + n0 ↔ (m2 - 1) * m = n0 | A User Theorem |
| numeral-26 | m2 ≠ 0 ⊦ (* m2) * m ≤ m + n0 ↔ (m2 - 1) * m ≤ n0 | A User Theorem |
| numeral-27 | m2 ≠ 0 ⊦ (* m2) * m < m + n0 ↔ (m2 - 1) * m < n0 | A User Theorem |
| numeral-28 | m1 ≠ 0 ⊦ m = (* m1) * m + n0 ↔ 0 = (m1 - 1) * m + n0 | A User Theorem |
| numeral-29 | m1 ≠ 0 ⊦ m ≤ (* m1) * m + n0 | A User Theorem |
| numeral-30 | m1 ≠ 0 ⊦ m < (* m1) * m + n0 ↔ (m1 - 1) * m + n0 ≠ 0 | A User Theorem |
| numeral-32 | m2 ≠ 0 ⊦ (* m2) * m + n ≤ m ↔ (m2 - 1) * m + n = 0 | A User Theorem |
| numeral-33 | m2 ≠ 0 ⊦ ¬ (* m2) * m + n < m | A User Theorem |
| numeral-35 | m1 ≠ 0 ⊦ m + n ≤ (* m1) * m ↔ n ≤ (m1 - 1) * m | A User Theorem |
| numeral-36 | m1 ≠ 0 ⊦ m + n < (* m1) * m ↔ n < (m1 - 1) * m | A User Theorem |
| one | ⊦ m0 * 1 = m0 | A User Theorem |
| one-01 | ⊦ m0 * m = 1 ↔ m0 = 1 ∧ m = 1 | A User Theorem |
| one-02 | ⊦ m0 ≠ 1 → (m0 * m = m ↔ m = 0) | A User Theorem |
| rdist | ⊦ m0 * (* m) + m0 * (* n) = m0 * (m + n) | A User Theorem |
| rsucc | ⊦ m +1 * n = m * n + n | A User Theorem |
| rsucc-01 | ⊦ (m + 1) * n = m * n + n | A User Theorem |
| rsucc-02 | ⊦ m * (n + 1) = m * n + m | A User Theorem |
| sqle | ⊦ m0 ≠ 0 ∧ m * m ≤ m0 + 1 → m ≤ m0 * m0 | A User Theorem |
| sqle-01 | ⊦ m * m ≤ n → m ≤ n | A User Theorem |
| sqle-02 | ⊦ m * m ≤ n ∧ n ≤ n0 → m ≤ n0 | A User Theorem |
| sqls | ⊦ m ≤ n → (m + 1 < n * n ↔ 1 < n) | A User Theorem |
| sqp | m0 ≠ 0, m0 ≠ 1, m0 * m0 ≤ m + 1 ⊦ m0 < m | A User Theorem |
| sqr | ⊦ m ≤ m * m | A User Theorem |
| sqr-01 | ⊦ m < m * m ↔ 1 < m | A User Theorem |
| sqr-02 | ⊦ m + 1 ≤ m * m ↔ 1 < m | A User Theorem |
| sqr-03 | ⊦ m + 1 < m * m ↔ 1 < m | A User Theorem |
| sqr-05 | ⊦ ¬ m * m < m | A User Theorem |
| sqr-06 | ⊦ m * m ≤ m ↔ m ≤ 1 | A User Theorem |
| sqr-07 | ⊦ m * m ≤ m + 1 ↔ m ≤ 1 | A User Theorem |
| sqr-08 | ⊦ m * m ≤ 2 ↔ m ≤ 1 | A User Theorem |
| sqr-09 | ⊦ 2 < m ∧ m ≤ n → ¬ n * n ≤ m + 1 | A User Theorem |
| square-eq | ⊦ m * (m + 1) = n * (n + 1) ↔ m = n | A User Theorem |
| square-eq-01 | ⊦ m * (m + 1) = (n + 1) * (n + 2) ↔ m = n + 1 | A User Theorem |
| square-eq-02 | ⊦ m * (m + 2) = n * (n + 2) ↔ m = n | A User Theorem |
| square-eq-03 | ⊦ m * (m + m0) = n * (n + m0) ↔ m = n | A User Theorem |
| square-even | ⊦ m * (m + 1) ≠ 2 * n + 1 | A User Theorem |
| square-even-01 | ⊦ m * m + m ≠ 2 * n + 1 | A User Theorem |
| square-inject | m * (m + 1) + 2 * m0 = n * (n + 1) + 2 * n0, m0 ≤ m, n0 ≤ n ⊦ m = n ∧ m0 = n0 | A User Theorem |
| square-interval | m * (m + 1) ≤ n * (n + 1) + 2 * n0, n * (n + 1) + 2 * n0 < (m + 1) * (m + 2), n0 ≤ n ⊦ m = n | A User Theorem |
| square-le | ⊦ m * (m + 1) ≤ n * (n + 1) ↔ m ≤ n | A User Theorem |
| square-le-01 | ⊦ m * (m + 1) ≤ (n + 1) * (n + 2) ↔ m ≤ n + 1 | A User Theorem |
| square-le-02 | ⊦ m * m ≤ n * n ↔ m ≤ n | A User Theorem |
| square-le-03 | ⊦ m * (m + m0) ≤ n * (n + m0) ↔ m ≤ n | A User Theorem |
| square-less | ⊦ m * m < n * n ↔ m < n | A User Theorem |
| square-ls | ⊦ m * (m + 1) < n * (n + 1) ↔ m < n | A User Theorem |
| square-ls-01 | ⊦ m ≠ 0 → ¬ m * (m + 1) < 2 | A User Theorem |
| square-ls-02 | ⊦ m * (m + 1) < (n + 1) * (n + 2) ↔ m < n + 1 | A User Theorem |
| square-ls-03 | ⊦ m * (m + 2) < n * (n + 2) ↔ m < n | A User Theorem |
| square-ls-04 | ⊦ m0 ≤ 2 * m → (m * m + m0 < n * n ↔ m < n) | A User Theorem |
| square-ls-05 | ⊦ m * (m + m0) < n * (n + m0) ↔ m < n | A User Theorem |
| square-one | ⊦ m * m + m ≠ 1 | A User Theorem |
| square-two | ⊦ m ≤ n → (n * n + n = m * 2 ↔ ¬ ¬(n = m ∧ n < 2)) | A User Theorem |
| sqzero | ⊦ m * m = 0 ↔ m = 0 | A User Theorem |
| succ | ⊦ (* m0) * m + m = (m0 + 1) * m | A User Theorem |
| succ-01 | ⊦ m ≠ 1 → m * n0 ≠ m * m0 + 1 | A User Theorem |
| succ-merge | ⊦ m * n + m = m * (n + 1) | A User Theorem |
| three | ⊦ m ≠ 1 → (m * m0 = 3 ↔ m = 3 ∧ m0 = 1) | A User Theorem |
| threeeq | ⊦ 3 ≠ 2 * n | A User Theorem |
| threels | ⊦ 3 < 2 * n ↔ 1 < n | A User Theorem |
| two-02 | ⊦ m + m = 2 * m | A User Theorem |
| two-03 | ⊦ m ≠ 1 → (m * m0 = 2 ↔ m = 2 ∧ m0 = 1) | A User Theorem |
| two-les-01 | ⊦ n ≤ 2 * n + 1 | A User Theorem |
| two-ls-01 | ⊦ 2 * m < 2 * n ↔ m < n | A User Theorem |
| two-one-01 | ⊦ 2 * m ≠ 1 | A User Theorem |
| two-succ-03 | ⊦ 2 * (m + 1) = n + 1 ↔ 2 * m + 1 = n | A User Theorem |
| two-succ-04 | ⊦ 2 * m + 1 < 2 * n ↔ m < n | A User Theorem |
| two-succ-05 | ⊦ 2 * m ≠ 2 * n + 1 | A User Theorem |
| two-succ-06 | ⊦ 2 * m = 2 * n + m0 → ¬ m < n | A User Theorem |
| two-zero-01 | ⊦ 2 * m = 0 ↔ m = 0 | A User Theorem |
| twoeq | ⊦ 2 = 2 * n ↔ n = 1 | A User Theorem |
| twoeqf | ⊦ m + m0 = 2 * n ∧ n < m → m0 < n | A User Theorem |
| twoeqf-01 | ⊦ m + m0 = 2 * n ∧ m < n → n < m0 | A User Theorem |
| twoeqf-02 | ⊦ m + m0 = 2 * n + 1 ∧ n < m → m0 ≤ n | A User Theorem |
| twoeqf-03 | ⊦ m + m0 = 2 * n + 1 ∧ m < n → n + 1 < m0 | A User Theorem |
| twole | ⊦ 2 * n ≤ n ↔ n = 0 | A User Theorem |
| twole-01 | ⊦ 2 ≤ 2 * n ↔ n ≠ 0 | A User Theorem |
| twole-02 | ⊦ m ≤ 2 * m | A User Theorem |
| twols | ⊦ ¬ 2 * n < n | A User Theorem |
| twols-01 | ⊦ 2 < 2 * n ↔ 1 < n | A User Theorem |
| zero | ⊦ 0 * n = 0 | A User Theorem |
| zero-01 | ⊦ m0 * m = 0 ↔ m0 = 0 ∨ m = 0 | A User Theorem |
| zero-02 | ⊦ m * n = m * n0 ↔ m = 0 ∨ n = n0 | A User Theorem |
| zero-03 | ⊦ m * n = m ↔ m = 0 ∨ n = 1 | A User Theorem |
| zero-04 | ⊦ m * n = m0 → (m0 = m * n0 ↔ m = 0 ∨ n = n0) | A User Theorem |
| zero-05 | ⊦ (m + 1) * n = 0 ↔ n = 0 | A User Theorem |
| zero-06 | ⊦ m ≠ 0 → (m * n = 0 ↔ n = 0) | A User Theorem |
| zero-num | 0 ≠ m ⊦ (* m) * n = 0 ↔ n = 0 | A User Theorem |