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: |
|---|---|---|
| sgn-0 | ⊦ sgn(0) = 0 | An Axiom |
| sgn-s | ⊦ n ≠ 0 → sgn(n) = 1 | An Axiom |
| sgn | ⊦ sgn(n) = (n ≠ 0 ⊃ 1;0) | A User Theorem |
| sgn-add | ⊦ m ≠ 0 → sgn(n + m) = 1 | A User Theorem |
| sgn-eq0 | ⊦ sgn(n) = 0 ↔ n = 0 | A User Theorem |
| sgn-lt | ⊦ n < m → sgn(m) = 1 | A User Theorem |
| sgn-num | m ≠ 0 ⊦ sgn(n + (* m)) = 1 | A User Theorem |