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: |
|---|---|---|
| Int2nat-zero | ⊦ i→n(0) = 0 | An Axiom |
| Nat2int-zero | ⊦ n→i(0) = 0 | An Axiom |
| Nat2int-succ | ⊦ n→i(n +1) = n→i(n) +1 | An Axiom |
| Int2nat-neg | ⊦ i < 0 → i→n(i) = i→n(~ i) | An Axiom |
| Int2nat-pos | ⊦ 0 < i → i→n(i) = i→n(i - 1) + 1 | An Axiom |
| abs | ⊦ i→n(abs(i)) = i→n(i) | A User Theorem |
| abs-01 | ⊦ i→n(1) = 1 | A User Theorem |
| abs-02 | ⊦ abs(n→i(n)) = n→i(n) | A User Theorem |
| abs-eq | ⊦ i→n(i) = i→n(j) ↔ abs(i) = abs(j) | A User Theorem |
| abs-neg | ⊦ i→n(~ i) = i→n(i) | A User Theorem |
| abs-negp | 0 ≤ i ⊦ i→n(~ i) = i→n(i) | A User Theorem |
| abs-one | ⊦ i < 0 → (i→n(i) = 1 ↔ i = ~1) | A User Theorem |
| abs-pred | ⊦ i→n(i - 1) < i→n(i) ↔ 0 < i | A User Theorem |
| abs-pred-01 | ⊦ i < 0 ∧ i ≠ ~1 → i→n(i + 1) = i→n(i) -1 | A User Theorem |
| abs-pred-02 | ⊦ 0 < i → i→n(i - 1) +1 = i→n(i) | A User Theorem |
| abs-succ | ⊦ i→n(i) < i→n(i + 1) ↔ 0 ≤ i | A User Theorem |
| abs-succ-01 | ⊦ i→n(i + 1) < i→n(i) ↔ i < 0 | A User Theorem |
| abs-succ-02 | ⊦ 0 < i ∧ i ≠ 1 → i→n(i - 1) = i→n(i) -1 | A User Theorem |
| abs-succ-03 | ⊦ 0 < i → i→n(i + 1) = i→n(i) + 1 | A User Theorem |
| abs-zero | ⊦ i→n(i) = 0 ↔ i = 0 | A User Theorem |
| add | 0 ≤ i, 0 ≤ j ⊦ i→n(i) + i→n(j) = i→n(i + j) | A User Theorem |
| add-01 | 0 ≤ i, 0 ≤ j ⊦ i→n(i + j) = i→n(i) + i→n(j) | A User Theorem |
| add-n2i-num | ⊦ 0 ≤ i → n→i(m) + (* i) = n→i(m + i→n(i)) | A User Theorem |
| add-nonneg-int-to-nat | ⊦ 0 ≤ i → i→n(i + n→i(n)) = i→n(i) + n | A User Theorem |
| eight | ⊦ i→n(1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) = 2 + 2 + 2 + 2 | A User Theorem |
| five | ⊦ i→n(1 + 1 + 1 + 1 + 1) = 2 + 2 + 1 | A User Theorem |
| four | ⊦ i→n(1 + 1 + 1 + 1) = 2 + 2 | A User Theorem |
| i2i-neg | ⊦ i < 0 → n→i(i→n(i)) = ~ i | A User Theorem |
| i2i-neg-01 | ⊦ i ≤ 0 → n→i(i→n(i)) = ~ i | A User Theorem |
| i2i-pos | ⊦ 0 < i → n→i(i→n(i)) = i | A User Theorem |
| i2i-pos-01 | ⊦ 0 ≤ i → n→i(i→n(i)) = i | A User Theorem |
| i2n | ⊦ i→n(i) * i→n(j) = i→n(i * j) | A User Theorem |
| i2n-divtwo | ⊦ i→n(2 * i) / 2 = i→n(i) | A User Theorem |
| i2n-mod | ⊦ 0 ≤ i ∧ 0 < j → i→n(i % j) = i→n(i) % i→n(j) | A User Theorem |
| i2n-mult | ⊦ 0 ≤ i ∧ 0 ≤ j → i→n(i * j) = i→n(i) * i→n(j) | A User Theorem |
| i2np | 0 ≤ i, 0 ≤ j ⊦ i→n(i) * i→n(j) = i→n(i * j) | A User Theorem |
| ini2-abs | ⊦ n→i(i→n(i)) = abs(i) | A User Theorem |
| inj | ⊦ n→i(m) = n→i(n) ↔ m = n | A User Theorem |
| inni-le | ⊦ i→n(i) ≤ n → ¬ n→i(n) < i | A User Theorem |
| inni-le-01 | ⊦ n→i(m) + n→i(n) ≤ j → ¬ i→n(j) < m + n | A User Theorem |
| inni-ls | ⊦ i→n(i) < n → ¬ n→i(n) ≤ i | A User Theorem |
| inni-ls-01 | ⊦ n→i(m) + n→i(n) < j → ¬ i→n(j) ≤ m + n | A User Theorem |
| k-one | ⊦ 1 -1 = n→i(0) | A User Theorem |
| labs | ⊦ i→n(i) < i→n(j) ↔ abs(i) < abs(j) | A User Theorem |
| labs-01 | ⊦ i→n(i) ≤ i→n(j) ↔ abs(i) ≤ abs(j) | A User Theorem |
| labsp | 0 ≤ i, 0 ≤ j ⊦ i→n(i) < i→n(j) ↔ abs(i) < abs(j) | A User Theorem |
| le | ⊦ n→i(m) ≤ n→i(n) ↔ m ≤ n | A User Theorem |
| le-fin-add | ⊦ n→i(m) ≤ n→i(n) + (* i) ∧ 0 ≤ i → m ≤ n + i→n(i) | A User Theorem |
| le-int-le-nat | ⊦ i ≥ 0 → ((* i) + n→i(n) ≤ n→i(m) ↔ i→n(i) + n ≤ m) | A User Theorem |
| ls-03 | n ≠ 0 ⊦ 0 ≤ i → i / n→i(n) ≤ i | A User Theorem |
| ls-fin-add | ⊦ n→i(m) < n→i(n) + (* i) ∧ 0 ≤ i → m < n + i→n(i) | A User Theorem |
| ls-int-ls-nat | ⊦ i ≥ 0 → ((* i) + n→i(n) < n→i(m) ↔ i→n(i) + n < m) | A User Theorem |
| minus-one | ⊦ i < 0 → (n→i(m) = i + 1 ↔ m = 0 ∧ i = ~1) | A User Theorem |
| mod-zero-02 | n ≠ 0 ⊦ 0 ≤ i → ¬ i % n→i(n) < 0 | A User Theorem |
| mone | ⊦ i→n(~1) = 1 | A User Theorem |
| mone-01 | ⊦ i + 1 = 0 → i→n(i) = 1 | A User Theorem |
| mult-ls-02 | n ≠ 0 ⊦ i / n→i(n) < i0 → i < i0 * n→i(n) | A User Theorem |
| mult-ls-03 | n ≠ 0 ⊦ i0 < i / n→i(n) → i0 * n→i(n) < i | A User Theorem |
| mult-ls-04 | ⊦ i / (n→i(n) + 1) < i0 → i < i0 * n→i(n) + i0 | A User Theorem |
| mult-ls-05 | ⊦ i0 < i / (n→i(n) + 1) → i0 * n→i(n) + i0 < i | A User Theorem |
| n2i | ⊦ n→i(2) = 1 + 1 | A User Theorem |
| n2i-01 | ⊦ n→i(1) = 1 | A User Theorem |
| n2i-add | ⊦ n→i(m + n) = n→i(m) + n→i(n) | A User Theorem |
| n2i-mult | ⊦ n→i(m * n) = n→i(m) * n→i(n) | A User Theorem |
| n2i-sub | ⊦ n ≤ m → n→i(m - n) = n→i(m) - n→i(n) | A User Theorem |
| n2i2 | ⊦ n→i(m) = 1 + 1 ↔ m = 2 | A User Theorem |
| n2n | ⊦ i→n(n→i(n)) = n | A User Theorem |
| nat | j ≠ 0 ⊦ i→n(i) / i→n(j) = i→n(i / j) | A User Theorem |
| nat-to-int-ge-0 | ⊦ ~1 ≠ n→i(n) + n→i(n0) | A User Theorem |
| nat2int | ⊦ 0 ≤ n→i(n) | A User Theorem |
| nat2int-01 | ⊦ i = j + n→i(n) → j ≤ i | A User Theorem |
| nat2int-02 | ⊦ n→i(n) = 0 ↔ n = 0 | A User Theorem |
| nat2int-03 | ⊦ n→i(n + 1) = n→i(n) + 1 | A User Theorem |
| nat2int-04 | ⊦ n→i(m) < n→i(n) ↔ m < n | A User Theorem |
| nat2int-05 | ⊦ n→i(m) = n→i(n) + 1 ↔ m = n + 1 | A User Theorem |
| nat2int-06 | ⊦ ¬ n→i(n) + 1 < 0 | A User Theorem |
| nat2int-07 | ⊦ 0 ≠ n→i(m) + 1 | A User Theorem |
| nat2int-08 | ⊦ ¬ n→i(n) < 0 | A User Theorem |
| nat2int-09 | ⊦ i→n(n→i(n) + 1) = n + 1 | A User Theorem |
| nat2int-10 | ⊦ n→i(n) ≤ 0 ↔ n = 0 | A User Theorem |
| nat2int-11 | ⊦ n→i(m) + 1 < n→i(n) ↔ m + 1 < n | A User Theorem |
| nat2int-12 | ⊦ i = (j + n→i(n)) + 1 + 1 → j ≤ i | A User Theorem |
| nat2int-13 | ⊦ i = (j + n→i(n)) + 1 → j ≤ i | A User Theorem |
| nat2int-14 | ⊦ n→i(n) < 1 ↔ n = 0 | A User Theorem |
| natpos | 0 < j, 0 ≤ i ⊦ i→n(i) / i→n(j) = i→n(i / j) | A User Theorem |
| nine | ⊦ i→n(1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) = 2 + 2 + 2 + 2 +1 | A User Theorem |
| num-i2n-eq | 0 ≤ i ⊦ i→n(i) = (* m) ↔ i = n→i(m) | A User Theorem |
| num-i2n-eq-01 | i < 0 ⊦ i→n(i) = (* m) ↔ ~ i = n→i(m) | A User Theorem |
| num-i2n-le | 0 ≤ i ⊦ i→n(i) ≤ (* m) ↔ i ≤ n→i(m) | A User Theorem |
| num-i2n-le-01 | i < 0 ⊦ i→n(i) ≤ (* m) ↔ ~ i ≤ n→i(m) | A User Theorem |
| num-i2n-le-02 | 0 ≤ i ⊦ (* m) ≤ i→n(i) ↔ n→i(m) ≤ i | A User Theorem |
| num-i2n-le-03 | i < 0 ⊦ (* m) ≤ i→n(i) ↔ n→i(m) ≤ ~ i | A User Theorem |
| num-i2n-ls | 0 ≤ i ⊦ i→n(i) < (* m) ↔ i < n→i(m) | A User Theorem |
| num-i2n-ls-01 | i < 0 ⊦ i→n(i) < (* m) ↔ ~ i < n→i(m) | A User Theorem |
| num-i2n-ls-02 | 0 ≤ i ⊦ (* m) < i→n(i) ↔ n→i(m) < i | A User Theorem |
| num-i2n-ls-03 | i < 0 ⊦ (* m) < i→n(i) ↔ n→i(m) < ~ i | A User Theorem |
| num-n2i-eq | 0 ≤ i ⊦ n→i(n) = (* i) ↔ n = i→n(i) | A User Theorem |
| num-n2i-eq-01 | i < 0 ⊦ n→i(n) ≠ (* i) | A User Theorem |
| num-n2i-ls | 0 ≤ i ⊦ n→i(n) < (* i) ↔ n < i→n(i) | A User Theorem |
| num-n2i-ls-01 | i < 0 ⊦ ¬ n→i(n) < (* i) | A User Theorem |
| num-n2i-ls-02 | 0 ≤ i ⊦ (* i) < n→i(n) ↔ i→n(i) < n | A User Theorem |
| num-n2i-ls-03 | i < 0 ⊦ (* i) < n→i(n) | A User Theorem |
| num-n2i-ls-04 | 0 ≤ i ⊦ n→i(n) ≤ (* i) ↔ n ≤ i→n(i) | A User Theorem |
| num-n2i-ls-05 | i < 0 ⊦ ¬ n→i(n) ≤ (* i) | A User Theorem |
| num-n2i-ls-06 | 0 ≤ i ⊦ (* i) ≤ n→i(n) ↔ i→n(i) ≤ n | A User Theorem |
| num-n2i-ls-07 | i < 0 ⊦ (* i) ≤ n→i(n) | A User Theorem |
| pos-add | ⊦ n→i(m) + n→i(n) < j → 0 < j | A User Theorem |
| pos-int | ⊦ n→i(m) < j → 0 < j | A User Theorem |
| qzero | ⊦ i < 0 ∧ j < 0 → i + j * n→i(n) < 0 | A User Theorem |
| qzero-01 | ⊦ i < j → n→i(n) * (i - j) ≤ 0 | A User Theorem |
| qzero-02 | ⊦ i < 0 → n→i(n) * i + i ≤ 0 | A User Theorem |
| rax | ⊦ 0 < i + 1 → i→n(i + 1) = i→n(i) + 1 | A User Theorem |
| rax-01 | ⊦ 1 < i → i→n(i - 1) = i→n(i) -1 | A User Theorem |
| rax-02 | ⊦ i + 1 < 0 → i→n(i + 1) = i→n(i) -1 | A User Theorem |
| rax-03 | ⊦ i < 1 → i→n(i - 1) = i→n(i) + 1 | A User Theorem |
| rax-04 | ⊦ 0 ≤ i → i→n(i + 1) = i→n(i) + 1 | A User Theorem |
| rlabs | ⊦ abs(i) < abs(j) ↔ i→n(i) < i→n(j) | A User Theorem |
| seven | ⊦ i→n(1 + 1 + 1 + 1 + 1 + 1 + 1) = 2 + 2 + 2 + 1 | A User Theorem |
| six | ⊦ i→n(1 + 1 + 1 + 1 + 1 + 1) = 2 + 2 + 2 | A User Theorem |
| sub | j ≤ i, 0 ≤ j ⊦ i→n(i - j) = i→n(i) - i→n(j) | A User Theorem |
| sub-01 | i ≤ j, j ≤ 0 ⊦ i→n(i - j) = i→n(i) - i→n(j) | A User Theorem |
| sub-same | ⊦ 0 ≤ i ∧ i ≤ j → (i→n(j) + m - i→n(i)) + i→n(i) = i→n(j) + m | A User Theorem |
| succ | ⊦ 0 < i → i→n(i) + 1 = i→n(i + 1) | A User Theorem |
| succ-01 | ⊦ n→i(m + 1) = n→i(m) + 1 | A User Theorem |
| switch-le | ⊦ i→n(i) ≤ n ↔ abs(i) ≤ n→i(n) | A User Theorem |
| switch-ls | ⊦ i→n(i) < n ↔ abs(i) < n→i(n) | A User Theorem |
| ten | ⊦ i→n(1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) = 2 + 2 + 2 + 2 + 2 | A User Theorem |
| three | ⊦ i→n(1 + 1 + 1) = 2 + 1 | A User Theorem |
| two | ⊦ i→n(0 -1 -1) = 2 | A User Theorem |
| two-01 | ⊦ i→n(1 + 1) = 2 | A User Theorem |
| zero-01 | ⊦ i < 0 ∧ j < 0 → i + j * (n→i(n) + 1) < 0 | A User Theorem |
| zero-02 | ⊦ i * n→i(n) < 0 ↔ n ≠ 0 ∧ i < 0 | A User Theorem |
| zero-08 | ⊦ i < 0 → i / (n→i(n) + 1) ≤ 0 | A User Theorem |
| zero-09 | n ≠ 0 ⊦ i < 0 → i / n→i(n) ≤ 0 | A User Theorem |
| zero-10 | ⊦ 0 ≤ i → 0 ≤ i / (n→i(n) + 1) | A User Theorem |
| zero-11 | n ≠ 0 ⊦ 0 ≤ i → 0 ≤ i / n→i(n) | A User Theorem |
| zero-12 | n ≠ 0 ⊦ 0 ≤ i → ¬ i / n→i(n) < 0 | A User Theorem |
| zero-13 | ⊦ i + j * n→i(n) < 0 ∧ m ≤ n ∧ 0 ≤ j → i + j * n→i(m) < 0 | A User Theorem |