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: |
|---|---|---|
| Max-right | ⊦ j < i → max(j, i) = i | An Axiom |
| Max-left | ⊦ ¬ j < i → max(j, i) = j | An Axiom |
| Min-left | ⊦ j < i → min(j, i) = j | An Axiom |
| Min-right | ⊦ ¬ j < i → min(j, i) = i | An Axiom |
| Sign-pos | ⊦ ¬ j < 0 → sgn(j) = 0 +1 | An Axiom |
| Sign-neg | ⊦ j < 0 → sgn(j) = 0 -1 | An Axiom |
| odd-def | ⊦ odd(i) ↔ (∃ j. i = j + j + 1) | An Axiom |
| even-def | ⊦ even(i) ↔ (∃ j. i = j + j) | An Axiom |
| even-2 | ⊦ even(2) | A User Theorem |
| even-add | ⊦ even(i + j) ↔ even(i) ∧ even(j) ∨ odd(i) ∧ odd(j) | A User Theorem |
| even-def-mod | ⊦ even(i) ↔ i % 2 = 0 | A User Theorem |
| even-mult | ⊦ even(i * j) ↔ even(i) ∨ even(j) | A User Theorem |
| even-not | ⊦ ¬ even(i) → ¬ even(i - 2) | A User Theorem |
| even-odd-rew | ⊦ even(i) ↔ ¬ odd(i) | A User Theorem |
| even-rec | ⊦ even(i) ↔ even(i - 2) | A User Theorem |
| even-zero | ⊦ even(0) | A User Theorem |
| max | ⊦ max(i, j) = j ↔ ¬ j < i | A User Theorem |
| max-01 | ⊦ max(i, j) < j0 ↔ i < j0 ∧ j < j0 | A User Theorem |
| max-02 | ⊦ max(i, j) = j0 → i = j0 ∨ j = j0 | A User Theorem |
| max-03 | ⊦ i < j0 ∧ j < j0 → max(i, j) < j0 | A User Theorem |
| max-04 | ⊦ ¬ max(i, j) < i | A User Theorem |
| max-a | ⊦ max(i, max(j, j0)) = max(max(i, j), j0) | A User Theorem |
| max-c | ⊦ max(i, j) = max(j, i) | A User Theorem |
| min | ⊦ j0 < i ∧ j0 < j → min(i, j) ≠ j0 | A User Theorem |
| min-01 | ⊦ j0 < i ∧ j0 < j → j0 < min(i, j) | A User Theorem |
| min-02 | ⊦ j0 < i ∧ j0 < j → ¬ min(i, j) < j0 | A User Theorem |
| min-03 | ⊦ ¬ i < min(i, j) | A User Theorem |
| min-a | ⊦ min(i, min(j, j0)) = min(min(i, j), j0) | A User Theorem |
| min-abs-zero | ⊦ min(0, abs(j)) = 0 | A User Theorem |
| min-abs-zero-01 | ⊦ ¬ min(abs(i), abs(j)) < 0 | A User Theorem |
| min-c | ⊦ min(i, j) = min(j, i) | A User Theorem |
| min-right | ⊦ j ≤ i → min(i, j) = j | A User Theorem |
| not-even-mod2 | ⊦ i % 2 ≠ 0 → ¬ even(i) | A User Theorem |
| not-even-odd | ⊦ ¬ even(i) ↔ odd(i) | A User Theorem |
| not-odd-ex | ⊦ ¬ odd(i) ↔ (∃ j. i = j + j) | A User Theorem |
| odd-add | ⊦ odd(i + j) ↔ odd(i) ∧ even(j) ∨ even(i) ∧ odd(j) | A User Theorem |
| odd-def-mod | ⊦ odd(i) ↔ i % 2 ≠ 0 | A User Theorem |
| odd-even-rew | ⊦ odd(i) ↔ ¬ even(i) | A User Theorem |
| odd-one | ⊦ odd(1) | A User Theorem |
| odd-rec | ⊦ 1 < i → (odd(i) ↔ odd(i - 2)) | A User Theorem |
| odd-two | ⊦ ¬ odd(2) | A User Theorem |
| odd-zero | ⊦ ¬ odd(0) | A User Theorem |
| sgn | ⊦ sgn(i) ≠ 1 ↔ sgn(i) = ~1 | A User Theorem |
| sgn+1 | ⊦ 0 ≤ j → sgn(j) = 1 | A User Theorem |
| sgn-01 | ⊦ sgn(i) = 1 ↔ 0 ≤ i | A User Theorem |
| sgn-01-01 | ⊦ i < 0 → sgn(i) * j = ~ j | A User Theorem |
| sgn-02 | ⊦ sgn(i) = ~1 ↔ i < 0 | A User Theorem |
| sgn-02-01 | ⊦ sgn(i) * j = sgn(i) * j0 ↔ j = j0 | A User Theorem |
| sgn-03 | ⊦ sgn(i) = 1 ∨ sgn(i) = ~1 | A User Theorem |
| sgn-04 | ⊦ j ≤ i → sgn(i - j) = 1 | A User Theorem |
| sgn-05 | ⊦ j + j0 ≤ i → sgn(i - j0 + j) = 1 | A User Theorem |
| sgn-06 | ⊦ i < j → sgn(i - j) = ~1 | A User Theorem |
| sgn-07 | ⊦ i < j + j0 → sgn(i - j0 + j) = ~1 | A User Theorem |
| sgn-08 | ⊦ sgn(i) ≠ 0 | A User Theorem |
| sgn-09 | ⊦ 0 ≤ i → sgn(i) * j = j | A User Theorem |
| sgn-1 | ⊦ j < 0 → sgn(j) = ~1 | A User Theorem |
| sr | ⊦ sgn(i) ≠ 1 → sgn(i) = ~1 | A User Theorem |