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: |
|---|---|---|
| zero-def | ⊦ 0_dec = mkDecimal(0, 0) | An Axiom |
| one-def | ⊦ 1_dec = mkDecimal(1, 0) | An Axiom |
| add-def | ⊦ dec_i + dec_j = mkDecimal(dec_i.int * 10 ^ dec_j.scale + dec_j.int * 10 ^ dec_i.scale, dec_i.scale + dec_j.scale) | An Axiom |
| sub-def | ⊦ dec_i - dec_j = mkDecimal(dec_i.int * 10 ^ dec_j.scale - dec_j.int * 10 ^ dec_i.scale, dec_i.scale + dec_j.scale) | An Axiom |
| mult-def | ⊦ dec_i * dec_j = mkDecimal(dec_i.int * dec_j.int, dec_i.scale + dec_j.scale) | An Axiom |
| neg-def | ⊦ ~ dec_i = mkDecimal(~ dec_i.int, dec_i.scale) | An Axiom |
| abs-def | ⊦ abs(dec_i) = mkDecimal(abs(dec_i.int), dec_i.scale) | An Axiom |
| ls-def | ⊦ dec_i < dec_j ↔ (dec_i - dec_j).int < 0 | An Axiom |
| le-def | ⊦ dec_i ≤ dec_j ↔ ¬ dec_j < dec_i | An Axiom |
| gr-def | ⊦ dec_i > dec_j ↔ dec_j < dec_i | An Axiom |
| ge-def | ⊦ dec_i ≥ dec_j ↔ ¬ dec_i < dec_j | An Axiom |
| abs-any-def | ⊦ abs(mkDecimal(i, j)) = mkDecimal(abs(i), j) | A User Theorem |
| abs-neg | ⊦ dec < mkDecimal(0, 0) → abs(dec) = ~ dec | A User Theorem |
| abs-not-neg | ⊦ mkDecimal(0, 0) ≤ abs(dec) | A User Theorem |
| abs-pos | ⊦ mkDecimal(0, 0) ≤ dec → abs(dec) = dec | A User Theorem |
| abs-zero | ⊦ abs(mkDecimal(0, 0)) = mkDecimal(0, 0) | A User Theorem |
| add-a | ⊦ dec0 + dec1 + dec2 = (dec0 + dec1) + dec2 | A User Theorem |
| add-c | ⊦ dec_i + dec_j = dec_j + dec_i | A User Theorem |
| add-def-any | ⊦ mkDecimal(i, j) + mkDecimal(i0, j0) = mkDecimal(i * 10 ^ abs(j0) + i0 * 10 ^ abs(j), abs(j) + abs(j0)) | A User Theorem |
| add-pos | ⊦ mkDecimal(0, 0) ≤ dec_i ∧ mkDecimal(0, 0) ≤ dec_j → mkDecimal(0, 0) ≤ dec_i + dec_j | A User Theorem |
| add-same | ⊦ mkDecimal(i, j) + mkDecimal(i0, j) = mkDecimal(i + i0, j) | A User Theorem |
| add-scale-eq | ⊦ dec_i.scale = dec_j.scale ∧ dec_i.int + dec_j.int ≠ 0 → (dec_i + dec_j).scale ≤ dec_i.scale | A User Theorem |
| add-scale-neq | ⊦ dec_i.scale ≠ dec_j.scale → (dec_i + dec_j).scale = max(dec_i.scale, dec_j.scale) | A User Theorem |
| add-zero | ⊦ dec_i + 0_dec = dec_i | A User Theorem |
| add-zero-01 | ⊦ dec_i + mkDecimal(0, j) = dec_i | A User Theorem |
| dec2int-not-neg | ⊦ mkDecimal(0, 0) ≤ dec → ¬ dec2int(dec) < 0 | A User Theorem |
| getint-abs | ⊦ abs(dec).int = abs(dec.int) | A User Theorem |
| le-add | ⊦ dec + mkDecimal(i, j) ≤ mkDecimal(i0, j) ↔ dec ≤ mkDecimal(i0 - i, j) | A User Theorem |
| le-add-01 | ⊦ mkDecimal(i, j) ≤ dec + mkDecimal(i0, j) ↔ mkDecimal(i - i0, j) ≤ dec | A User Theorem |
| le-ls-neq | ⊦ dec ≤ dec0 ↔ dec < dec0 ∨ dec = dec0 | A User Theorem |
| le-ls-trans | ⊦ dec ≤ dec0 ∧ dec0 < dec1 → dec < dec1 | A User Theorem |
| le-pos | ⊦ mkDecimal(0, 0) ≤ dec ↔ 0 ≤ dec.int | A User Theorem |
| le-ref | ⊦ dec ≤ dec | A User Theorem |
| le-same | ⊦ mkDecimal(i, j) ≤ mkDecimal(i0, j) ↔ i ≤ i0 | A User Theorem |
| le-trans | ⊦ dec ≤ dec0 ∧ dec0 ≤ dec1 → dec ≤ dec1 | A User Theorem |
| le-zero | ⊦ mkDecimal(0, 0) ≤ mkDecimal(i, j) ↔ 0 ≤ i | A User Theorem |
| less-def-any | ⊦ mkDecimal(i, j) < mkDecimal(i0, j0) ↔ i * 10 ^ abs(j0) < i0 * 10 ^ abs(j) | A User Theorem |
| less-irref | ⊦ ¬ dec < dec | A User Theorem |
| less-same | ⊦ mkDecimal(i, j) < mkDecimal(i0, j) ↔ i < i0 | A User Theorem |
| less-totality | ⊦ dec < dec0 ∨ dec = dec0 ∨ dec0 < dec | A User Theorem |
| less-trans | ⊦ dec < dec0 ∧ dec0 < dec1 → dec < dec1 | A User Theorem |
| ls-add | ⊦ dec + mkDecimal(i, j) < mkDecimal(i0, j) ↔ dec < mkDecimal(i0 - i, j) | A User Theorem |
| ls-add-01 | ⊦ mkDecimal(i, j) < dec + mkDecimal(i0, j) ↔ mkDecimal(i - i0, j) < dec | A User Theorem |
| ls-add-02 | ⊦ dec_i + dec_j < dec_j ↔ dec_i < mkDecimal(0, 0) | A User Theorem |
| ls-le-trans | ⊦ dec < dec0 ∧ dec0 ≤ dec1 → dec < dec1 | A User Theorem |
| ls-not | ⊦ ¬ dec < dec0 ↔ dec0 ≤ dec | A User Theorem |
| ls-zero | ⊦ mkDecimal(0, 0) < mkDecimal(i, j) ↔ 0 < i | A User Theorem |
| ls-zero-01 | ⊦ mkDecimal(i, i0) < mkDecimal(0, 0) ↔ i < 0 | A User Theorem |
| mult-a | ⊦ dec0 * dec1 * dec2 = (dec0 * dec1) * dec2 | A User Theorem |
| mult-abs | ⊦ abs(dec * dec0) = abs(dec) * abs(dec0) | A User Theorem |
| mult-c | ⊦ dec_i * dec_j = dec_j * dec_i | A User Theorem |
| mult-def-any | ⊦ mkDecimal(i, j) * mkDecimal(i0, j0) = mkDecimal(i * i0, abs(j) + abs(j0)) | A User Theorem |
| mult-dist | ⊦ dec * (dec_i + dec_j) = dec * dec_i + dec * dec_j | A User Theorem |
| mult-eq-same | ⊦ dec ≠ mkDecimal(0, 0) → (dec_i * dec = dec_j * dec ↔ dec_i = dec_j) | A User Theorem |
| mult-le | ⊦ mkDecimal(0, 0) < dec → (dec * dec_i ≤ dec * dec_j ↔ dec_i ≤ dec_j) | A User Theorem |
| mult-ls | ⊦ mkDecimal(0, 0) < dec → (dec * dec_i < dec * dec_j ↔ dec_i < dec_j) | A User Theorem |
| mult-one | ⊦ dec_i * 1_dec = dec_i | A User Theorem |
| mult-pos | ⊦ mkDecimal(0, 0) ≤ dec_i ∧ mkDecimal(0, 0) ≤ dec_j → mkDecimal(0, 0) ≤ dec_i * dec_j | A User Theorem |
| mult-pos-02 | ⊦ mkDecimal(0, 0) ≤ dec_i ∧ mkDecimal(0, 0) ≤ dec_j → ¬ dec_i * dec_j < mkDecimal(0, 0) | A User Theorem |
| mult-zero | ⊦ dec_i * 0_dec = 0_dec | A User Theorem |
| mult-zero-01 | ⊦ mkDecimal(0, 0) * dec = mkDecimal(0, 0) | A User Theorem |
| neg-any-def | ⊦ mkDecimal(~ i, j) = ~ mkDecimal(i, j) | A User Theorem |
| scale-abs | ⊦ abs(dec).scale = dec.scale | A User Theorem |
| square-abs | ⊦ abs(dec * dec) = dec * dec | A User Theorem |
| square-int-nlz | ⊦ ¬ (dec * dec).int < 0 | A User Theorem |
| square-isSquare | ⊦ isSquare((dec * dec).int) | A User Theorem |
| square-ls | ⊦ dec * dec < dec0 * dec0 ↔ abs(dec) < abs(dec0) | A User Theorem |
| square-pos | ⊦ mkDecimal(0, 0) ≤ dec * dec | A User Theorem |
| square-pos-01 | ⊦ mkDecimal(0, 0) < dec * dec ↔ dec ≠ mkDecimal(0, 0) | A User Theorem |
| square-scale | ⊦ even((dec * dec).scale) | A User Theorem |
| square-scale-01 | ⊦ (dec * dec).scale % 2 = 0 | A User Theorem |
| square-sqrt | ⊦ mkDecimal(0, 0) ≤ dec → mkDecimal(sqrt((dec * dec).int), (dec * dec).scale / 2) = dec | A User Theorem |
| square-sqrt-01 | ⊦ mkDecimal(sqrt((dec * dec).int), (dec * dec).scale / 2) * mkDecimal(sqrt((dec * dec).int), (dec * dec).scale / 2) = dec * dec | A User Theorem |
| square-sqrt-02 | ⊦ dec.scale % 2 = 0 ∧ isSquare(dec.int) → mkDecimal(sqrt(dec.int), dec.scale / 2) * mkDecimal(sqrt(dec.int), dec.scale / 2) = dec | A User Theorem |
| sub-add | ⊦ dec_i + dec_j - dec_j = dec_i | A User Theorem |
| sub-def-any | ⊦ mkDecimal(i, j) - mkDecimal(i0, j0) = mkDecimal(i * 10 ^ abs(j0) - i0 * 10 ^ abs(j), abs(j) + abs(j0)) | A User Theorem |
| sub-id | ⊦ dec - dec = mkDecimal(0, 0) | A User Theorem |
| sub-same | ⊦ mkDecimal(i, j) - mkDecimal(i0, j) = mkDecimal(i - i0, j) | A User Theorem |
| sub-zero | ⊦ dec - mkDecimal(0, i) = dec | A User Theorem |