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: |
|---|---|---|
| Pot-zero | ⊦ j ^ 0 = 1 | An Axiom |
| Pot-pos | ⊦ 0 < i → j ^ i = j ^ i -1 * j | An Axiom |
| Pot-neg | ⊦ i < 0 → j ^ i = 1 / j ^ abs(i) | An Axiom |
| 2pot-leone | ⊦ 2 ^ i < 1 ↔ i < 0 | A User Theorem |
| abs-2pot | ⊦ abs(2 ^ i) = 2 ^ i | A User Theorem |
| add-eq2pot | ⊦ 0 ≤ j ∧ 0 ≤ i ∧ 0 ≤ i0 → (2 ^ i = 2 ^ i0 + j ↔ j = 2 ^ i0 * (2 ^ (i - i0) - 1) ∧ i0 ≤ i) | A User Theorem |
| add-eq2pot-01 | ⊦ 0 ≤ j ∧ 0 ≤ i ∧ 0 ≤ i0 → (2 * 2 ^ i = 2 ^ i0 + j ↔ j = 2 ^ i0 * (2 ^ (i + 1 - i0) - 1) ∧ i0 ≤ i + 1) | A User Theorem |
| div-div-rec | ⊦ j < 0 ∧ 0 < i → ((j - (2 ^ i - 1)) / 2 ^ i - 1) / 2 = (j - (2 ^ (i + 1) - 1)) / 2 ^ (i + 1) | A User Theorem |
| div-div-rec-01 | ⊦ j < 0 ∧ 0 < i → (j - (2 ^ i - 1)) / 2 ^ i = ((j - (2 ^ (i - 1) - 1)) / 2 ^ (i - 1) - 1) / 2 | A User Theorem |
| div-twopot | ⊦ 0 ≤ i ∧ 0 ≤ j → 2 ^ i / 2 ^ j = 2 ^ (i - j) | A User Theorem |
| div2 | ⊦ 2 ^ i / 2 = 2 ^ (i - 1) | A User Theorem |
| div2-2pot | ⊦ 0 ≤ i ∧ 0 ≤ j → (j / 2 ^ i) / 2 = j / 2 ^ (i + 1) | A User Theorem |
| div2-2pot-01 | ⊦ 0 ≤ i ∧ 0 ≤ j → (j / 2) / 2 ^ i = j / 2 ^ (i + 1) | A User Theorem |
| div2-2pot-02 | ⊦ 0 ≤ i ∧ 0 < j → (i * 2 ^ j) / 2 = i * 2 ^ (j - 1) | A User Theorem |
| div2-2pot-03 | ⊦ 0 < i ∧ 0 ≤ j → (j * 2 ^ i + 1) / 2 = j * 2 ^ (i - 1) | A User Theorem |
| div2-2pot-04 | ⊦ 0 < j → (i * 2 ^ j) / 2 = i * 2 ^ (j - 1) | A User Theorem |
| div2-2pot-neg | ⊦ i < 0 ∧ 0 < j → (i * 2 ^ j) / 2 = i * 2 ^ (j - 1) | A User Theorem |
| divmod2-2pot | ⊦ 0 < i ∧ 0 ≤ j → (j % 2 ^ i) / 2 = (j / 2) % 2 ^ (i - 1) | A User Theorem |
| divmod2-2pot-neg | ⊦ j < 0 ∧ 1 < i → ((j % 2 ^ i - 1) / 2) % 2 = ((j - 1) / 2) % 2 | A User Theorem |
| eq-one | ⊦ 2 ^ i = 1 ↔ i = 0 | A User Theorem |
| eq-pos | ⊦ 1 < i0 ∧ 0 ≤ i ∧ 0 ≤ j → (i0 ^ i = i0 ^ j ↔ i = j) | A User Theorem |
| eq-two | ⊦ 0 ≤ i ∧ 0 ≤ j → (2 ^ i = 2 ^ j ↔ i = j) | A User Theorem |
| eq2 | ⊦ 2 ^ i = 2 ↔ i = 1 | A User Theorem |
| eqone | ⊦ i ^ j = 1 ∧ 0 ≤ j → j = 0 ∨ abs(i) = 1 | A User Theorem |
| eqone-01 | ⊦ i ^ j = 1 ∧ 0 < j → abs(i) = 1 | A User Theorem |
| eqone-02 | ⊦ i ^ ~ j = 1 ∧ j < 0 → abs(i) = 1 | A User Theorem |
| equal-minus-one | ⊦ i ≠ 0 ∨ 0 ≤ j → (i ^ j = ~1 ↔ i = ~1 ∧ j ≠ 0 ∧ abs(j) % 2 = 1) | A User Theorem |
| even-square | ⊦ even(i ^2) ↔ even(i) | A User Theorem |
| exin2pot | ⊦ 0 < j → (∃ i. 0 ≤ i ∧ 2 ^ i ≤ j ∧ j < 2 ^ (i + 1)) | A User Theorem |
| exin2pot-neg | ⊦ j < 0 → (∃ i. ~1 ≤ i ∧ j < ~(2 ^ i) ∧ ~(2 ^ (i + 1)) ≤ j) | A User Theorem |
| exinpot | 0 < j, 1 < i ⊦ ∃ i0. 0 ≤ i0 ∧ i ^ i0 ≤ j ∧ j < i ^ (i0 + 1) | A User Theorem |
| geom-mod | ⊦ i ≠ 1 ∧ 0 ≤ j → (1 - i ^ j) % (1 - i) = 0 | A User Theorem |
| grz | ⊦ 0 < i → (0 < i ^ j ↔ i = 1 ∨ 0 ≤ j) | A User Theorem |
| isSquare-10pot | ⊦ isSquare(10 ^ (2 * abs(i))) | A User Theorem |
| le-2pot | ⊦ 0 ≤ i ∧ 0 ≤ j → (2 ^ i ≤ j / 2 ↔ 2 ^ (i + 1) ≤ j) | A User Theorem |
| le-2pot-01 | ⊦ 0 ≤ i ∧ 0 ≤ j → (j / 2 ≤ 2 ^ i ↔ j ≤ 2 ^ (i + 1) + 1) | A User Theorem |
| le-2pot-succ | ⊦ 0 < i ∧ 0 < i0 ∧ 0 < j → (2 ^ i ≤ j * 2 ^ i0 + 1 ↔ 2 ^ i ≤ j * 2 ^ i0) | A User Theorem |
| le-pos | ⊦ 1 < i ∧ 0 ≤ j → (i ^ j ≤ i ^ j0 ↔ j ≤ j0) | A User Theorem |
| le-pos-01 | ⊦ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 < j → (i ^ j ≤ i0 ^ j ↔ i ≤ i0) | A User Theorem |
| le-same | ⊦ 0 < i → (2 ^ (i - 1) ≤ j + 2 ^ i ↔ 0 ≤ j + 2 ^ (i - 1)) | A User Theorem |
| lemon2pot | ⊦ j ≤ 2 ^ i ∧ i ≤ i0 ∧ 0 ≤ i → j ≤ 2 ^ i0 | A User Theorem |
| lemon2pot-01 | ⊦ j ≤ 2 ^ n→i(m * n - 1) ∧ n ≤ n0 ∧ m ≠ 0 ∧ n ≠ 0 → j ≤ 2 ^ n→i(m * n0 - 1) | A User Theorem |
| lemon2pot-02 | ⊦ j ≤ 2 ^ n→i(m * n - 1) + j0 ∧ n ≤ n0 ∧ m ≠ 0 ∧ n ≠ 0 → j ≤ 2 ^ n→i(m * n0 - 1) + j0 | A User Theorem |
| ls-2pot | ⊦ 0 ≤ i → (2 ^ i < j * 2 ^ i ↔ 1 < j) | A User Theorem |
| ls-2pot-01 | ⊦ 0 ≤ i → (j * 2 ^ i < j0 * 2 ^ i ↔ j < j0) | A User Theorem |
| ls-mult-2pot | ⊦ 0 < j ∧ 0 ≤ i ∧ 0 ≤ i0 → (j * 2 ^ i < 2 ^ i0 ↔ j < 2 ^ (i0 - i)) | A User Theorem |
| ls-pos | ⊦ 1 < i ∧ 0 ≤ j → (i ^ j < i ^ j0 ↔ j < j0) | A User Theorem |
| ls-pos-01 | ⊦ i ≤ i0 ∧ 0 ≤ i ∧ 0 ≤ j → i ^ j ≤ i0 ^ j | A User Theorem |
| ls-pos-02 | ⊦ i ≤ i0 ∧ 0 ≤ i ∧ 0 ≤ j → ¬ i0 ^ j < i ^ j | A User Theorem |
| ls-pos-03 | ⊦ 0 ≤ i ∧ 0 ≤ i0 ∧ 0 < j → (i ^ j < i0 ^ j ↔ i < i0) | A User Theorem |
| ls-pos-2pot | ⊦ 0 ≤ j → (2 ^ j < 2 ^ j0 ↔ j < j0) | A User Theorem |
| ls-pos-2pot-01 | 0 ≤ j ⊦ 2 ^ j < 2 ^ j0 ↔ j < j0 | A User Theorem |
| ls-same | ⊦ 0 < i → (j + 2 ^ i < 2 ^ (i - 1) ↔ j + 2 ^ (i - 1) < 0) | A User Theorem |
| minus-odd | ⊦ odd(j) ∧ 0 < j → ~ i ^ j = ~(i ^ j) | A User Theorem |
| minus-one-even | ⊦ 0 < j ∧ j % 2 = 0 → ~1 ^ j = 1 | A User Theorem |
| minus-one-odd | ⊦ 0 < j ∧ j % 2 = 1 → ~1 ^ j = ~1 | A User Theorem |
| minus-square | ⊦ 0 ≤ j → ~ i ^ (2 * j) = i ^ (2 * j) | A User Theorem |
| minus-square-01 | ⊦ ~ i ^ 2 = i ^ 2 | A User Theorem |
| mod-2pot | ⊦ 0 < i → (j * 2 ^ i) % 2 = 0 | A User Theorem |
| mod-add1-negneg | ⊦ j < 0 ∧ j0 < 0 ∧ 0 < i → (j * 2 ^ i + j0) % 2 ^ i = j0 % 2 ^ i | A User Theorem |
| mod-add1-pospos | ⊦ 0 ≤ j ∧ 0 ≤ j0 ∧ 0 < i → (j * 2 ^ i + j0) % 2 ^ i = j0 % 2 ^ i | A User Theorem |
| mod-lesame | ⊦ 0 < i → ¬ 2 ^ i ≤ j % 2 ^ i | A User Theorem |
| mod-lez | ⊦ 0 ≤ j ∧ 0 < i → (j % 2 ^ i ≤ 0 ↔ j % 2 ^ i = 0) | A User Theorem |
| mod-lsz | ⊦ 0 ≤ j ∧ 0 < i → ¬ j % 2 ^ i < 0 | A User Theorem |
| mod-next-square | ⊦ (i ^ 2 * (i + 1) ^ 2) % 4 = 0 | A User Theorem |
| mod-ngez | ⊦ j < 0 ∧ 0 ≤ i → (0 ≤ j % 2 ^ i ↔ j % 2 ^ i = 0) | A User Theorem |
| mod-ngez-01 | ⊦ j < 0 ∧ 0 < i → (0 ≤ j % 2 ^ i ↔ j % 2 ^ i = 0) | A User Theorem |
| mod-pot-shift-pos | ⊦ 0 < j ∧ 0 ≤ i0 → (i % j) ^ i0 % j = i ^ i0 % j | A User Theorem |
| mod-same | ⊦ 0 < j ∧ i ≠ 0 → (i * i0) ^ j % i = 0 | A User Theorem |
| mod-two-ge | ⊦ j ≤ i ∧ 0 ≤ j → 2 ^ i % 2 ^ j = 0 | A User Theorem |
| mod-two-ge-01 | ⊦ j < i ∧ 0 ≤ j → (2 ^ i - 1) % 2 ^ j = 2 ^ j - 1 | A User Theorem |
| mod-two-ls | ⊦ i < j ∧ 0 ≤ i → 2 ^ i % 2 ^ j = 2 ^ i | A User Theorem |
| mod-two-ls-01 | ⊦ i ≤ j ∧ 0 ≤ i → (2 ^ i - 1) % 2 ^ j = 2 ^ i - 1 | A User Theorem |
| mod2-2pot | ⊦ 0 < i → (j % 2 ^ i) % 2 = j % 2 | A User Theorem |
| mod2-2pot-01 | ⊦ 0 ≤ i ∧ 0 ≤ j → (j % 2 ^ (i + 1)) / 2 = (j / 2) % 2 ^ i | A User Theorem |
| mod2-2pot-02 | ⊦ j % 2 ^ i = 1 ∧ 0 < i ∧ 0 ≤ j → j % 2 = 1 | A User Theorem |
| mod2-2pot-03 | ⊦ 0 ≤ i ∧ 0 < j → (i * 2 ^ j) % 2 = 0 | A User Theorem |
| mod2-2pot-04 | ⊦ 0 < i ∧ 0 ≤ j → (j * 2 ^ i + 1) % 2 = 1 | A User Theorem |
| mod2-2pot-05 | ⊦ 0 ≤ i ∧ 0 ≤ j → (j % 2 ^ i ≤ 0 ↔ j % 2 ^ i = 0) | A User Theorem |
| mod2-2pot-06 | ⊦ 0 ≤ i ∧ 0 < j → (j % 2 ^ i ≤ 0 ↔ j % 2 ^ i = 0) | A User Theorem |
| mod2-pos | ⊦ 0 ≤ i ∧ 0 ≤ j → ¬ j % 2 ^ i < 0 | A User Theorem |
| notneg | ⊦ 0 ≤ i ∧ 0 ≤ j → ¬ i ^ j < 0 | A User Theorem |
| notneg-01 | ⊦ 0 < i ∧ 0 ≤ j → ¬ i ^ j ≤ 0 | A User Theorem |
| notneg-02 | ⊦ 0 < i → ¬ i ^ j < 0 | A User Theorem |
| notone | ⊦ 1 < i ∧ 0 < j → ¬ i ^ j ≤ 1 | A User Theorem |
| odd-square | ⊦ odd(i ^2) ↔ odd(i) | A User Theorem |
| one | ⊦ i ^ 1 = i | A User Theorem |
| one-01 | ⊦ 1 ^ j = 1 | A User Theorem |
| one-02 | ⊦ 0 < j → 1 ^ j = 1 | A User Theorem |
| one-03 | ⊦ j + 1 = 0 → i ^ ~ j = i | A User Theorem |
| pot-add-min | ⊦ 0 ≤ j ∧ 0 ≤ j0 → i * 10 ^ j + i0 * 10 ^ j0 = (i * 10 ^ (j - min(j, j0)) + i0 * 10 ^ (j0 - min(j, j0))) * 10 ^ min(j, j0) | A User Theorem |
| pot-dist-pos | ⊦ 0 ≤ j ∧ 0 ≤ j0 → i ^ (j + j0) = i ^ j * i ^ j0 | A User Theorem |
| pot-div | ⊦ 0 ≤ j0 ∧ j0 ≤ j ∧ 0 < i → i ^ j / i ^ j0 = i ^ (j - j0) | A User Theorem |
| pot-div3-nls | ⊦ 2 ≤ j ∧ 2 < i → ¬ j ^ i / 3 < j | A User Theorem |
| pot-eq-sub | ⊦ 0 < j ∧ 0 ≤ j0 ∧ j0 ≤ j1 → (i * j ^ j0 = i0 * j ^ j1 ↔ i = i0 * j ^ (j1 - j0)) | A User Theorem |
| pot-lez | ⊦ 0 < i → (i ^ j ≤ 0 ↔ i ^ j = 0) | A User Theorem |
| pot-mod-add-zero | ⊦ 0 ≤ j ∧ 0 < j0 → ((i + i0 * j ^ j0) % j = 0 ↔ i % j = 0) | A User Theorem |
| pot-mod-zero | ⊦ 0 < j ∧ 0 ≤ j0 ∧ j0 ≤ j1 → j ^ j1 % j ^ j0 = 0 | A User Theorem |
| pot-nls | ⊦ 0 < i ∧ 0 < j → ¬ i ^ j < i | A User Theorem |
| pot-pot | 0 ≤ i, 0 ≤ j, 0 ≤ j0 ⊦ (i ^ j) ^ j0 = i ^ (j * j0) | A User Theorem |
| pot-pot-01 | ⊦ 0 ≤ j ∧ 0 ≤ j0 → (i ^ j) ^ j0 = i ^ (j * j0) | A User Theorem |
| pot-pot-02 | ⊦ 0 ≤ j ∧ 0 ≤ j0 → i ^ (j * j0) = (i ^ j) ^ j0 | A User Theorem |
| pot-pot-03 | ⊦ 0 ≤ j ∧ 0 ≤ j0 → (i ^ (j * j0) ≠ (i ^ j) ^ j0 ↔ false) | A User Theorem |
| pot-root-est | ⊦ 1024 ≤ i → ¬ 4 ^ (i / 3) ≤ (2 * i) ^ sqrt(2 * i) | A User Theorem |
| pot-square | ⊦ 0 ≤ j → i ^ (2 * j) = (i * i) ^ j | A User Theorem |
| pot-square-01 | ⊦ 0 ≤ j → (i * i) ^ j = i ^ (2 * j) | A User Theorem |
| pot-square-02 | ⊦ 0 ≤ j → ((i * i) ^ j ≠ i ^ (2 * j) ↔ false) | A User Theorem |
| pot-square-03 | ⊦ i * i = i ^ 2 | A User Theorem |
| pot-square-04 | ⊦ i ^ 2 = i * i | A User Theorem |
| pot-square-05 | ⊦ i ^ 2 ≠ i * i ↔ false | A User Theorem |
| pot-square-est | ⊦ 36 ≤ i → ¬ 4 ^ (i / 6) < (i + 1) * (i + 1) | A User Theorem |
| pot-square-est-01 | ⊦ 0 ≤ i → ¬ 4 ^ i ≤ i * i | A User Theorem |
| pot-square-est-02 | ⊦ 1 < i → ¬ 4 ^ i ≤ (i + 1) * (i + 1) | A User Theorem |
| pot-square-est-div6 | ⊦ 36 ≤ i → ¬ 4 ^ (i / 6) ≤ (i + 1) * (i + 1) | A User Theorem |
| pot-sub-dist | ⊦ 0 ≤ j0 ∧ j0 ≤ j ∧ i ≠ 0 → i ^ (j - j0) = i ^ j / i ^ j0 | A User Theorem |
| pot-zero-01 | ⊦ 0 < i → (i ^ j = 0 ↔ j < 0 ∧ 1 < i) | A User Theorem |
| pot2-add | 0 < i ⊦ 2 ^ (i - 1) + 2 ^ (i - 1) = 2 ^ i | A User Theorem |
| pot2-div2 | ⊦ 0 < i → 2 ^ i / 2 = 2 ^ (i - 1) | A User Theorem |
| pot2-est-div6 | ⊦ 36 ≤ i → ¬ 2 ^ (i / 6) ≤ i + 1 | A User Theorem |
| pot2-est-mult8 | ⊦ 0 ≤ i → ¬ 8 * 2 ^ i < i + 7 | A User Theorem |
| pot2-le-pred | ⊦ 2 ^ (i - 1) ≤ 2 ^ i | A User Theorem |
| pot2-le-pred-01 | ⊦ 2 ^ (i - 1) + 1 ≤ 2 ^ i ↔ 0 ≤ i | A User Theorem |
| pot2-ls-pred | ⊦ 2 ^ (i - 1) < 2 ^ i ↔ 0 ≤ i | A User Theorem |
| pot2-ls-pred-01 | ⊦ 2 ^ (i - 1) + 1 < 2 ^ i ↔ 1 < i | A User Theorem |
| pot2-mod2-zero | ⊦ 0 < i → 2 ^ i % 2 = 0 | A User Theorem |
| pot2-pos | ⊦ 0 < 2 ^ i ↔ 0 ≤ i | A User Theorem |
| pot2-pos-01 | ⊦ 1 < 2 ^ i ↔ 0 < i | A User Theorem |
| pot2-pos-02 | ⊦ i < 0 → 2 * i ≤ 2 ^ j | A User Theorem |
| pot2-pos-03 | ⊦ i < 0 → 2 * i < 2 ^ j | A User Theorem |
| pot2-pos-04 | ⊦ i < 0 → 2 * i ≤ 2 ^ j + 1 | A User Theorem |
| pot2-pos-05 | ⊦ i < 0 → 2 * i < 2 ^ j + 1 | A User Theorem |
| pot2-suble | ⊦ 0 < i → (j + 2 ^ (i - 1) ≤ 2 ^ i ↔ j ≤ 2 ^ (i - 1)) | A User Theorem |
| pot2-subls | ⊦ 0 < i → (j + 2 ^ (i - 1) < 2 ^ i ↔ j < 2 ^ (i - 1)) | A User Theorem |
| pot2-succ | ⊦ 0 ≤ i → 2 ^ (i + 1) - 2 ^ i = 2 ^ i | A User Theorem |
| pot2-succ-01 | ⊦ 0 < i → 2 ^ (i + 1) - 2 ^ i = 2 ^ i | A User Theorem |
| pred-le | ⊦ 0 < i → ¬ 2 ^ i ≤ 2 ^ (i - 1) | A User Theorem |
| sqrt-10pot | ⊦ sqrt(10 ^ (2 * abs(i))) = 10 ^ abs(i) | A User Theorem |
| square-mod-four | ⊦ ((i - 1) ^ 2 * i ^ 2) % 4 = 0 | A User Theorem |
| square-nls | ⊦ i ^ 2 ≤ j → ¬ sqrt(j) < i | A User Theorem |
| succ | ⊦ 0 ≤ i → j ^ (i + 1) = j ^ i * j | A User Theorem |
| two-le | ⊦ 0 ≤ i → (2 ^ i ≤ 2 ^ j ↔ i ≤ j) | A User Theorem |
| two-le-01 | ⊦ 0 ≤ i → (2 ^ i ≤ 2 ↔ i ≤ 1) | A User Theorem |
| two-leone | ⊦ 2 ^ i ≤ 1 ↔ i < 1 | A User Theorem |
| two-lez | ⊦ 0 ≤ i → ¬ 2 ^ i ≤ 0 | A User Theorem |
| two-lez-01 | ⊦ 2 ^ i ≤ 0 ↔ i < 0 | A User Theorem |
| two-ls | ⊦ 0 ≤ i → (2 < 2 ^ i ↔ 1 < i) | A User Theorem |
| two-lsz | ⊦ ¬ 2 ^ i < 0 | A User Theorem |
| two-minus | ⊦ i < 0 → 2 ^ i = 0 | A User Theorem |
| two-minus-01 | ⊦ 2 ^ ~ 1 = 0 | A User Theorem |
| two-mod | ⊦ 1 < i → 2 ^ i % 2 = 0 | A User Theorem |
| two-mod-01 | ⊦ 1 < i → (2 ^ i - 1) % 2 = 1 | A User Theorem |
| two-mone | ⊦ 1 < i → ¬ 2 ^ i -1 ≤ 0 | A User Theorem |
| two-zero | ⊦ 0 ≤ j → 2 ^ j ≠ 0 | A User Theorem |
| two-zero-01 | ⊦ 2 ^ n→i(m) ≠ 0 | A User Theorem |
| twolezero | ⊦ ¬ 2 ^ n→i(m) ≤ 0 | A User Theorem |
| twopot-mone-div | ⊦ j ≤ i ∧ 0 ≤ j → (2 ^ i - 1) / 2 ^ j = 2 ^ i / 2 ^ j - 1 | A User Theorem |
| twotwo | ⊦ 2 ^ 2 = 4 | A User Theorem |
| zero | ⊦ 0 < j → (i ^ j = 0 ↔ i = 0) | A User Theorem |
| zero-01 | ⊦ 0 < j → 0 ^ j = 0 | A User Theorem |
| zero-02 | ⊦ j < 0 → (i ^ ~ j = 0 ↔ i = 0) | A User Theorem |
| zero-03 | ⊦ j < 0 → 0 ^ ~ j = 0 | A User Theorem |
| zerozero | ⊦ 0 ^ 0 = 1 | A User Theorem |