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: |
|---|---|---|
| disj-1 | ⊦ ¬(true ↔ false) | An Axiom |
| case-1 | ⊦ (boolvar ↔ true) ∨ (boolvar ↔ false) | An Axiom |
| gen | bool freely generated by true, false; | An Axiom |