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: |
|---|---|---|
| Equality | ⊦ dec_i = dec_j ↔ dec_i.int = dec_j.int ∧ dec_i.scale = dec_j.scale | An Axiom |
| intvalue-base | ⊦ ¬(i % 10 = 0 ∧ j ≠ 0 ∧ i ≠ 0) → mkDecimal(i, j).int = i | An Axiom |
| intvalue-rec | ⊦ i % 10 = 0 ∧ j ≠ 0 ∧ i ≠ 0 → mkDecimal(i, j).int = mkDecimal(i / 10, abs(j) - 1).int | An Axiom |
| scale-base | ⊦ ¬(i % 10 = 0 ∧ j ≠ 0 ∧ i ≠ 0) → mkDecimal(i, j).scale = abs(j) | An Axiom |
| scale-rec | ⊦ i % 10 = 0 ∧ j ≠ 0 ∧ i ≠ 0 → mkDecimal(i, j).scale = mkDecimal(i / 10, abs(j) - 1).scale | An Axiom |
| gen | An Axiom | |
| dec2int-def | ⊦ dec2int(dec) = dec.int / 10 ^ dec.scale | An Axiom |
| maxScale-rec | ⊦ i % 10 = 0 ∧ i ≠ 0 → maxScale(i) = maxScale(i / 10) + 1 | An Axiom |
| maxScale-base | ⊦ i % 10 ≠ 0 ∧ i ≠ 0 → maxScale(i) = 0 | An Axiom |
| maxScale-zero | ⊦ maxScale(0) = 0 | An Axiom |
| intvalue-zero | ⊦ mkDecimal(0, j).int = 0 | An Axiom |
| scale-zero | ⊦ mkDecimal(0, j).scale = 0 | An Axiom |
| truncate-nothing-def | ⊦ dec.scale ≤ abs(i) → truncate(dec, i) = dec | An Axiom |
| truncate-really-def | ⊦ abs(i) < dec.scale → truncate(dec, i) = mkDecimal(dec.int / 10 ^ (dec.scale - abs(i)), abs(i)) | An Axiom |
| inc-def | ⊦ inc(dec) = mkDecimal(dec.int + 1, dec.scale) | An Axiom |
| dec2int-def-any | ⊦ dec2int(mkDecimal(i, j)) = i / 10 ^ abs(j) | A User Theorem |
| dec2int-zero | ⊦ dec2int(mkDecimal(i, 0)) = i | A User Theorem |
| dec2int-zero-01 | ⊦ dec2int(mkDecimal(0, j)) = 0 | A User Theorem |
| eq-same | ⊦ mkDecimal(i, j) = mkDecimal(i0, j) ↔ i = i0 | A User Theorem |
| eq-zero | ⊦ mkDecimal(i, j) = mkDecimal(0, j0) ↔ i = 0 | A User Theorem |
| equality-any | ⊦ mkDecimal(i, j) = mkDecimal(i0, j0) ↔ i * 10 ^ abs(j0) = i0 * 10 ^ abs(j) | A User Theorem |
| ex-mkDecimal | ⊦ ∃ i, j. dec = mkDecimal(i, j) ∧ dec.int = i ∧ dec.scale = j ∧ 0 ≤ j | A User Theorem |
| getint-neg | ⊦ ~ mkDecimal(i, j).int = mkDecimal(~ i, j).int | A User Theorem |
| getint-neg-01 | ⊦ mkDecimal(~ i, j).int = ~ mkDecimal(i, j).int | A User Theorem |
| getint-neg-02 | ⊦ mkDecimal(i, j).int < 0 ↔ i < 0 | A User Theorem |
| getint-pos | ⊦ 0 < mkDecimal(i, j).int ↔ 0 < i | A User Theorem |
| getint-pos-01 | ⊦ 0 ≤ mkDecimal(i, j).int ↔ 0 ≤ i | A User Theorem |
| getint-zero | ⊦ mkDecimal(i, j).int = 0 ↔ i = 0 | A User Theorem |
| intvalue-mod-10 | ⊦ dec.scale ≠ 0 → dec.int % 10 ≠ 0 | A User Theorem |
| maxScale-le-zero | ⊦ maxScale(i) ≤ 0 ↔ maxScale(i) = 0 | A User Theorem |
| maxScale-min | ⊦ min(maxScale(i), 0) = 0 | A User Theorem |
| maxScale-not-negt | ⊦ ¬ maxScale(i) < 0 | A User Theorem |
| maxScale-pot10 | ⊦ 0 ≤ i → maxScale(10 ^ i) = i | A User Theorem |
| maxScale-pot10-01 | ⊦ i % 10 ≠ 0 ∧ 0 ≤ j → maxScale(i * 10 ^ j) = j | A User Theorem |
| maxScale-pot10-02 | ⊦ 0 ≤ j ∧ i ≠ 0 → maxScale(i * 10 ^ j) = maxScale(i) + j | A User Theorem |
| maxScale-pot10-add | ⊦ 0 ≤ j ∧ 0 ≤ j0 ∧ i % 10 ≠ 0 ∧ i0 % 10 ≠ 0 ∧ (i + i0) % 10 ≠ 0 → maxScale(i * 10 ^ j + i0 * 10 ^ j0) = min(j, j0) | A User Theorem |
| maxScale-pot10-nls | ⊦ 0 ≤ j ∧ i ≠ 0 → ¬ maxScale(i * 10 ^ j) < j | A User Theorem |
| maxScale-zero-01 | ⊦ (i / 10 ^ maxScale(i)) % 10 = 0 ↔ i = 0 | A User Theorem |
| mkDecimal-constructor | ⊦ mkDecimal(dec.int, dec.scale) = dec | A User Theorem |
| mkDecimal-enlarge | ⊦ 0 ≤ j0 → mkDecimal(i, j) = mkDecimal(i * 10 ^ j0, abs(j) + j0) | A User Theorem |
| mkDecimal-maxScale-le | ⊦ maxScale(i) ≤ abs(j) → mkDecimal(i, j) = mkDecimal(i / 10 ^ maxScale(i), abs(j) - maxScale(i)) | A User Theorem |
| mkDecimal-maxScale-le-int | ⊦ maxScale(i) ≤ abs(j) → mkDecimal(i, j).int = i / 10 ^ maxScale(i) | A User Theorem |
| mkDecimal-maxScale-le-scale | ⊦ maxScale(i) ≤ abs(j) → mkDecimal(i, j).scale = abs(j) - maxScale(i) | A User Theorem |
| mkDecimal-maxScale-nle | ⊦ ¬ maxScale(i) ≤ abs(j) → mkDecimal(i, j) = mkDecimal(i / 10 ^ abs(j), 0) | A User Theorem |
| mkDecimal-maxScale-nle-int | ⊦ ¬ maxScale(i) ≤ abs(j) → mkDecimal(i, j).int = i / 10 ^ abs(j) | A User Theorem |
| mkDecimal-maxScale-nle-scale | ⊦ ¬ maxScale(i) ≤ abs(j) → mkDecimal(i, j).scale = 0 | A User Theorem |
| mkDecimal-negated | ⊦ mkDecimal(mkDecimal(~ i, j).int, mkDecimal(i, j).scale) = mkDecimal(~ i, j) | A User Theorem |
| mkDecimal-rec | ⊦ i % 10 = 0 ∧ j ≠ 0 → mkDecimal(i, j) = mkDecimal(i / 10, abs(j) - 1) | A User Theorem |
| mkDecimal-reduce-int | ⊦ mkDecimal(i, j).int = i / 10 ^ min(maxScale(i), abs(j)) | A User Theorem |
| mkDecimal-reduce-scale | ⊦ mkDecimal(i, j).scale = max(0, abs(j) - maxScale(i)) | A User Theorem |
| mkDecimal-scale-not-neg | ⊦ mkDecimal(i, j) = mkDecimal(i, abs(j)) | A User Theorem |
| mkDecimal-selectors | ⊦ dec = mkDecimal(dec.int, dec.scale) | A User Theorem |
| mkDecimal-zero | ⊦ mkDecimal(0, j) = mkDecimal(0, 0) | A User Theorem |
| scale-le | ⊦ mkDecimal(i, j).scale ≤ abs(j) | A User Theorem |
| scale-negate | ⊦ mkDecimal(~ i, j).scale = mkDecimal(i, j).scale | A User Theorem |
| scale-neq | ⊦ abs(j) < j0 → mkDecimal(i, j).scale ≠ j0 | A User Theorem |
| scale-neq-01 | ⊦ j ≠ 0 → mkDecimal(i, abs(j) - 1).scale ≠ abs(j) | A User Theorem |
| scale-not-neg | ⊦ ¬ dec.scale < 0 | A User Theorem |
| test-inc-01 | ⊦ inc(mkDecimal(99, 2)) = mkDecimal(1, 0) | A User Theorem |
| test-truncate-01 | ⊦ truncate(mkDecimal(314159265358979323844, 20), 2) = mkDecimal(314, 2) | A User Theorem |