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-succ | ⊦ i * j +1 = i * j + i | An Axiom |
| Mult-zero | ⊦ i * 0 = 0 | An Axiom |
| Mult-pred | ⊦ i * j -1 = i * j - i | An Axiom |
| 5-not-even | ⊦ 5 ≠ 2 * i | A User Theorem |
| 7-not-even | ⊦ 7 ≠ 2 * i | A User Theorem |
| abs-eqall | ⊦ abs(i * j) = abs(i) * abs(j) | A User Theorem |
| abs-eqneg | ⊦ j < 0 ∧ i < 0 → abs(i) * abs(j) = i * j | A User Theorem |
| abs-ls | ⊦ j < 0 ∧ i < 0 ∧ j < j0 ∧ j0 < 0 → abs(j0) < i * j | A User Theorem |
| abs-ls-same | ⊦ abs(i) * abs(j) < i ↔ 0 < i ∧ j = 0 | A User Theorem |
| abs-ls-same-01 | ⊦ abs(i) * j < i ↔ 0 < i ∧ j ≤ 0 ∨ i < 0 ∧ j < ~1 | A User Theorem |
| abs-not-neg | ⊦ ¬ abs(i) * abs(j) < 0 | A User Theorem |
| add-mult-two | ⊦ i + i = 2 * i | A User Theorem |
| associativity | ⊦ i * j * j0 = (i * j) * j0 | A User Theorem |
| auxexdivmod | i0 * j ≤ i, i < (i0 + i1) * j, 0 ≤ i0, 0 < j, 0 ≤ i, 0 ≤ i1 ⊦ ∃ i0. i0 * j ≤ i ∧ i < (i0 + 1) * j ∧ 0 ≤ i0 | A User Theorem |
| auxexdivmod-01 | 0 < j, 0 ≤ i ⊦ ∃ i0. i0 * j ≤ i ∧ i < (i0 + 1) * j ∧ 0 ≤ i0 | A User Theorem |
| commutativity | ⊦ i * j = j * i | A User Theorem |
| dist-lsplit | ⊦ (i + i0) * j = i * j + i0 * j | A User Theorem |
| dist-rmerge | ⊦ i * j + i * j0 = i * (j + j0) | A User Theorem |
| dist-rsplit | ⊦ i * (j + j0) = i * j + i * j0 | A User Theorem |
| dist-sub-merge | ⊦ i * j - i * j0 = i * (j - j0) | A User Theorem |
| dist-sub-split | ⊦ (i - j) * j0 = i * j0 - j * j0 | A User Theorem |
| eq-dist | ⊦ (i + j) * i0 = j0 + j * i0 ↔ i * i0 = j0 | A User Theorem |
| eq-neg | ⊦ i < 0 → (i * j = i * j0 ↔ j = j0) | A User Theorem |
| eq-nonzero | ⊦ i ≠ 0 → (i * j = i * j0 ↔ j = j0) | A User Theorem |
| eq-nonzero-01 | ⊦ i ≠ 0 → (j * i = j0 * i ↔ j = j0) | A User Theorem |
| eq-nonzero-02 | ⊦ i ≠ 0 → (i * j = j0 * i ↔ j = j0) | A User Theorem |
| eq-nonzero-03 | ⊦ i ≠ 0 → (j * i = i * j0 ↔ j = j0) | A User Theorem |
| eq-one | ⊦ i * j = 1 ↔ abs(i) = 1 ∧ i = j | A User Theorem |
| eq-one-neg | ⊦ i * j = ~1 ↔ abs(i) = 1 ∧ i = ~ j | A User Theorem |
| eq-pos | ⊦ 0 < i → (i * j = i * j0 ↔ j = j0) | A User Theorem |
| eq-pos-01 | ⊦ 0 < j → (i * j = i0 * j ↔ i = i0) | A User Theorem |
| eq-same | ⊦ i * j = i ↔ i = 0 ∨ j = 1 | A User Theorem |
| eq-same-01 | ⊦ i ≠ 0 → (i * j = i ↔ j = 1) | A User Theorem |
| eq-same-02 | ⊦ 0 < i → (i * j = i ↔ j = 1) | A User Theorem |
| eq-same-03 | ⊦ i < 0 → (i * j = i ↔ j = 1) | A User Theorem |
| eq-succ | ⊦ i * (i0 + 1) + j = i + j0 ↔ i * i0 + j = j0 | A User Theorem |
| eq-succ-01 | ⊦ (i + i0) * j + j0 = (i + i1) * j + j1 ↔ i0 * j + j0 = i1 * j + j1 | A User Theorem |
| est-nle | ⊦ j0 ≤ j ∧ ¬ i * j0 ≤ i0 ∧ 0 ≤ i → ¬ i * j ≤ i0 | A User Theorem |
| ex-two | ⊦ (∃ j. i = 2 * j) ∨ (∃ j. i = 2 * j + 1) | A User Theorem |
| exdivmod | j ≠ 0 ⊦ ∃ i0, j0. i = i0 * j + j0 ∧ abs(j0) < abs(j) | A User Theorem |
| exdivmodpos | ⊦ 0 ≤ i ∧ 0 < j → (∃ i0, j0. i = i0 * j + j0 ∧ 0 ≤ i0 ∧ 0 ≤ j0 ∧ j0 < j) | A User Theorem |
| four | ⊦ 2 * 2 = 4 | A User Theorem |
| le-abs | ⊦ i * abs(j) ≤ i0 * abs(j) ↔ ¬ ¬(j = 0 ∨ i ≤ i0) | A User Theorem |
| le-dist | ⊦ i * (j + i0) ≤ i * (j0 + i0) + j1 ↔ i * j ≤ i * j0 + j1 | A User Theorem |
| le-dist-01 | ⊦ i * (j + i0) + j1 ≤ i * (j0 + i0) ↔ i * j + j1 ≤ i * j0 | A User Theorem |
| le-dist-02 | ⊦ i * (j + i0) + j2 ≤ i * (j0 + i0) + j1 ↔ i * j + j2 ≤ i * j0 + j1 | A User Theorem |
| le-neg | ⊦ i < 0 → (i * j ≤ i * i0 ↔ i0 ≤ j) | A User Theorem |
| le-neg-01 | ⊦ i < 0 → (j * i ≤ i0 * i ↔ i0 ≤ j) | A User Theorem |
| le-one | ⊦ 1 < j → (i * j ≤ 1 ↔ i ≤ 0) | A User Theorem |
| le-pos | ⊦ 0 < i → (i * j ≤ i * i0 ↔ j ≤ i0) | A User Theorem |
| le-pos-01 | ⊦ 0 < i → (j * i ≤ i0 * i ↔ j ≤ i0) | A User Theorem |
| le-same | ⊦ 0 < i → (i * j ≤ i ↔ j ≤ 1) | A User Theorem |
| le-same-01 | ⊦ 0 < i → (i ≤ i * j ↔ 1 ≤ j) | A User Theorem |
| le-same-02 | ⊦ i < 0 → (i * j ≤ i ↔ 1 ≤ j) | A User Theorem |
| le-same-03 | ⊦ i < 0 → (i ≤ i * j ↔ j ≤ 1) | A User Theorem |
| le-same-04 | ⊦ i * abs(j) ≤ abs(j) ↔ j = 0 ∨ i ≤ 1 | A User Theorem |
| le-same-05 | ⊦ 1 < i → (i * abs(j) ≤ abs(j) ↔ j = 0) | A User Theorem |
| le-same-06 | ⊦ 0 < j → (i * abs(j) ≤ abs(j) ↔ i ≤ 1) | A User Theorem |
| le-two | ⊦ 2 * i ≤ 2 * j + 1 ↔ i ≤ j | A User Theorem |
| ls-add | ⊦ 0 ≤ j1 ∧ j1 < j → (i0 * j + j1 < j ↔ i0 ≤ 0) | A User Theorem |
| ls-add-02 | ⊦ i * (j + j1) + i0 < i * j + j0 ↔ i * j1 + i0 < j0 | A User Theorem |
| ls-add-03 | ⊦ i * j + i0 < i * (j + j1) + j0 ↔ i0 < i * j1 + j0 | A User Theorem |
| ls-dist | ⊦ i * (j + i0) < i * (j0 + i0) + j1 ↔ i * j < i * j0 + j1 | A User Theorem |
| ls-dist-01 | ⊦ i * (j + i0) + j1 < i * (j0 + i0) ↔ i * j + j1 < i * j0 | A User Theorem |
| ls-dist-02 | ⊦ i * (j + i0) + j2 < i * (j0 + i0) + j1 ↔ i * j + j2 < i * j0 + j1 | A User Theorem |
| ls-dist-03 | ⊦ i * (j + 1) + j1 < i ↔ i * j + j1 < 0 | A User Theorem |
| ls-dist-04 | ⊦ i < i * (j + 1) + j1 ↔ 0 < i * j + j1 | A User Theorem |
| ls-dist-05 | ⊦ i * (j + 1) + j1 ≤ i ↔ i * j + j1 ≤ 0 | A User Theorem |
| ls-dist-06 | ⊦ i ≤ i * (j + 1) + j1 ↔ 0 ≤ i * j + j1 | A User Theorem |
| ls-forward | ⊦ i * j < i * j0 → i ≠ 0 | A User Theorem |
| ls-neg | ⊦ i < 0 → (i * j < i * j0 ↔ j0 < j) | A User Theorem |
| ls-pos | ⊦ 0 < i → (i * j < i * j0 ↔ j < j0) | A User Theorem |
| ls-pos-01 | ⊦ 0 < j → (i * j < i0 * j ↔ i < i0) | A User Theorem |
| ls-pos-02 | ⊦ abs(j0) < j → (i * j < i0 * j ↔ i < i0) | A User Theorem |
| ls-same | ⊦ 0 < i → (i * j < i ↔ j < 1) | A User Theorem |
| ls-same-01 | ⊦ 0 < i → (i < i * j ↔ 1 < j) | A User Theorem |
| ls-same-02 | ⊦ i < 0 → (i * j < i ↔ 1 < j) | A User Theorem |
| ls-same-03 | ⊦ i < 0 → (i < i * j ↔ j < 1) | A User Theorem |
| ls-same-04 | ⊦ 0 < i → (j * i < i ↔ j < 1) | A User Theorem |
| ls-same-05 | ⊦ 1 < i → (j * i < i ↔ j < 1) | A User Theorem |
| ls-same-06 | ⊦ i + j * j0 < j ↔ i + j * (j0 - 1) < 0 | A User Theorem |
| ls-sub | ⊦ i0 < i → ((i - i0) * j < (i - i0) * j0 ↔ j < j0) | A User Theorem |
| ls-two | ⊦ i < 0 ∧ 0 ≤ j → 2 * i < j | A User Theorem |
| ls-two-01 | ⊦ i < 0 ∧ 0 ≤ j → 2 * i ≤ j | A User Theorem |
| ls-two-02 | ⊦ i < 0 ∧ 0 < j → 2 * i < j | A User Theorem |
| ls-two-03 | ⊦ i < 0 ∧ 0 < j → 2 * i ≤ j | A User Theorem |
| minus-left | ⊦ ~ i * j = ~(i * j) | A User Theorem |
| minus-one | ⊦ i + 1 = 0 → i * j = ~ j | A User Theorem |
| minus-one-01 | ⊦ i * ~1 = ~ i | A User Theorem |
| minus-one-02 | ⊦ ~1 * i = ~ i | A User Theorem |
| mod-neq | ⊦ abs(j1) < abs(i) ∧ j1 ≠ 0 → i * j ≠ i * j0 + j1 | A User Theorem |
| mod-nle | ⊦ 0 ≤ i0 ∧ i0 < i ∧ 0 < j ∧ 0 < i → (j * i + i0 ≤ j ↔ i = 1 ∧ i0 = 0) | A User Theorem |
| mod-nls | ⊦ j < 0 ∧ 0 ≤ i0 ∧ i0 < i ∧ 0 < i → ¬ j < j * i + i0 | A User Theorem |
| modeqp | i * j + j0 = i0 * j + j1, 0 ≤ j0, j0 < j, 0 ≤ j1, j1 < j ⊦ i = i0 ∧ j0 = j1 | A User Theorem |
| modeqp-01 | i * j + j0 = i0 * j + j1, j0 ≤ 0, abs(j0) < j, j1 ≤ 0, abs(j1) < j ⊦ i = i0 ∧ j0 = j1 | A User Theorem |
| modeqp-02 | i * j + j0 = i0 * j + j1, j < 0, 0 ≤ j0, j0 < abs(j), 0 ≤ j1, j1 < abs(j) ⊦ i = i0 ∧ j0 = j1 | A User Theorem |
| modeqp-03 | i * j + j0 = i0 * j + j1, j < 0, j0 ≤ 0, j < j0, j1 ≤ 0, j < j1 ⊦ i = i0 ∧ j0 = j1 | A User Theorem |
| modeqp-copied | i * j + j0 = i0 * j + j1, 0 ≤ j0, j0 < j, 0 ≤ j1, j1 < j ⊦ i = i0 ∧ j0 = j1 | A User Theorem |
| modeqp-neg | i * i0 + j0 = i1 * j + j1, j0 < 0, abs(j0) < j, j1 < 0, abs(j1) < j, i < 0, 0 ≤ i0 ⊦ j < i0 ∨ i ≤ i1 | A User Theorem |
| modeqp-pos | i * i0 + j0 = i1 * j + j1, 0 ≤ j0, j0 < j, 0 ≤ j1, j1 < j, 0 ≤ i0, 0 ≤ i ⊦ j < i0 ∨ i1 ≤ i | A User Theorem |
| modlep | j * i ≤ j * i0 + j0, 0 ≤ j0, j0 < j ⊦ i ≤ i0 | A User Theorem |
| modlep-01 | j * i ≤ j * i0 + j0, abs(j0) < j ⊦ i ≤ i0 | A User Theorem |
| modlep-02 | j * i + j0 ≤ j * i0, abs(j0) < j ⊦ i ≤ i0 | A User Theorem |
| modlep-03 | j * i + j0 ≤ j * i0 + j1, 0 ≤ j0, j0 < j, abs(j1) < j ⊦ i ≤ i0 | A User Theorem |
| modlep-04 | j * i + j0 ≤ j * i0 + j1, j0 ≤ 0, j1 ≤ 0, abs(j0) < j, abs(j1) < j ⊦ i ≤ i0 | A User Theorem |
| modlsp | j * i < j * i0 + j0, 0 ≤ j0, j0 < j ⊦ i ≤ i0 | A User Theorem |
| modlsp-01 | j * i < j * i0 + j0, abs(j0) < j ⊦ i ≤ i0 | A User Theorem |
| modlsp-02 | j * i + j0 < j * i0, abs(j0) < j ⊦ i ≤ i0 | A User Theorem |
| modlsp-03 | j * i + j0 < j * i0 + j1, 0 ≤ j0, j0 < j, abs(j1) < j ⊦ i ≤ i0 | A User Theorem |
| modlsp-04 | j * i < j * i0 + j0, j < 0, abs(j0) < abs(j) ⊦ i0 ≤ i | A User Theorem |
| modlsp-05 | j * i + j0 < j * i0, j < 0, abs(j0) < abs(j) ⊦ i0 ≤ i | A User Theorem |
| modlsp-06 | j * i + j0 < j * i0 + j1, j < j1, j1 ≤ 0, abs(j0) < abs(j) ⊦ i0 ≤ i | A User Theorem |
| modneqp | i * i0 + j0 = i1 * j + j1, 0 ≤ j1, j1 < j, 0 ≤ j0, j0 < j, 0 ≤ i0, i0 ≤ j, 0 ≤ i, i < i1 ⊦ | A User Theorem |
| mods-eq | ⊦ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 ≤ j0 ∧ 0 ≤ j1 ∧ j0 < j ∧ j1 < j → (i * j + j0 = i0 * j + j1 ↔ i = i0 ∧ j0 = j1) | A User Theorem |
| mods-ls | ⊦ i < i0 ∧ 0 ≤ j0 ∧ j0 < j → i * j < i0 * j + j0 | A User Theorem |
| mods-ls-01 | ⊦ i < i0 ∧ abs(j0) < j → i * j < i0 * j + j0 | A User Theorem |
| mods-ls-02 | ⊦ i < i0 ∧ 0 ≤ j0 ∧ j0 < j → i * j + j0 < i0 * j | A User Theorem |
| mods-ls-03 | ⊦ i < i0 ∧ abs(j0) < j → i * j + j0 < i0 * j | A User Theorem |
| mods-ls-04 | ⊦ j0 < j ∧ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 ≤ j0 → (i * j + j0 < i0 * j ↔ i < i0) | A User Theorem |
| mods-nls | ⊦ 0 < i → ¬ i * abs(j) < j | A User Theorem |
| mods-zero-07 | ⊦ 0 ≤ i → ¬ 2 * i + 1 < 0 | A User Theorem |
| modzero | ⊦ 0 < i ∧ abs(j0) < j → ¬ i * j + j0 < 0 | A User Theorem |
| modzero-01 | ⊦ i < 0 ∧ j0 < j ∧ 0 ≤ j → i * j + j0 < 0 | A User Theorem |
| modzero-02 | ⊦ i < 0 ∧ j0 < j ∧ 0 < j → i * j + j0 < 0 | A User Theorem |
| modzero-03 | ⊦ i < 0 ∧ j0 < j ∧ 0 < j → ¬ 0 ≤ i * j + j0 | A User Theorem |
| modzero-04 | ⊦ i < 0 ∧ j < j0 ∧ j < 0 → ¬ i * j + j0 < 0 | A User Theorem |
| modzero-05 | ⊦ i < 0 ∧ j < j0 ∧ j < 0 → 0 ≤ i * j + j0 | A User Theorem |
| modzero-06 | ⊦ i < 0 ∧ j < j0 ∧ j < 0 → 0 < i * j + j0 | A User Theorem |
| modzero-07 | ⊦ j0 + j < 0 ∧ j < 0 ∧ 0 < i → ¬ 0 ≤ i * j + j0 | A User Theorem |
| modzero-08 | ⊦ 0 < i ∧ abs(j0) < j → ¬ i * j + j0 ≤ 0 | A User Theorem |
| mult-add-greater | ⊦ 0 < i ∧ 0 < j ∧ 0 < i1 → ¬ (i + j) * i1 < i * i1 | A User Theorem |
| mult-gt-both | ⊦ 0 ≤ i ∧ 0 ≤ j ∧ 0 ≤ i1 ∧ 0 ≤ j1 ∧ i < i1 ∧ j < j1 → i * j < i1 * j1 | A User Theorem |
| mult-gt-one | ⊦ 0 < i ∧ 1 < i1 → i < i1 * i | A User Theorem |
| mult-pos | ⊦ 0 ≤ i ∧ 0 < j ∧ i1 < 0 → i * i1 ≠ j | A User Theorem |
| mult-pos-pos | ⊦ 0 < i2 → (i1 * i2 = i2 ↔ i1 = 1) | A User Theorem |
| mult-sub-less | ⊦ 0 < i ∧ 0 < j ∧ 0 < i1 → (i - j) * i1 < i * i1 | A User Theorem |
| mult-sub-lesseq | ⊦ 0 < i ∧ 0 < j ∧ 0 < i1 → (i - j) * i1 ≤ i * i1 | A User Theorem |
| neq-3-not-even | ⊦ ~3 ≠ 2 * i | A User Theorem |
| neq-5-not-even | ⊦ ~5 ≠ 2 * i | A User Theorem |
| neq-7-not-even | ⊦ ~7 ≠ 2 * i | A User Theorem |
| neq-9-not-even | ⊦ ~9 ≠ 2 * i | A User Theorem |
| neq-not-zero | ⊦ i * j ≠ i * j0 → i ≠ 0 | A User Theorem |
| neq-not-zero-01 | ⊦ i ≠ i * j0 → i ≠ 0 | A User Theorem |
| neq-two | ⊦ 2 * i ≠ 1 | A User Theorem |
| noeth-ls-pos | ⊦ ∀ i0. abs(i0) < i → 0 < abs(i0) → (abs(i0) * j < abs(i0) * j0 ↔ j < j0) | A User Theorem |
| noeth-modlep | ⊦ abs(j) < j1 → abs(j) * i ≤ abs(j) * i0 + j0 ∧ 0 ≤ j0 ∧ j0 < abs(j) → i ≤ i0 | A User Theorem |
| noeth-zero-ls | abs(i) < i0, 0 < abs(i), 0 < j ⊦ 0 < abs(i) * j | A User Theorem |
| numabs | 0 ≤ j, 0 ≤ j0 ⊦ 0 ≤ i → abs(i * (* j) + (* j0)) = i * j + j0 | A User Theorem |
| numabs-01 | 0 ≤ j, 0 ≤ j0 ⊦ 0 < i → abs(i * (* j) + (* j0)) = i * j + j0 | A User Theorem |
| numdist | ⊦ i0 * (* i) + i0 * (* j) = i0 * (i + j) | A User Theorem |
| numeq | ⊦ (* i2) * i + j = (* i1) * i + j0 ↔ (i2 - i1) * i + j = j0 | A User Theorem |
| numeq-01 | ⊦ (* i2) * i = (* i1) * i + j0 ↔ (i2 - i1) * i = j0 | A User Theorem |
| numeq-02 | ⊦ (* i2) * i + j = i + j0 ↔ (i2 - 1) * i + j = j0 | A User Theorem |
| numeq-03 | ⊦ (* i2) * i = i + j0 ↔ (i2 - 1) * i = j0 | A User Theorem |
| numeq-04 | ⊦ i = (* i1) * i + j0 ↔ 0 = (i1 - 1) * i + j0 | A User Theorem |
| numle | ⊦ (* i1) * j ≤ (* i2) * j ↔ 0 ≤ (i2 - i1) * j | A User Theorem |
| numle-01 | ⊦ (* i2) * i ≤ (* i1) * i + j0 ↔ (i2 - i1) * i ≤ j0 | A User Theorem |
| numle-02 | ⊦ (* i2) * i + j ≤ (* i1) * i ↔ (i2 - i1) * i + j ≤ 0 | A User Theorem |
| numle-03 | ⊦ (* i2) * i + j ≤ i + j0 ↔ (i2 - 1) * i + j ≤ j0 | A User Theorem |
| numle-04 | ⊦ i + j ≤ (* i1) * i + j0 ↔ j ≤ (i1 - 1) * i + j0 | A User Theorem |
| numle-05 | ⊦ (* i2) * i ≤ i + j0 ↔ (i2 - 1) * i ≤ j0 | A User Theorem |
| numle-06 | ⊦ (* i2) * i + j ≤ (* i1) * i + j0 ↔ (i2 - i1) * i + j ≤ j0 | A User Theorem |
| numle-07 | ⊦ (* i1) * j ≤ j ↔ 0 ≤ (1 - i1) * j | A User Theorem |
| numle-08 | ⊦ i + j ≤ (* i1) * i ↔ j ≤ (i1 - 1) * i | A User Theorem |
| numle-09 | ⊦ j ≤ (* i1) * j ↔ 0 ≤ (i1 - 1) * j | A User Theorem |
| numle-10 | ⊦ 0 < i → ((* i) * j ≤ (* i) * j0 ↔ j ≤ j0) | A User Theorem |
| numle-11 | ⊦ i < 0 → ((* i) * j ≤ (* i) * j0 ↔ j0 ≤ j) | A User Theorem |
| numle-12 | ⊦ j ≤ (* i1) * j + i ↔ 0 ≤ (i1 - 1) * j + i | A User Theorem |
| numle-13 | ⊦ (* i1) * j + i ≤ j ↔ (i1 - 1) * j + i ≤ 0 | A User Theorem |
| numleneg | ⊦ i < 0 → (j ≤ (* i) * i0 ↔ j + ~ i * i0 ≤ 0) | A User Theorem |
| numleneg-01 | ⊦ i < 0 → ((* i) * i0 ≤ j ↔ 0 ≤ j + ~ i * i0) | A User Theorem |
| numleneg-02 | i < 0 ⊦ (* i) * i0 ≤ j ↔ 0 ≤ ~ i * i0 + j | A User Theorem |
| numleneg-03 | i < 0 ⊦ j ≤ (* i) * i0 ↔ ~ i * i0 + j ≤ 0 | A User Theorem |
| numls | ⊦ (* i1) * j < (* i2) * j ↔ 0 < (i2 - i1) * j | A User Theorem |
| numls-01 | ⊦ (* i2) * i < (* i1) * i + j0 ↔ (i2 - i1) * i < j0 | A User Theorem |
| numls-02 | ⊦ (* i2) * i + j < (* i1) * i ↔ j < (i1 - i2) * i | A User Theorem |
| numls-03 | ⊦ (* i2) * i + j < i + j0 ↔ (i2 - 1) * i + j < j0 | A User Theorem |
| numls-04 | ⊦ i + j < (* i1) * i + j0 ↔ j < (i1 - 1) * i + j0 | A User Theorem |
| numls-05 | ⊦ (* i2) * i < i + j0 ↔ (i2 - 1) * i < j0 | A User Theorem |
| numls-06 | ⊦ (* i2) * i + j < (* i1) * i + j0 ↔ (i2 - i1) * i + j < j0 | A User Theorem |
| numls-07 | ⊦ (* i1) * j < j ↔ 0 < (1 - i1) * j | A User Theorem |
| numls-08 | ⊦ i + j < (* i1) * i ↔ j < (i1 - 1) * i | A User Theorem |
| numls-09 | ⊦ j < (* i1) * j ↔ 0 < (i1 - 1) * j | A User Theorem |
| numls-10 | ⊦ 0 < i → ((* i) * j < (* i) * j0 ↔ j < j0) | A User Theorem |
| numls-11 | ⊦ i < 0 → ((* i) * j < (* i) * j0 ↔ j0 < j) | A User Theorem |
| numls-12 | ⊦ j < (* i1) * j + i ↔ 0 < (i1 - 1) * j + i | A User Theorem |
| numls-13 | ⊦ (* i1) * j + i < j ↔ (i1 - 1) * j + i < 0 | A User Theorem |
| numlsneg | ⊦ i < 0 → (j < (* i) * i0 ↔ j + ~ i * i0 < 0) | A User Theorem |
| numlsneg-01 | ⊦ i < 0 → ((* i) * i0 < j ↔ 0 < j + ~ i * i0) | A User Theorem |
| numlsneg-02 | i < 0 ⊦ (* i) * i0 < j ↔ 0 < ~ i * i0 + j | A User Theorem |
| numlsneg-03 | i < 0 ⊦ j < (* i) * i0 ↔ ~ i * i0 + j < 0 | A User Theorem |
| numsub | ⊦ i * (* j) + j0 - i = i * (j - 1) + j0 | A User Theorem |
| numsucc | ⊦ (* i0) * i + i = (i0 + 1) * i | A User Theorem |
| odd-even | ⊦ 2 * i ≠ 2 * j + 1 | A User Theorem |
| one | ⊦ 1 * i = i | A User Theorem |
| one-01 | ⊦ i = 1 → i * j = j | A User Theorem |
| ple-neg | i < 0, j < 0, i0 ≤ i, j0 < j ⊦ i * j ≤ i0 * j0 | A User Theorem |
| ple-pos | 0 < i, 0 < j, i ≤ i0, j ≤ j0 ⊦ i * j ≤ i0 * j0 | A User Theorem |
| ple-pos-better | 0 ≤ i, 0 ≤ j, i ≤ i0, j ≤ j0 ⊦ i * j ≤ i0 * j0 | A User Theorem |
| pls-neg | i < 0, j < 0, i0 ≤ i, j0 < j ⊦ i * j < i0 * j0 | A User Theorem |
| pls-pos | 0 < i, 0 < j, i ≤ i0, j < j0 ⊦ i * j < i0 * j0 | A User Theorem |
| pls-pos-01 | ⊦ i * j < j0 ∧ i0 ≤ i ∧ 0 ≤ j → i0 * j < j0 | A User Theorem |
| pls-pos-02 | ⊦ i < i0 * j ∧ j ≤ j0 ∧ 0 ≤ i0 → i < i0 * j0 | A User Theorem |
| pnle-neg | i < 0, j < 0, i0 ≤ i, j0 < j ⊦ ¬ i0 * j0 ≤ i * j | A User Theorem |
| pnle-pos | i ≤ i0, j < j0, i0 ≠ 0, 0 ≤ i, 0 ≤ j ⊦ ¬ i0 * j0 ≤ i * j | A User Theorem |
| pnls-neg | i < 0, j < 0, i0 ≤ i, j0 < j ⊦ ¬ i0 * j0 < i * j | A User Theorem |
| pnls-negpos | i ≤ i0, j0 ≤ j, 0 ≤ j0, i0 ≤ 0 ⊦ ¬ i0 * j0 < i * j | A User Theorem |
| pnls-pos | i ≤ i0, j ≤ j0, 0 ≤ i, 0 ≤ j ⊦ ¬ i0 * j0 < i * j | A User Theorem |
| pnls-posneg | i0 ≤ i, j ≤ j0, 0 ≤ i0, j0 ≤ 0 ⊦ ¬ i0 * j0 < i * j | A User Theorem |
| pred-rmerge | ⊦ i * j - i = i * (j - 1) | A User Theorem |
| pzero-gr | 0 < i ∧ 0 < j ∨ i < 0 ∧ j < 0 ⊦ 0 < i * j | A User Theorem |
| pzero-ls | 0 < i ∧ j < 0 ∨ i < 0 ∧ 0 < j ⊦ i * j < 0 | A User Theorem |
| short-mult-max | ⊦ i < 256 ∧ j ≤ 256 ∧ 0 ≤ i → ¬ 65536 ≤ i * j | A User Theorem |
| square-abs | ⊦ abs(i * i) = i * i | A User Theorem |
| square-eq | ⊦ i * i = j * j ↔ abs(i) = abs(j) | A User Theorem |
| square-eq-01 | ⊦ 0 ≤ i ∧ 0 ≤ j → (i * (i + 1) = j * (j + 1) ↔ i = j) | A User Theorem |
| square-eq-02 | ⊦ 0 ≤ i ∧ 0 ≤ j → (i * (i + 1) = (j + 1) * (j + 2) ↔ i = j + 1) | A User Theorem |
| square-even | ⊦ i * (i + 1) ≠ 2 * j + 1 | A User Theorem |
| square-ex | ⊦ 0 < i → (∃ j. 0 < j ∧ j * j ≤ i ∧ i < (j + 1) * (j + 1)) | A User Theorem |
| square-gez | ⊦ 0 ≤ i * i | A User Theorem |
| square-gez-01 | ⊦ 0 ≤ i * i + j * j | A User Theorem |
| square-gez-02 | ⊦ 0 ≤ i + i * i | A User Theorem |
| square-inject | i * (i + 1) + 2 * i0 = j * (j + 1) + 2 * j0, i0 ≤ i, j0 ≤ j, 0 ≤ i0, 0 ≤ j, 0 ≤ j0 ⊦ i = j ∧ i0 = j0 | A User Theorem |
| square-interval | i * (i + 1) ≤ j * (j + 1) + 2 * j0, j * (j + 1) + 2 * j0 < (i + 1) * (i + 2), j0 ≤ j, 0 ≤ i, 0 ≤ j0 ⊦ i = j | A User Theorem |
| square-le | ⊦ i * i ≤ j * j ↔ abs(i) ≤ abs(j) | A User Theorem |
| square-le-01 | ⊦ i ≤ i * i | A User Theorem |
| square-le-02 | ⊦ abs(i) ≤ i * i | A User Theorem |
| square-le-03 | ⊦ i0 ≤ i → i0 ≤ i + j * j | A User Theorem |
| square-le-04 | ⊦ 0 ≤ i ∧ 0 ≤ j → (i * (i + 1) ≤ j * (j + 1) ↔ i ≤ j) | A User Theorem |
| square-le-05 | ⊦ 0 ≤ i ∧ 0 ≤ j → (i * (i + 1) ≤ (j + 1) * (j + 2) ↔ i ≤ j + 1) | A User Theorem |
| square-le-06 | ⊦ i * i ≤ i + 1 ↔ ¬ ¬(i = 0 ∨ i = 1) | A User Theorem |
| square-lez | ⊦ ¬ i * i < 0 | A User Theorem |
| square-lez-01 | ⊦ i * i ≤ 0 ↔ i = 0 | A User Theorem |
| square-ls | ⊦ i * i < j * j ↔ abs(i) < abs(j) | A User Theorem |
| square-ls-01 | ⊦ i < i0 → i < i0 + j * j | A User Theorem |
| square-ls-02 | ⊦ 0 ≤ i ∧ 0 ≤ j → (i * (i + 1) < j * (j + 1) ↔ i < j) | A User Theorem |
| square-ls-03 | ⊦ 0 ≤ i ∧ 0 ≤ j → (i * (i + 1) < (j + 1) * (j + 2) ↔ i < j + 1) | A User Theorem |
| square-ls-04 | ⊦ 0 < i → ¬ i * (i + 1) < 2 | A User Theorem |
| square-minus | ⊦ ~(i * i) < 0 ↔ i ≠ 0 | A User Theorem |
| square-one-le | ⊦ i * i ≤ 1 ↔ i = 0 ∨ i = 1 ∨ i = ~1 | A User Theorem |
| square-zero | ⊦ i * i = 0 ↔ i = 0 | A User Theorem |
| square-zero-01 | ⊦ 0 ≤ i → ¬ (i + 1) * (i + 2) ≤ 0 | A User Theorem |
| square-zero-02 | ⊦ 0 ≤ j ∧ 0 ≤ i → ¬ (i + j) * (i + j + 1) < 0 | A User Theorem |
| succ-lsplit | ⊦ (i + 1) * j = i * j + j | A User Theorem |
| succ-rmerge | ⊦ i * j + i = i * (j + 1) | A User Theorem |
| succ-rsplit | ⊦ i * (j + 1) = i * j + i | A User Theorem |
| three | ⊦ 1 < i → (i * j = 3 ↔ i = 3 ∧ j = 1) | A User Theorem |
| three-01 | ⊦ 2 * i ≠ 3 | A User Theorem |
| two-eq | ⊦ 2 * i = 2 * j ↔ i = j | A User Theorem |
| two-le | ⊦ 2 * i + j ≤ 2 * (i + i0) ↔ j ≤ 2 * i0 | A User Theorem |
| two-le-01 | ⊦ 2 * i + j ≤ 2 * (i + i0) + j0 ↔ j ≤ 2 * i0 + j0 | A User Theorem |
| two-le-02 | ⊦ 2 * (i + j) ≤ 2 * (i + i0) ↔ j ≤ i0 | A User Theorem |
| two-le-03 | ⊦ 2 * (i + j) ≤ 2 * (i + i0) + j0 ↔ 2 * j ≤ 2 * i0 + j0 | A User Theorem |
| two-le-04 | ⊦ 2 * (i + j) + i1 ≤ 2 * (i + i0) + j0 ↔ 2 * j + i1 ≤ 2 * i0 + j0 | A User Theorem |
| two-leone | ⊦ 2 * i ≤ 1 ↔ i ≤ 0 | A User Theorem |
| two-ls | ⊦ 2 * i + j < 2 * (i + i0) ↔ j < 2 * i0 | A User Theorem |
| two-ls-01 | ⊦ 2 * i + j < 2 * (i + i0) + j0 ↔ j < 2 * i0 + j0 | A User Theorem |
| two-ls-02 | ⊦ 2 * (i + j) < 2 * (i + i0) ↔ j < i0 | A User Theorem |
| two-ls-03 | ⊦ 2 * (i + j) < 2 * (i + i0) + j0 ↔ 2 * j < 2 * i0 + j0 | A User Theorem |
| two-ls-04 | ⊦ 2 * (i + j) + i1 < 2 * (i + i0) + j0 ↔ 2 * j + i1 < 2 * i0 + j0 | A User Theorem |
| two-mone | ⊦ 2 * i ≠ ~1 | A User Theorem |
| two-oddeq | ⊦ 2 * i + 1 ≠ 2 * j | A User Theorem |
| two-pred | ⊦ 2 * (i - 1) + 1 = 2 * i - 1 | A User Theorem |
| two-sub | ⊦ 2 * (j0 + i0) + j - 2 * j0 + i = 2 * i0 + j - i | A User Theorem |
| two-sub-01 | ⊦ 2 * i0 + j - i0 + j0 = i0 + j - j0 | A User Theorem |
| two-zero | ⊦ 2 * i = 0 ↔ i = 0 | A User Theorem |
| zero-eq | ⊦ i * j = 0 ↔ i = 0 ∨ j = 0 | A User Theorem |
| zero-ge | ⊦ 0 < i → (0 ≤ i * j ↔ 0 ≤ j) | A User Theorem |
| zero-ge-01 | ⊦ i < 0 → (0 ≤ i * j ↔ j ≤ 0) | A User Theorem |
| zero-ge-02 | ⊦ 0 ≤ i → (0 ≤ i * j ↔ ¬ ¬(i = 0 ∨ 0 ≤ j)) | A User Theorem |
| zero-ge-03 | ⊦ i ≤ 0 → (0 ≤ i * j ↔ ¬ ¬(i = 0 ∨ j ≤ 0)) | A User Theorem |
| zero-ge-add | ⊦ 0 ≤ j1 ∧ j1 < j → (0 ≤ i0 * j + j1 ↔ 0 ≤ i0) | A User Theorem |
| zero-ge-add-01 | ⊦ 0 ≤ j ∧ 0 ≤ j0 ∧ 0 ≤ i0 → 0 ≤ i0 * j + j0 | A User Theorem |
| zero-ge-add-02 | ⊦ 0 ≤ i + j ∧ 0 < j0 → 0 ≤ i * j0 + j * j0 | A User Theorem |
| zero-ge-case | ⊦ 0 ≤ i * j ↔ i = 0 ∨ j = 0 ∨ 0 ≤ i ∧ 0 ≤ j ∨ i ≤ 0 ∧ j ≤ 0 | A User Theorem |
| zero-gr | ⊦ 0 < i → (0 < i * j ↔ 0 < j) | A User Theorem |
| zero-gr-01 | ⊦ i < 0 → (0 < i * j ↔ j < 0) | A User Theorem |
| zero-gr-02 | ⊦ 0 ≤ i → (0 < i * j ↔ ¬ ¬(0 < j ∧ i ≠ 0)) | A User Theorem |
| zero-gr-03 | ⊦ i ≤ 0 → (0 < i * j ↔ ¬ ¬(j < 0 ∧ i ≠ 0)) | A User Theorem |
| zero-gr-add | ⊦ 0 < j → (0 < i * j + j ↔ 0 ≤ i) | A User Theorem |
| zero-gr-add-01 | ⊦ 0 ≤ i ∧ j < 0 ∧ j0 ≤ 0 → ¬ 0 < i * j + j0 | A User Theorem |
| zero-gr-add-02 | ⊦ 0 ≤ i0 ∧ i0 ≤ i1 ∧ j < 0 → ¬ 0 < i1 * j + i0 | A User Theorem |
| zero-gr-case | ⊦ 0 < i * j ↔ 0 < i ∧ 0 < j ∨ i < 0 ∧ j < 0 | A User Theorem |
| zero-le | ⊦ 0 < i → (i * j ≤ 0 ↔ j ≤ 0) | A User Theorem |
| zero-le-01 | ⊦ i < 0 → (i * j ≤ 0 ↔ 0 ≤ j) | A User Theorem |
| zero-le-02 | ⊦ 0 ≤ i → (i * j ≤ 0 ↔ ¬ ¬(i = 0 ∨ j ≤ 0)) | A User Theorem |
| zero-le-03 | ⊦ i ≤ 0 → (i * j ≤ 0 ↔ ¬ ¬(i = 0 ∨ 0 ≤ j)) | A User Theorem |
| zero-le-case | ⊦ i * j ≤ 0 ↔ i = 0 ∨ j = 0 ∨ 0 ≤ i ∧ j ≤ 0 ∨ i ≤ 0 ∧ 0 ≤ j | A User Theorem |
| zero-le-two | ⊦ 2 * i ≤ 0 ↔ i ≤ 0 | A User Theorem |
| zero-left | ⊦ 0 * i = 0 | A User Theorem |
| zero-ls | ⊦ 0 < i → (i * j < 0 ↔ j < 0) | A User Theorem |
| zero-ls-01 | ⊦ i < 0 → (i * j < 0 ↔ 0 < j) | A User Theorem |
| zero-ls-02 | ⊦ 0 ≤ i → (i * j < 0 ↔ ¬ ¬(j < 0 ∧ i ≠ 0)) | A User Theorem |
| zero-ls-03 | ⊦ i ≤ 0 → (i * j < 0 ↔ ¬ ¬(0 < j ∧ i ≠ 0)) | A User Theorem |
| zero-ls-case | ⊦ i * j < 0 ↔ 0 < i ∧ j < 0 ∨ i < 0 ∧ 0 < j | A User Theorem |
| zero-ls-sub | ⊦ i < j → ((i - j) * j0 < 0 ↔ 0 < j0) | A User Theorem |
| zero-ls-two | ⊦ 2 * i < 0 ↔ i < 0 | A User Theorem |
| zero-neq | ⊦ i < 0 → (i * j = 0 ↔ j = 0) | A User Theorem |
| zero-neq-01 | ⊦ 0 < i → (i * j = 0 ↔ j = 0) | A User Theorem |