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: |
|---|---|---|
| numerator-zero | ⊦ rational(0, j).num = 0 | An Axiom |
| numerator-pos | ⊦ i ≠ 0 ∧ 0 < j → rational(i, j).num = i / gcd(i, j) | An Axiom |
| numerator-neg1 | ⊦ 0 < i ∧ j < 0 → rational(i, j).num = ~(i / gcd(i, j)) | An Axiom |
| numerator-neg2 | ⊦ i < 0 ∧ j < 0 → rational(i, j).num = abs(i) / gcd(i, j) | An Axiom |
| denominator-zero | ⊦ rational(0, j).denom = 1 | An Axiom |
| denominator-pos | ⊦ i ≠ 0 ∧ j ≠ 0 → rational(i, j).denom = abs(j) / gcd(i, j) | An Axiom |
| zero-def | ⊦ 0r = rational(0, 1) | An Axiom |
| one-def | ⊦ 1r = rational(1, 1) | An Axiom |
| add-def | ⊦ ri + rj = rational(ri.num * rj.denom + ri.denom * rj.num, ri.denom * rj.denom) | An Axiom |
| sub-def | ⊦ ri - rj = rational(ri.num * rj.denom - ri.denom * rj.num, ri.denom * rj.denom) | An Axiom |
| mult-def | ⊦ ri * rj = rational(ri.num * rj.num, ri.denom * rj.denom) | An Axiom |
| div-def | ⊦ ri / rj = rational(ri.num * rj.denom, ri.denom * rj.num) | An Axiom |
| neg-def | ⊦ ~ ri = 0r - ri | An Axiom |
| abs-def | ⊦ abs(ri) = rational(abs(ri.num), ri.denom) | An Axiom |
| Ls-def | ⊦ ri < rj ↔ (ri - rj).num < 0 | An Axiom |
| Le-def | ⊦ ri ≤ rj ↔ ¬ rj < ri | An Axiom |
| Gr-def | ⊦ ri > rj ↔ rj < ri | An Axiom |
| Ge-def | ⊦ ri ≥ rj ↔ ¬ ri < rj | An Axiom |
| gen | An Axiom | |
| Equality | ⊦ ri = rj ↔ ri.num = rj.num ∧ ri.denom = rj.denom | An Axiom |
| denominator-zero-den | ⊦ i ≠ 0 → rational(i, 0).denom = 1 | An Axiom |
| numerator-zero-den | ⊦ i ≠ 0 → rational(i, 0).num = i | An Axiom |
| Extsimple | ⊦ i1 ≠ 0 ∧ i2 ≠ 0 ∧ j1 ≠ 0 ∧ j2 ≠ 0 → ( rational(i1, j1) = rational(i2, j2) ↔ abs(i1) / gcd(i1, j1) = abs(i2) / gcd(i2, j2) ∧ abs(j1) / gcd(i1, j1) = abs(j2) / gcd(i2, j2) ∧ ( (0 < i1 ∧ 0 < j1 ∨ i1 < 0 ∧ j1 < 0) ∧ (0 < i2 ∧ 0 < j2 ∨ i2 < 0 ∧ j2 < 0) ∨ (0 < i1 ∧ j1 < 0 ∨ i1 < 0 ∧ 0 < j1) ∧ (0 < i2 ∧ j2 < 0 ∨ i2 < 0 ∧ 0 < j2))) | A User Theorem |
| abs-num | ⊦ abs(rj).num = abs(rj.num) | A User Theorem |
| abs-pos | ⊦ 0 < j → abs(rational(i, j)) = rational(abs(i), j) | A User Theorem |
| add-asso | ⊦ (ri + rj) + rj0 = ri + rj + rj0 | A User Theorem |
| add-comm | ⊦ ri + rj = rj + ri | A User Theorem |
| add-def-01 | 0 < j1, 0 < j2, gcd(i1, j1) = 1, gcd(i2, j2) = 1 ⊦ rational(i1, j1) + rational(i2, j2) = rational(i1 * j2 + j1 * i2, j1 * j2) | A User Theorem |
| add-def-02 | 0 < j1, 0 < j2 ⊦ rational(i1, j1) + rational(i2, j2) = rational(i1 * j2 + j1 * i2, j1 * j2) | A User Theorem |
| add-def-03 | ⊦ j1 ≠ 0 ∧ j2 ≠ 0 → rational(i1, j1) + rational(i2, j2) = rational(i1 * j2 + j1 * i2, j1 * j2) | A User Theorem |
| add-eq | ⊦ ri + rj = ri + rj0 ↔ rj = rj0 | A User Theorem |
| add-zero | ⊦ ri + 0r = ri | A User Theorem |
| add-zero-01 | ⊦ rational(0, j1) + rational(i0, j0) = rational(i0, j0) | A User Theorem |
| add-zero-02 | ⊦ rational(0, j) + rj = rj | A User Theorem |
| canon-any | ⊦ 0 < j → rational(i, j) = rational(i / gcd(i, j), j / gcd(i, j)) | A User Theorem |
| canon-pos | ⊦ 0 ≤ i ∧ 0 < j → rational(i, j) = rational(i / gcd(i, j), j / gcd(i, j)) | A User Theorem |
| denom-id | ⊦ gcd(i, j) = 1 ∧ 0 < j → rational(i, j).denom = j | A User Theorem |
| denom-neg | ⊦ j < 0 → rational(i, j) = rational(~ i, abs(j)) | A User Theorem |
| denom-neg-01 | ⊦ rational(~ i, j).denom = rational(i, j).denom | A User Theorem |
| denom-neg-02 | ⊦ (~ ri).denom = ri.denom | A User Theorem |
| denom-not-zero | ⊦ ri.denom ≠ 0 | A User Theorem |
| denom-one | ⊦ rational(i, 1).denom = 1 | A User Theorem |
| denom-pos | ⊦ ¬ rj.denom < 0 | A User Theorem |
| denom-pos-01 | ⊦ ¬ rj.denom ≤ 0 | A User Theorem |
| denum-same | ⊦ rational(abs(rj.num), rj.denom).denom = rj.denom | A User Theorem |
| denum-same-01 | ⊦ rational(rj.num, rj.denom).denom = rj.denom | A User Theorem |
| denum-same-02 | ⊦ rational(abs(rj).num, rj.denom).denom = rj.denom | A User Theorem |
| distributivity | ⊦ ri * (rj + rj0) = ri * rj + ri * rj0 | A User Theorem |
| div-def-01 | ⊦ 0 < j ∧ 0 < j0 ∧ i0 ≠ 0 → rational(i, j) / rational(i0, j0) = rational(i * j0, j * i0) | A User Theorem |
| div-neg | ⊦ rj ≠ 0r → ~ ri / rj = ~(ri / rj) | A User Theorem |
| div-neg-01 | ⊦ rj ≠ 0r → ri / ~ rj = ~(ri / rj) | A User Theorem |
| div-pos-def | ⊦ 0 < i ∧ 0 < i0 ∧ 0 < j ∧ 0 < j0 → rational(i, j) / rational(i0, j0) = rational(i * j0, j * i0) | A User Theorem |
| elim-sub | ⊦ ri0 = ri - rj ↔ ri = ri0 + rj | A User Theorem |
| equal-same | ⊦ 0 < j → (rational(i, j) = rational(i0, j) ↔ i = i0) | A User Theorem |
| equality-01 | rational(i, j) = rational(i0, j0), 0 < j, 0 < j0 ⊦ i * j0 = i0 * j | A User Theorem |
| equality-02 | i * j0 = i0 * j, 0 < j, 0 < j0 ⊦ rational(i, j) = rational(i0, j0) | A User Theorem |
| equality-def | ⊦ 0 < j ∧ 0 < j0 → (rational(i, j) = rational(i0, j0) ↔ i * j0 = i0 * j) | A User Theorem |
| equality-pos | i * j0 = i0 * j, 0 < j, 0 < j0, 0 < i, 0 < i0 ⊦ rational(i, j) = rational(i0, j0) | A User Theorem |
| exrat | ⊦ ∃ i, j. ri = rational(i, j) ∧ ri.num = i ∧ ri.denom = j ∧ 0 < j | A User Theorem |
| exrat-01 | ⊦ ∃ i, j. ri = rational(i, j) ∧ 0 < j | A User Theorem |
| exrat-gcd1 | ri ≠ 0r ⊦ ∃ i, j. ri = rational(i, j) ∧ ri.num = i ∧ ri.denom = j ∧ 0 < j ∧ gcd(i, j) = 1 | A User Theorem |
| factor-rat | ⊦ j ≠ 0 ∧ i1 ≠ 0 → rational(i * i1, j * i1) = rational(i, j) | A User Theorem |
| factor-rat-01 | ⊦ j ≠ 0 ∧ i1 ≠ 0 → rational(i1 * i, i1 * j) = rational(i, j) | A User Theorem |
| factor-rat-02 | ⊦ 0 < j ∧ i1 ≠ 0 → rational(i1 * i, i1 * j) = rational(i, j) | A User Theorem |
| factor-rat-03 | ⊦ 0 < j ∧ 0 < i1 → rational(i1 * i, i1 * j) = rational(i, j) | A User Theorem |
| gcd-num-one | ⊦ rj.num ≠ 0 → gcd(rj.num, rj.denom) = 1 | A User Theorem |
| int-add | ⊦ rational(i, 1) + rational(j, 1) = rational(i + j, 1) | A User Theorem |
| int-mult | ⊦ rational(i, 1) * rational(j, 1) = rational(i * j, 1) | A User Theorem |
| int2rat-equal | ⊦ i = j ↔ rational(i, 1) = rational(j, 1) | A User Theorem |
| irreflexivity | ⊦ ¬ ri < ri | A User Theorem |
| ls-def | ⊦ 0 < j ∧ 0 < j0 → (rational(i, j) < rational(i0, j0) ↔ i * j0 < i0 * j) | A User Theorem |
| make | ⊦ rational(ri.num, ri.denom) = ri | A User Theorem |
| mult-ass | ⊦ (ri * rj) * rj1 = ri * rj * rj1 | A User Theorem |
| mult-comm | ⊦ ri * rj = rj * ri | A User Theorem |
| mult-def-01 | gcd(i1, j1) = 1, gcd(i2, j2) = 1, 0 < j1, 0 < j2 ⊦ rational(i1, j1) * rational(i2, j2) = rational(i1 * i2, j1 * j2) | A User Theorem |
| mult-def-02 | 0 < j1, 0 < j2 ⊦ rational(i1, j1) * rational(i2, j2) = rational(i1 * i2, j1 * j2) | A User Theorem |
| mult-def-03 | ⊦ j1 ≠ 0 ∧ j2 ≠ 0 → rational(i1, j1) * rational(i2, j2) = rational(i1 * i2, j1 * j2) | A User Theorem |
| mult-one | ⊦ ri * 1r = ri | A User Theorem |
| mult-one-01 | ⊦ rational(1, 1) * rj = rj | A User Theorem |
| mult-split | ⊦ i = i0 + i1 → ri + rational(i0, 1) * rj + rational(i1, 1) * rj = ri + rational(i, 1) * rj | A User Theorem |
| mult-zero | ⊦ ri * 0r = 0r | A User Theorem |
| mult-zero-01 | ⊦ ri * rational(0, j) = 0r | A User Theorem |
| neg-intro | ⊦ j ≠ 0 → rational(i, ~ j) = rational(~ i, j) | A User Theorem |
| neg-neg | ⊦ j ≠ 0 → rational(~ i, ~ j) = rational(i, j) | A User Theorem |
| negate | ⊦ 0 < j → rational(~ i, j) = ~ rational(i, j) | A User Theorem |
| negate-01 | ⊦ rational(~ i, j) = ~ rational(i, j) | A User Theorem |
| negate-02 | ⊦ ~ ~ ri = ri | A User Theorem |
| negate-eq | ⊦ ~ ri = ~ rj ↔ ri = rj | A User Theorem |
| num-div-denom | ⊦ i1 ≠ 0 → rational(i, i1).num / rational(i, i1).denom = i / i1 | A User Theorem |
| num-div-denom-01 | ⊦ i1 ≠ 0 ∧ j ≠ 0 → (rational(i, i1).num * j) / rational(i, i1).denom = (i * j) / i1 | A User Theorem |
| num-id | ⊦ gcd(i, j) = 1 ∧ 0 < j → rational(i, j).num = i | A User Theorem |
| num-neg | ⊦ j ≠ 0 → rational(~ i, ~ j).num = rational(i, j).num | A User Theorem |
| num-neg-01 | ⊦ rational(~ i, j).num = ~ rational(i, j).num | A User Theorem |
| num-neg-02 | ⊦ 0 < j → (rational(i, j).num < 0 ↔ i < 0) | A User Theorem |
| num-neg-03 | ⊦ (~ ri).num = ~ ri.num | A User Theorem |
| num-pos | ⊦ 0 < i ∧ 0 < j → rational(i, j).num = i / gcd(i, j) | A User Theorem |
| num-same | ⊦ rational(ri.num, ri.denom).num = ri.num | A User Theorem |
| num-same-01 | ⊦ rational(abs(ri.num), ri.denom).num = abs(ri).num | A User Theorem |
| num-same-02 | ⊦ rational(abs(ri).num, ri.denom).num = abs(ri).num | A User Theorem |
| num-zero | ⊦ rational(i, j).num = 0 ↔ i = 0 | A User Theorem |
| num-zero-denum-one | ⊦ rj.num = 0 → rj.denom = 1 | A User Theorem |
| one | ⊦ i ≠ 0 → rational(i, i) = rational(1, 1) | A User Theorem |
| rational-add-same | ⊦ rational(i, j) + rational(i1, j) = rational(i + i1, j) | A User Theorem |
| root-is-irrational | ⊦ ri * ri = rational(j, 1) → (∃ i. j = i * i) | A User Theorem |
| sub-def-01 | ⊦ 0 < j1 ∧ 0 < j2 → rational(i1, j1) - rational(i2, j2) = rational(i1, j1) + rational(~ i2, j2) | A User Theorem |
| totality | ⊦ ri < rj ∨ ri = rj ∨ rj < ri | A User Theorem |
| transitivity | ⊦ ri < rj ∧ rj < rj0 → ri < rj0 | A User Theorem |
| zero-denom | ⊦ rational(i, 0) = rational(i, 1) | A User Theorem |
| zero-num | ⊦ rational(0, j) = rational(0, 1) | A User Theorem |
| zero-num-01 | ⊦ rational(0, i * j) = rational(0, 1) | A User Theorem |
| zero-num-02 | ⊦ rational(0, i / j) = rational(0, 1) | A User Theorem |