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: |
|---|---|---|
| le-def | ⊦ i ≤ j ↔ ¬ j < i | An Axiom |
| gr-def | ⊦ i > j ↔ j < i | An Axiom |
| ge-def | ⊦ i ≥ j ↔ ¬ i < j | An Axiom |
| Abs-pos | ⊦ ¬ j < 0 → abs(j) = j | An Axiom |
| Minus-def | ⊦ ~ i = 0 - i | An Axiom |
| Abs-neg | ⊦ j < 0 → abs(j) = 0 - j | An Axiom |
| Sub-def | ⊦ i + (j - i) = j | An Axiom |
| abs | ⊦ 1 < i → abs(i) = i | A User Theorem |
| abs-01 | ⊦ abs(abs(i)) = abs(i) | A User Theorem |
| abs-02 | ⊦ abs(0) = 0 | A User Theorem |
| abs-03 | ⊦ 0 ≤ abs(i) | A User Theorem |
| abs-04 | ⊦ 0 ≤ i → abs(i + 1) = abs(i) + 1 | A User Theorem |
| abs-05 | ⊦ i < 0 → abs(i + 1) = abs(i) - 1 | A User Theorem |
| abs-06 | ⊦ 0 < abs(i) ↔ i ≠ 0 | A User Theorem |
| abs-07 | ⊦ abs(i) = 0 ↔ i = 0 | A User Theorem |
| abs-08 | ⊦ i < 0 → abs(i) = ~ i | A User Theorem |
| abs-09 | ⊦ 0 < i → abs(i - 1) = abs(i) - 1 | A User Theorem |
| abs-10 | ⊦ abs(i) - 1 < 0 ↔ i = 0 | A User Theorem |
| abs-11 | ⊦ j < 0 → ¬ abs(i) < j | A User Theorem |
| abs-12 | ⊦ 0 ≤ i ∧ 0 ≤ j → abs(i + j) = abs(i) + abs(j) | A User Theorem |
| abs-14 | ⊦ j < 0 ∧ 0 < i + j → abs(j) < i | A User Theorem |
| abs-15 | ⊦ j < 0 ∧ i + j ≤ 0 → ¬ abs(j) < i | A User Theorem |
| abs-16 | ⊦ 0 < j → abs(j) = j | A User Theorem |
| abs-17 | ⊦ 0 < j → abs(j + 1) = j + 1 | A User Theorem |
| abs-18 | ⊦ abs(i) = i ↔ 0 ≤ i | A User Theorem |
| abs-19 | ⊦ j ≤ i → j ≤ abs(i) | A User Theorem |
| abs-21 | ⊦ i ≠ j → (abs(i) = abs(j) ↔ i = ~ j) | A User Theorem |
| abs-abs | ⊦ j ≠ 0 → abs(abs(j) - 1) = abs(j) - 1 | A User Theorem |
| abs-abs-01 | ⊦ abs(abs(i) + abs(j)) = abs(i) + abs(j) | A User Theorem |
| abs-add | ⊦ i < 0 → i + abs(i) = 0 | A User Theorem |
| abs-add-le-zero | ⊦ abs(i) + abs(j) ≤ 0 ↔ i = 0 ∧ j = 0 | A User Theorem |
| abs-add-pos | ⊦ ¬ abs(i) + abs(j) < 0 | A User Theorem |
| abs-add-zero | ⊦ abs(i) + abs(j) = 0 ↔ i = 0 ∧ j = 0 | A User Theorem |
| abs-le-succ | ⊦ abs(i + 1) ≤ abs(i) ↔ i < 0 | A User Theorem |
| abs-ls | ⊦ i < j ∧ j < 0 → abs(j) < abs(i) | A User Theorem |
| abs-ls-01 | ⊦ j < i ∧ 0 ≤ j → abs(j - i) ≤ abs(i) | A User Theorem |
| abs-ls-02 | ⊦ j ≤ j0 ∧ j0 ≤ i → abs(j0 - j) ≤ abs(i - j) | A User Theorem |
| abs-ls-03 | ⊦ j < i → (i < abs(j - i) ↔ j < 0) | A User Theorem |
| abs-ls-04 | 0 ≤ i, abs(j) < i ⊦ 0 ≤ i + j | A User Theorem |
| abs-mone | ⊦ abs(~1) = 1 | A User Theorem |
| abs-neg | ⊦ abs(~ i) = abs(i) | A User Theorem |
| abs-one | ⊦ abs(1) = 1 | A User Theorem |
| abs-one-01 | ⊦ i ≠ 0 ∧ i ≠ 1 → (abs(i) ≤ 1 ↔ i = ~1) | A User Theorem |
| abs-sub | ⊦ ¬ abs(j - i) + i < j | A User Theorem |
| abs-sub-01 | ⊦ i + 1 ≠ j ∧ i < j → ¬ abs(j - i) ≤ abs(j - (i + 1) + 1) | A User Theorem |
| abs-sub-02 | ⊦ i < j → ¬ abs(j - i) ≤ abs(j - i + 1) | A User Theorem |
| abs-succ | ⊦ i < 0 → (i + 1 = abs(j) ↔ i = ~1 ∧ j = 0) | A User Theorem |
| abs-two | ⊦ abs(1 + 1) = 1 + 1 | A User Theorem |
| abs-zero | ⊦ abs(i) ≤ 0 ↔ i = 0 | A User Theorem |
| absa | ⊦ i ≤ 0 ∧ j ≤ 0 → abs(i + j) = abs(i) + abs(j) | A User Theorem |
| abseq | ⊦ abs(i) + i = 0 ↔ i ≤ 0 | A User Theorem |
| absle | ⊦ 0 ≤ i → abs(i) = i | A User Theorem |
| absle-01 | ⊦ i ≤ 0 ∧ j ≤ 0 → (abs(i) ≤ abs(j) ↔ j ≤ i) | A User Theorem |
| absls | ⊦ ¬ abs(i) < 0 | A User Theorem |
| absls-01 | ⊦ ¬ abs(i) < i | A User Theorem |
| absls-02 | ⊦ i ≤ 0 ∧ j ≤ 0 → (abs(i) < abs(j) ↔ j < i) | A User Theorem |
| absls-03 | ⊦ i + 1 < abs(i) ↔ i < 0 | A User Theorem |
| absls-04 | ⊦ i < abs(i -1) ↔ i ≤ 0 | A User Theorem |
| absls-05 | ⊦ abs(i) ≤ abs(i -1) ↔ i ≤ 0 | A User Theorem |
| absls-06 | ⊦ i < abs(i) ↔ i < 0 | A User Theorem |
| absneg | ⊦ abs(i) = i ∨ abs(i) = ~ i | A User Theorem |
| absneg-01 | ⊦ abs(i) ≠ i → abs(i) = ~ i | A User Theorem |
| absneg-02 | ⊦ abs(i) ≠ ~ i → abs(i) = i | A User Theorem |
| absone | ⊦ abs(i) = j + 1 ∧ j ≤ 0 ∧ i ≠ 0 → j = 0 | A User Theorem |
| absone-01 | ⊦ abs(i) = j + 1 + 1 ∧ j < 0 ∧ i ≠ 0 → j = ~1 | A User Theorem |
| absone-02 | ⊦ abs(i) = j + 1 ∧ i ≠ 0 → 0 ≤ j | A User Theorem |
| absp | 0 ≤ j, j < i ⊦ abs(j - i) ≤ abs(i) | A User Theorem |
| absp-01 | j ≤ j0, i ≤ j ⊦ abs(j - i) ≤ abs(j0 - i) | A User Theorem |
| abssub | ⊦ j ≤ i → abs(i - j) = i - j | A User Theorem |
| abssub-01 | ⊦ j < i → abs(i - j + 1) = i - j + 1 | A User Theorem |
| abssub-02 | ⊦ j < i → abs(i - j) = i - j | A User Theorem |
| abssub-03 | j ≤ i ⊦ abs((* i) - j) + j = i | A User Theorem |
| abssub-04 | ⊦ j ≤ i → abs(i - j) + j = i | A User Theorem |
| abssub-05 | i0 ≤ i + 1 ⊦ j < i0 → abs((* i) - j) + j = i | A User Theorem |
| add-pos-ge | ⊦ j0 ≥ 0 → i + j0 ≥ i | A User Theorem |
| add-rew | ⊦ j = i0 + j0 ↔ j - i0 = j0 | A User Theorem |
| add-shift | ⊦ i + j = i0 ↔ i = i0 - j | A User Theorem |
| anti | ⊦ i ≤ j → (j ≤ i ↔ i = j) | A User Theorem |
| bet | ⊦ 0 < i → (i ≤ 1 ↔ i = 1) | A User Theorem |
| bet-01 | ⊦ 0 ≤ i → (i < 1 ↔ i = 0) | A User Theorem |
| discard-add2-lels-left | ⊦ i + j ≤ j0 ∧ 0 < j → i < j0 | A User Theorem |
| elim-sub | ⊦ i0 = i - j ↔ i = i0 + j | A User Theorem |
| estimate-add1-le-left | ⊦ i + j ≤ j0 ∧ i0 ≤ i → i0 + j ≤ j0 | A User Theorem |
| estimate-add1-le-right | ⊦ j0 ≤ i + j ∧ i ≤ i0 → j0 ≤ i0 + j | A User Theorem |
| estimate-add1-ls-left | ⊦ i + j < j0 ∧ i0 ≤ i → i0 + j < j0 | A User Theorem |
| estimate-add1-ls-right | ⊦ j0 < i + j ∧ i ≤ i0 → j0 < i0 + j | A User Theorem |
| estimate-add1-lsle-left | ⊦ i + j ≤ j0 ∧ i0 < i → i0 + j < j0 | A User Theorem |
| estimate-add1-lsle-right | ⊦ j0 ≤ i + j ∧ i < i0 → j0 < i0 + j | A User Theorem |
| estimate-add2-le-left | ⊦ i + j ≤ i0 ∧ j0 ≤ j → i + j0 ≤ i0 | A User Theorem |
| estimate-add2-le-right | ⊦ i0 ≤ i + j ∧ j ≤ j0 → i0 ≤ i + j0 | A User Theorem |
| estimate-add2-ls-left | ⊦ i + j < i0 ∧ j0 ≤ j → i + j0 < i0 | A User Theorem |
| estimate-add2-ls-right | ⊦ i0 < i + j ∧ j ≤ j0 → i0 < i + j0 | A User Theorem |
| estimate-add2-lsle-left | ⊦ i + j ≤ i0 ∧ j0 < j → i + j0 < i0 | A User Theorem |
| estimate-add2-lsle-right | ⊦ i0 ≤ i + j ∧ j < j0 → i0 < i + j0 | A User Theorem |
| ex-le-add | ⊦ i ≤ j ↔ (∃ i0. j = i + i0 ∧ 0 ≤ i0) | A User Theorem |
| forward-le | ⊦ i ≤ j ∧ 0 < i → 0 < j | A User Theorem |
| forward-le-01 | ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j | A User Theorem |
| forward-le-02 | ⊦ j < i ∧ i ≤ 0 → j < 0 | A User Theorem |
| forward-le-03 | ⊦ j ≤ i ∧ i < 0 → j < 0 | A User Theorem |
| forward-le-04 | ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0 | A User Theorem |
| forward-le-05 | ⊦ i < j ∧ 0 ≤ i → 0 < j | A User Theorem |
| forward-lele | ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1 | A User Theorem |
| forward-lels | ⊦ i ≤ j ∧ j < j0 → i < j0 | A User Theorem |
| forward-lsle | ⊦ i < j ∧ j ≤ j0 → i < j0 | A User Theorem |
| ge | ⊦ i ≥ j ↔ j ≤ i | A User Theorem |
| int-add-pos | ⊦ 0 ≤ j ∧ j < j1 ∧ j + i = j1 → 0 < i | A User Theorem |
| int-add-pos-01 | ⊦ 0 ≤ j ∧ j < j1 ∧ j + i = j1 → ¬ i ≤ 0 | A User Theorem |
| int-add-same-pos | ⊦ j > 0 → i < i + j | A User Theorem |
| int-simp-01 | ⊦ i < i1 ∧ i2 < i3 → (i + i2 = i1 + i3 ↔ false) | A User Theorem |
| int-simp-02 | ⊦ i ≤ i1 ∧ i2 < i3 → (i + i2 = i1 + i3 ↔ false) | A User Theorem |
| int-simp-03 | ⊦ i < i1 ∧ i2 ≤ i3 → (i + i2 = i1 + i3 ↔ false) | A User Theorem |
| int-simp-04 | ⊦ i < i1 ∧ i2 < i3 → (i1 + i3 < i + i2 ↔ false) | A User Theorem |
| int-simp-05 | ⊦ i ≤ i1 ∧ i2 < i3 → (i1 + i3 < i + i2 ↔ false) | A User Theorem |
| int-simp-06 | ⊦ i < i1 ∧ i2 ≤ i3 → (i1 + i3 < i + i2 ↔ false) | A User Theorem |
| int-simp-07 | ⊦ i ≤ i1 ∧ i2 ≤ i3 → (i1 + i3 < i + i2 ↔ false) | A User Theorem |
| int-simp-08 | ⊦ i < i1 ∧ i2 < i3 → (i1 + i3 ≤ i + i2 ↔ false) | A User Theorem |
| int-simp-09 | ⊦ i ≤ i1 ∧ i2 < i3 → (i1 + i3 ≤ i + i2 ↔ false) | A User Theorem |
| int-simp-10 | ⊦ i < i1 ∧ i2 ≤ i3 → (i1 + i3 ≤ i + i2 ↔ false) | A User Theorem |
| int-simp-11 | ⊦ i2 + i = i1 ∧ i0 + i2 < i1 → ¬ i ≤ i0 | A User Theorem |
| k-sub-rec1 | ⊦ j > 0 ∧ i = i0 +1 → i - j = i0 - j -1 | A User Theorem |
| k-sub-rec2 | ⊦ j < 0 ∧ i = i0 -1 → i - j = i0 - j +1 | A User Theorem |
| le-add | ⊦ i + j ≤ i0 + j ↔ i ≤ i0 | A User Theorem |
| le-add-01 | ⊦ i + j ≤ i0 ∧ j ≥ 0 ∧ j0 ≥ 0 → i - j0 ≤ i0 | A User Theorem |
| le-add-02 | ⊦ i + j0 ≤ i0 ∧ j0 ≥ 0 → i ≤ i0 | A User Theorem |
| le-add-03 | ⊦ i ≤ i0 ∧ j0 ≥ 0 → i ≤ i0 + j0 | A User Theorem |
| le-add-04 | ⊦ i + j0 ≤ i0 ∧ j0 ≥ 0 → i ≤ i0 + j0 | A User Theorem |
| le-add-05 | ⊦ 0 ≤ i ∧ i + i0 + i1 + i2 ≤ i3 ∧ 0 < i2 → ¬ i + i3 < i1 + i2 + i0 | A User Theorem |
| le-add-06 | ⊦ 0 ≤ i ∧ i0 + i + i1 ≤ i2 → ¬ i + i2 < i1 + i0 | A User Theorem |
| le-add-07 | ⊦ 0 ≤ i ∧ 0 < i0 ∧ i0 + i2 + j ≤ i1 → ¬ i + i1 < j + i2 | A User Theorem |
| le-add-08 | ⊦ 0 < i ∧ 0 ≤ i0 ∧ i0 + i1 + i2 + i ≤ j → ¬ i0 + j < i1 + i2 | A User Theorem |
| le-rec | ⊦ i ≠ j → (i ≤ j ↔ i ≤ j - 1) | A User Theorem |
| le-rew-succ | ⊦ i ≤ j ↔ i < j + 1 | A User Theorem |
| le-sub-same | ⊦ i - j ≤ i0 - j ↔ i ≤ i0 | A User Theorem |
| le-three | ⊦ 1 < i ∧ i ≠ 2 → (i ≤ 3 ↔ i = 3) | A User Theorem |
| lels | ⊦ ¬ i < j ↔ j ≤ i | A User Theorem |
| lels-01 | ⊦ ¬ i ≤ j ↔ j < i | A User Theorem |
| lels-02 | ⊦ i ≠ j → (i ≤ j ↔ i < j) | A User Theorem |
| lels-03 | ⊦ i < j → (¬ ¬ j ≤ i ↔ false) | A User Theorem |
| lels-04 | ⊦ i ≤ j → (¬ ¬ j < i ↔ false) | A User Theorem |
| lenls | ⊦ i ≤ j → ¬ j < i | A User Theorem |
| leone | ⊦ 1 ≤ i ↔ 0 < i | A User Theorem |
| lep | ⊦ i ≤ i + j ↔ 0 ≤ j | A User Theorem |
| lep-01 | ⊦ i + j ≤ i ↔ j ≤ 0 | A User Theorem |
| lep-02 | ⊦ i + j ≤ i + j0 ↔ j ≤ j0 | A User Theorem |
| lepr | ⊦ ¬ i ≤ i -1 | A User Theorem |
| ler | ⊦ i ≤ i | A User Theorem |
| les | ⊦ i < j → (j ≤ i + 1 ↔ j = i + 1) | A User Theorem |
| ls-rew-succ | ⊦ i < j ↔ i + 1 ≤ j | A User Theorem |
| lsone | ⊦ i < 1 ↔ i ≤ 0 | A User Theorem |
| lstwo | ⊦ i ≠ 1 ∧ 0 ≤ i → (i < 2 ↔ i = 0) | A User Theorem |
| lstwo-01 | ⊦ i ≠ 0 ∧ 0 ≤ i → (i < 2 ↔ i = 1) | A User Theorem |
| minus | ⊦ ~(~ i - 1) = i + 1 | A User Theorem |
| minus-01 | ⊦ ~(i + 1) = ~ i - 1 | A User Theorem |
| minus-02 | ⊦ ~(i - 1) = ~ i + 1 | A User Theorem |
| minus-add | i < 0 ⊦ (* i) + j = j - ~ i | A User Theorem |
| minus-ass | ⊦ i - i1 - j = i - i1 + j | A User Theorem |
| minus-five | ⊦ ~(1 + 1 + 1) - 1 + 1 = ~(1 + 1 + 1 + 1 + 1) | A User Theorem |
| minus-four | ⊦ ~(1 + 1) - 1 + 1 = ~(1 + 1 + 1 + 1) | A User Theorem |
| minus-gr | ⊦ 0 > ~ i ↔ i > 0 | A User Theorem |
| minus-neg | j < 0 ⊦ i - (* j) = i + ~ j | A User Theorem |
| minus-rew | ⊦ i - j = i + ~ j | A User Theorem |
| minus-sub | ⊦ ~(i - j) = j - i | A User Theorem |
| minus-three | ⊦ ~(1 + 1) - 1 = ~(1 + 1 + 1) | A User Theorem |
| mmone | ⊦ ~ ~1 = 1 | A User Theorem |
| mone | ⊦ ~1 = ~ 1 | A User Theorem |
| mone-01 | ⊦ i + ~1 = i - 1 | A User Theorem |
| mone-02 | ⊦ i < ~1 ↔ i < ~ 1 | A User Theorem |
| mone-03 | ⊦ i + 1 = 0 → ~ i = 1 | A User Theorem |
| mone-04 | ⊦ 0 ≤ i + 1 ∧ i ≠ ~1 → 0 ≤ i | A User Theorem |
| mone-05 | ⊦ i ≤ ~1 ↔ i < 0 | A User Theorem |
| mone-06 | ⊦ ~1 < i ↔ 0 ≤ i | A User Theorem |
| mone-07 | ⊦ i + 1 ≠ 0 → (~1 ≤ i ↔ 0 ≤ i) | A User Theorem |
| mone-08 | ⊦ i < 0 → (~1 ≤ i ↔ i = ~1) | A User Theorem |
| mone-neg | ⊦ 0 ≤ i ∧ 0 ≤ j → i + j ≠ ~1 | A User Theorem |
| neg | ⊦ 0 < ~ i ↔ i < 0 | A User Theorem |
| neg-01 | ⊦ ~ j < ~ i ↔ i < j | A User Theorem |
| neg-02 | ⊦ ~ ~ i = i | A User Theorem |
| neg-03 | ⊦ ~ i + i = 0 | A User Theorem |
| neg-04 | ⊦ ~ 0 = 0 | A User Theorem |
| neg-05 | ⊦ ~ i < 0 ↔ 0 < i | A User Theorem |
| neg-06 | ⊦ 0 - i = ~ i | A User Theorem |
| neg-07 | ⊦ i < ~ j ↔ i + j < 0 | A User Theorem |
| neg-08 | ⊦ i + ~ j < 0 ↔ i < j | A User Theorem |
| neg-09 | ⊦ 0 < i + ~ j ↔ j < i | A User Theorem |
| neg-10 | ⊦ ~ i = 0 ↔ i = 0 | A User Theorem |
| neg-11 | ⊦ ~ i + ~ j = ~(i + j) | A User Theorem |
| neg-12 | ⊦ ~ i = ~ j ↔ i = j | A User Theorem |
| neg-13 | ⊦ ~ i < j ↔ 0 < j + i | A User Theorem |
| neg-14 | ⊦ i = ~ i ↔ i = 0 | A User Theorem |
| neg-15 | ⊦ i + ~ j = i - j | A User Theorem |
| neg-add | ⊦ i + ~ i = 0 | A User Theorem |
| neg-eq | ⊦ ~ i = j → (~ j = i ↔ true) | A User Theorem |
| negadd | ⊦ i + ~ j < ~ j0 ↔ i + j0 < j | A User Theorem |
| negeq | ⊦ ~ i = j ↔ i + j = 0 | A User Theorem |
| negle-07 | ⊦ i ≤ ~ j ↔ i + j ≤ 0 | A User Theorem |
| negle-13 | ⊦ ~ i ≤ j ↔ 0 ≤ i + j | A User Theorem |
| negone | ⊦ ~(i + 1) = (~ i)-1 | A User Theorem |
| not-mone | ⊦ 0 ≤ j ∧ 0 ≤ i → i + j ≠ ~1 | A User Theorem |
| not-mtwo | ⊦ 0 ≤ j ∧ 0 ≤ i → i + j ≠ ~2 | A User Theorem |
| notle-pos | ⊦ 0 ≤ i ∧ ¬ i0 ≤ j → ¬ i + i0 ≤ j | A User Theorem |
| num-between | i + 1 = i0 ⊦ (* i) < j → (j ≤ (* i0) ↔ j = i0) | A User Theorem |
| num-eq-shift | j < 0 ⊦ i + (* j) = i0 ↔ i = i0 + ~ j | A User Theorem |
| num-subadd | ⊦ (* i) - j + (* i0) = i - i0 - j | A User Theorem |
| numabsneg | ⊦ i < 0 → abs((* i)) = ~ i | A User Theorem |
| numabspos | ⊦ 0 ≤ i → abs((* i)) = i | A User Theorem |
| numadd | ⊦ i + (* j) = i0 + (* j0) ↔ i = i0 + (j0 - j) | A User Theorem |
| numadd-01 | ⊦ (* j) = i0 + (* j0) ↔ j - j0 = i0 | A User Theorem |
| numle-01 | ⊦ i + (* j) ≤ i0 + (* j0) ↔ i ≤ i0 + (j0 - j) | A User Theorem |
| numle-02 | ⊦ (* j) ≤ i0 + (* j0) ↔ j - j0 ≤ i0 | A User Theorem |
| numle-03 | ⊦ i + (* j) ≤ (* j0) ↔ i ≤ j0 - j | A User Theorem |
| numlef | ⊦ (* i) ≤ j ∧ i ≠ 0 → i - 1 < j | A User Theorem |
| numlef-01 | ⊦ (* i) ≤ j → i - 1 < j | A User Theorem |
| numleledel | j0 ≠ 0, j ≤ j0 ⊦ i ≤ (* j) → i ≤ (* j0) | A User Theorem |
| numleledel-01 | i0 ≠ 0, i0 ≤ i ⊦ (* i) ≤ j → (* i0) ≤ j | A User Theorem |
| numlelsdel | j0 ≠ 0, j ≤ j0 ⊦ i < (* j) → i < (* j0) | A User Theorem |
| numlelsdel-01 | i0 ≠ 0, i0 ≤ i ⊦ (* i) < j → (* i0) < j | A User Theorem |
| numls-01 | ⊦ i + (* j) < i0 + (* j0) ↔ i < i0 + (j0 - j) | A User Theorem |
| numls-02 | ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0 | A User Theorem |
| numls-03 | ⊦ i + (* j) < (* j0) ↔ i < j0 - j | A User Theorem |
| numlsf | ⊦ (* i) < j ∧ i ≠ 0 → i + 1 ≤ j | A User Theorem |
| numlsf-01 | ⊦ (* i) < j ∧ 0 < i → 0 ≤ j ∧ 0 < j | A User Theorem |
| numlsf-02 | ⊦ (* i) < j → i + 1 ≤ j | A User Theorem |
| numlsledel | j0 ≠ 0, j < j0 ⊦ i ≤ (* j) → i < (* j0) | A User Theorem |
| numlsledel-01 | i0 ≠ 0, i0 < i ⊦ (* i) ≤ j → (* i0) < j | A User Theorem |
| numlslsdel | ⊦ i ≤ j ∧ j0 ≠ 0 ∧ j < j0 → i < (* j0) | A User Theorem |
| numlslsdel-01 | ⊦ i ≤ j ∧ i0 ≠ 0 ∧ i0 < i → (* i0) < j | A User Theorem |
| numlslsdel-02 | ⊦ i < j ∧ j0 ≠ 0 ∧ j ≤ j0 → i < (* j0) | A User Theorem |
| numlslsdel-03 | ⊦ i < j ∧ i0 ≠ 0 ∧ i0 ≤ i → (* i0) < j | A User Theorem |
| numsub | ⊦ (* i) + i0 - (* j) = (i - j) + i0 | A User Theorem |
| one-03 | ⊦ 0 < i ∧ 0 ≤ j → (1 = i + j ↔ i = 1 ∧ j = 0) | A User Theorem |
| ple | i ≤ j, i0 ≤ j0 ⊦ i + i0 ≤ j + j0 | A User Theorem |
| ple-01 | i < j, i0 ≤ j0 ⊦ i + i0 < j + j0 | A User Theorem |
| ple-02 | i + j0 ≤ j, 0 ≤ j0 ⊦ i ≤ j | A User Theorem |
| ple-03 | i + j0 ≤ j, i0 ≤ j0 ⊦ i + i0 ≤ j | A User Theorem |
| ple-04 | i ≤ j + i0, j ≤ j0 ⊦ i ≤ j0 + i0 | A User Theorem |
| pls | j0 < i + j, j ≤ j0 ⊦ j0 < i + j0 | A User Theorem |
| pls-01 | i ≤ j + i0, j < j0 ⊦ i < j0 + i0 | A User Theorem |
| rew-eqzero | ⊦ i + j = 0 ↔ i = ~ j | A User Theorem |
| rew-eqzero-01 | ⊦ i + j = 0 ↔ j = ~ i | A User Theorem |
| sub-add | ⊦ i + j - i = j | A User Theorem |
| sub-add-01 | ⊦ i + (j - i0) = i + j - i0 | A User Theorem |
| sub-add-02 | ⊦ (i + j) + 1 - i = j + 1 | A User Theorem |
| sub-add-03 | ⊦ i + j - (i - 1) = j + 1 | A User Theorem |
| sub-add-04 | ⊦ i + j - 1 - i = j - 1 | A User Theorem |
| sub-add-05 | ⊦ i + j - i + 1 = j - 1 | A User Theorem |
| sub-add-06 | ⊦ i + j - i0 + j = i - i0 | A User Theorem |
| sub-add-07 | ⊦ i + 1 - j = (i - j) + 1 | A User Theorem |
| sub-add-08 | ⊦ i - j + 1 = i - j - 1 | A User Theorem |
| sub-add-09 | ⊦ i - j + i = ~ j | A User Theorem |
| sub-eq | ⊦ i - j = i0 ↔ i = i0 + j | A User Theorem |
| sub-eq-01 | ⊦ i = j → i - j = 0 | A User Theorem |
| sub-le | ⊦ i - j ≤ i0 ↔ i ≤ j + i0 | A User Theorem |
| sub-le-01 | ⊦ i ≤ j - i0 ↔ i + i0 ≤ j | A User Theorem |
| sub-less | ⊦ 0 < i ∧ 0 < j ∧ 0 < i1 → i ≤ j - i1 → i ≤ j | A User Theorem |
| sub-ls | ⊦ i - j < i0 ↔ i < j + i0 | A User Theorem |
| sub-ls-01 | ⊦ i < j - i0 ↔ i + i0 < j | A User Theorem |
| sub-ls-02 | ⊦ (i - j) + i0 < j0 ↔ i + i0 < j + j0 | A User Theorem |
| sub-minus | ⊦ ~ i - ~ j = j - i | A User Theorem |
| sub-pred | ⊦ i -1 = i - 1 | A User Theorem |
| sub-same | ⊦ i - (i - j) = j | A User Theorem |
| sub-same-01 | ⊦ i + j - j = i | A User Theorem |
| sub-shift | ⊦ i + j - i0 = (i - i0) + j | A User Theorem |
| sub-shift-second | ⊦ i + j - i0 = i + (j - i0) | A User Theorem |
| sub-sub | ⊦ i - j - i0 = i - j + i0 | A User Theorem |
| sub-sub-01 | ⊦ i - 1 - j = i - j - 1 | A User Theorem |
| sub-sub-02 | ⊦ i - (j - 1) = (i - j) + 1 | A User Theorem |
| sub-sub-03 | ⊦ i - i = 0 | A User Theorem |
| sub-sub-04 | ⊦ i - (j - j0) = i + j0 - j | A User Theorem |
| sub-zero | ⊦ i + (0 - i0) = i - i0 | A User Theorem |
| sub-zero-01 | ⊦ i - 0 = i | A User Theorem |
| subneg | ⊦ i - ~ j = i + j | A User Theorem |
| subsub | ⊦ ~ i - j = ~(i + j) | A User Theorem |
| succ-01 | ⊦ i + 1 ≤ j ↔ i < j | A User Theorem |
| succ-02 | ⊦ i < j + 1 ↔ i ≤ j | A User Theorem |
| transrew | ⊦ ¬ i ≤ i0 ∧ i ≤ j → ¬ j ≤ i0 | A User Theorem |
| transrew-01 | ⊦ ¬ i ≤ i0 ∧ j ≤ i0 → ¬ i ≤ j | A User Theorem |
| ttwo | ⊦ i + i ≤ j + j ↔ i ≤ j | A User Theorem |
| zero-eq | ⊦ 0 ≤ i ∧ 0 ≤ j → (i + j = 0 ↔ i = 0 ∧ j = 0) | A User Theorem |
| zero-ge | ⊦ 0 ≤ i ∧ 0 ≤ j → 0 ≤ i + j | A User Theorem |
| zero-ge-01 | ⊦ i < 0 ∧ j < 0 → ¬ 0 ≤ i + j | A User Theorem |
| zero-gels | ⊦ i < 0 ∧ 0 ≤ j → ¬ j < i | A User Theorem |
| zero-gels-01 | ⊦ i < 0 ∧ 0 ≤ j → i < j | A User Theorem |
| zero-gels-02 | ⊦ i < 0 ∧ 0 < j → ¬ j ≤ i | A User Theorem |
| zero-gels-03 | ⊦ i < 0 ∧ 0 ≤ j → i ≤ j | A User Theorem |
| zero-gels-04 | ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j | A User Theorem |
| zero-gs | ⊦ 0 ≤ i ∧ 0 ≤ j → ¬ i + j < 0 | A User Theorem |
| zero-not | ⊦ abs(i) < j ∧ j ≤ abs(i0) → i + i0 ≠ 0 | A User Theorem |
| zeroone | ⊦ 0 ≤ i ∧ i ≤ 1 → i = 0 ∨ i = 1 | A User Theorem |