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-01 | ⊦ N ≠ C | An Axiom |
| disj-02 | ⊦ V ≠ N | An Axiom |
| disj-03 | ⊦ V ≠ C | An Axiom |
| case | ⊦ vstate = V ∨ vstate = N ∨ vstate = C | An Axiom |
| gen | An Axiom | |
| case-01 | ⊦ vstate ≠ V ∧ vstate ≠ N → (vstate ≠ C ↔ false) | A User Theorem |