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: |
|---|---|---|
| Square-def | ⊦ i ^2 = i * i | An Axiom |
| Sqrt-def | ⊦ 0 ≤ i → sqrt(i) ^2 ≤ i ∧ i < sqrt(i) +1 ^2 | An Axiom |
| isSquare-def | ⊦ isSquare(i) ↔ (∃ j. j * j = i) | An Axiom |
| abs | ⊦ abs(i) ^2 = i ^2 | A User Theorem |
| abs-01 | j ≠ 0 ⊦ (abs(i) / j)^2 = (i / j)^2 | A User Theorem |
| add-even | ⊦ (j1 + j2) % 2 = 0 → ((j1 ^2 + j2 ^2) % 2 ≠ 0 ↔ false) | A User Theorem |
| div | ⊦ i % j = 0 ∧ j ≠ 0 → (i / j)^2 = i ^2 / j ^2 | A User Theorem |
| euler-four-square-identity | ⊦ (i1 ^2 + i2 ^2 + i3 ^2 + i4 ^2) * (j1 ^2 + j2 ^2 + j3 ^2 + j4 ^2) = (i1 * j1 - i2 * j2 - i3 * j3 - i4 * j4)^2 + ((i1 * j2 + i2 * j1) + i3 * j4 - i4 * j3)^2 + (((i1 * j3 - i2 * j4) + i3 * j1) + i4 * j2)^2 + ((i1 * j4 + i2 * j3 - i3 * j2) + i4 * j1)^2 | A User Theorem |
| euler-four-square-identity2 | ⊦ (i1 ^2 + i2 ^2 + i3 ^2 + i4 ^2) * (j1 ^2 + j2 ^2 + j3 ^2 + j4 ^2) = (((i1 * j1 + i2 * j2) + i3 * j3) + i4 * j4)^2 + ((i1 * j2 - i2 * j1 - i3 * j4) + i4 * j3)^2 + (i1 * j3 + i2 * j4 - i3 * j1 - i4 * j2)^2 + ((i1 * j4 - i2 * j3) + i3 * j2 - i4 * j1)^2 | A User Theorem |
| even | ⊦ i ^2 % 2 = 0 ↔ i % 2 = 0 | A User Theorem |
| four-square-le-zero | ⊦ i ^2 + i0 ^2 + i1 ^2 + i2 ^2 ≤ 0 ↔ i = 0 ∧ i0 = 0 ∧ i1 = 0 ∧ i2 = 0 | A User Theorem |
| inverse-i | ⊦ sqrt(i ^2) = abs(i) | A User Theorem |
| inverse-ii | ⊦ sqrt(i * i) = abs(i) | A User Theorem |
| isSquare-one | ⊦ isSquare(1) | A User Theorem |
| isSquare-pos | ⊦ isSquare(i) → 0 ≤ i | A User Theorem |
| isSquare-square | ⊦ isSquare(i * i) | A User Theorem |
| isSquare-zero | ⊦ isSquare(0) | A User Theorem |
| le | ⊦ i ^2 ≤ j ^2 ↔ abs(i) ≤ abs(j) | A User Theorem |
| le-plus | ⊦ 0 ≤ i ∧ 0 < j → i ^2 < (i + j)^2 | A User Theorem |
| minus | ⊦ (~ i)^2 = i ^2 | A User Theorem |
| minus-01 | ⊦ i ^2 = (~ i)^2 | A User Theorem |
| neq | ⊦ j ^2 ≠ j * j ↔ false | A User Theorem |
| one | ⊦ 1 ^2 = 1 | A User Theorem |
| one-01 | ⊦ sqrt(1) = 1 | A User Theorem |
| positive | ⊦ i ^2 ≥ 0 | A User Theorem |
| root-abs | ⊦ 0 ≤ i → abs(sqrt(i)) = sqrt(i) | A User Theorem |
| root-elim | ⊦ 0 ≤ i → (∃ j, j0. i = j * j + j0 ∧ j0 ≤ 2 * j ∧ 0 ≤ j ∧ 0 ≤ j0 ∧ j = sqrt(i)) | A User Theorem |
| root-le | ⊦ i ≤ j ∧ 0 ≤ i ∧ 0 ≤ j → sqrt(i) ≤ sqrt(j) | A User Theorem |
| root-nls | ⊦ 0 ≤ i → ¬ i < sqrt(i) * sqrt(i) | A User Theorem |
| root-pos | ⊦ 0 ≤ i → 0 ≤ sqrt(i) | A User Theorem |
| sqrt-estimate | ⊦ j ^2 ≤ i ∧ i < (j + 1)^2 ∧ 0 ≤ j → sqrt(i) = j | A User Theorem |
| sqrt-isSquare | ⊦ isSquare(i) → sqrt(i) * sqrt(i) = i | A User Theorem |
| sqrt-mult-squares | ⊦ isSquare(i) ∧ isSquare(j) → sqrt(i * j) = sqrt(i) * sqrt(j) | A User Theorem |
| square-four | ⊦ sqrt(4) = 2 | A User Theorem |
| square-le-one | ⊦ 0 < i → (sqrt(i) ≤ 1 ↔ i < 4) | A User Theorem |
| square-le-one-01 | ⊦ 0 < i → (sqrt(2 * i) ≤ 1 ↔ i = 1) | A User Theorem |
| square-nls | ⊦ i ^2 ≤ j → ¬ sqrt(j) < i | A User Theorem |
| square-not-neg | ⊦ 0 ≤ i → ¬ sqrt(i) < 0 | A User Theorem |
| square-not-neg-01 | ⊦ 0 < i → ¬ sqrt(2 * i) < 0 | A User Theorem |
| square-not-neg-02 | ⊦ 0 ≤ i → (sqrt(i) ≤ 0 ↔ i = 0) | A User Theorem |
| square-not-neg-03 | ⊦ 0 < i → ¬ sqrt(2 * i) ≤ 0 | A User Theorem |
| square-not-neg-04 | ⊦ 0 < i → sqrt(2 * i) ≠ 0 | A User Theorem |
| square-not-neg-05 | ⊦ 0 < i → sqrt(i) ≠ 0 | A User Theorem |
| square-three | ⊦ sqrt(3) = 1 | A User Theorem |
| square-two | ⊦ sqrt(2) = 1 | A User Theorem |
| two-even | ⊦ 2 * i = j1 ^2 + j2 ^2 → i = ((j1 - j2) / 2)^2 + ((j1 + j2) / 2)^2 | A User Theorem |
| two-even-01 | ⊦ (j1 + j2) % 2 = 0 → j1 ^2 + j2 ^2 = 2 * (((j1 - j2) / 2)^2 + ((j1 + j2) / 2)^2) | A User Theorem |
| two-ex | ⊦ 2 * i = j1 ^2 + j2 ^2 → (∃ i1, i2. i = i1 ^2 + i2 ^2) | A User Theorem |
| two-identity | ⊦ (i1 ^2 + i2 ^2) * (j1 ^2 + j2 ^2) = (i1 * j1 + i2 * j2)^2 + (i1 * j2 - i2 * j1)^2 | A User Theorem |
| two-le-three | ⊦ i ^2 ≤ 3 ↔ abs(i) ≤ 1 | A User Theorem |
| two-le-two | ⊦ i ^2 ≤ 2 ↔ abs(i) ≤ 1 | A User Theorem |
| two-ls | ⊦ i ^2 < j ^2 ↔ abs(i) < abs(j) | A User Theorem |
| two-ls-pospos | ⊦ 0 ≤ i ∧ 0 ≤ j → (i ^2 < j ^2 ↔ i < j) | A User Theorem |
| two-minus | ⊦ (i - j)^2 = (i ^2 - 2 * i * j) + j ^2 | A User Theorem |
| two-mult | ⊦ (i * j)^2 = i ^2 * j ^2 | A User Theorem |
| two-not-neg | ⊦ ¬ i ^2 < 0 | A User Theorem |
| two-plus | ⊦ (i + j)^2 = i ^2 + 2 * i * j + j ^2 | A User Theorem |
| two-pm | ⊦ (i * i0 + j * j0)^2 = i ^2 * i0 ^2 + 2 * i * i0 * j * j0 + j ^2 * j0 ^2 | A User Theorem |
| zero | ⊦ i ^2 = 0 ↔ i = 0 | A User Theorem |
| zero-01 | ⊦ sqrt(0) = 0 | A User Theorem |
| zero-i | ⊦ 0 ^2 = 0 | A User Theorem |