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: |
|---|---|---|
| div-def | ⊦ dec_i / dec_j = div(dec_i, dec_j, 0) | An Axiom |
| div-precision-def | ⊦ ¬ dec_j | dec_i → div(dec_i, dec_j, i) = mkDecimal((dec_i.int * 10 ^ (dec_j.scale + abs(i))) / dec_j.int / 10 ^ maxScale(dec_j.int), dec_i.scale + abs(i) + maxScale(dec_j.int)) | An Axiom |
| div-exact-def | ⊦ dec_j | dec_i → div(dec_i, dec_j, i) * dec_j = dec_i | An Axiom |
| divides-def | ⊦ dec_j | dec_i ↔ (∃ dec_j0. dec_j * dec_j0 = dec_i) | An Axiom |
| sqrt-def | ⊦ sqrt(dec) = sqrt(dec, 0) | An Axiom |
| isSquare-def | ⊦ isSquare(dec_i) ↔ (∃ dec. dec * dec = dec_i) | An Axiom |
| sqrt-odd-precision-def | ⊦ odd(dec_i.scale) → sqrt(dec_i, i) = mkDecimal(sqrt(dec_i.int * 10 ^ (2 * abs(i) + 1)), (dec_i.scale + 1) / 2 + abs(i)) | An Axiom |
| sqrt-even-precision-def | ⊦ even(dec_i.scale) → sqrt(dec_i, i) = mkDecimal(sqrt(dec_i.int * 10 ^ (2 * abs(i))), dec_i.scale / 2 + abs(i)) | An Axiom |
| isSquare-isSquare | ⊦ isSquare(dec) ↔ isSquare(dec.int) ∧ dec.scale % 2 = 0 | A User Theorem |
| isSquare-pos | ⊦ isSquare(dec) → 0_dec ≤ dec | A User Theorem |
| isSquare-scale | ⊦ isSquare(dec) → even(dec.scale) | A User Theorem |
| isSquare-square | ⊦ isSquare(dec * dec) | A User Theorem |
| sqrt-exact-def | ⊦ isSquare(dec) → sqrt(dec, i) = mkDecimal(sqrt(dec.int), dec.scale / 2) | A User Theorem |
| sqrt-exact-square | ⊦ dec0 * dec0 = dec ∧ 0_dec ≤ dec0 → sqrt(dec, i) = dec0 | A User Theorem |
| sqrt-isSquare | ⊦ isSquare(dec) → sqrt(dec, i) * sqrt(dec, i) = dec | A User Theorem |
| test-div-01 | ⊦ div(mkDecimal(1, 0), mkDecimal(3, 0), 4) = mkDecimal(3333, 4) | A User Theorem |
| test-div-02 | ⊦ mkDecimal(5, 0) / mkDecimal(2, 0) = mkDecimal(25, 1) | A User Theorem |
| test-div-03 | ⊦ mkDecimal(1, 0) / mkDecimal(1000, 0) = mkDecimal(1, 3) | A User Theorem |
| test-div-04 | ⊦ mkDecimal(5540535, 4) / mkDecimal(45, 4) = mkDecimal(123123, 0) | A User Theorem |
| test-divides-01 | ⊦ ¬ mkDecimal(3, 0) | mkDecimal(1, 0) | A User Theorem |
| test-divides-02 | ⊦ mkDecimal(2, 0) | mkDecimal(5, 0) | A User Theorem |
| test-divides-03 | ⊦ mkDecimal(1000, 0) | mkDecimal(1, 0) | A User Theorem |
| test-divides-04 | ⊦ mkDecimal(45, 4) | mkDecimal(5540535, 4) | A User Theorem |
| test-sqrt-01 | ⊦ sqrt(mkDecimal(144, 2)) = mkDecimal(12, 1) | A User Theorem |
| test-sqrt-02 | ⊦ sqrt(mkDecimal(2, 0), 2) = mkDecimal(141, 2) | A User Theorem |
| test-sqrt-03 | ⊦ sqrt(mkDecimal(144, 1), 3) = mkDecimal(37947, 4) | A User Theorem |
| test-sqrt-04 | ⊦ sqrt(mkDecimal(29, 4), 3) = mkDecimal(5385, 5) | A User Theorem |
| test-sqrt-05 | ⊦ sqrt(mkDecimal(29, 5), 3) = mkDecimal(17029, 6) | A User Theorem |