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 | ⊦ mkchar(i) = mkchar(j) ↔ abs(i) % 2 ^ 16 = abs(j) % 2 ^ 16 | An Axiom |
| gen | An Axiom |