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 | ⊦ MODE_R ≠ MODE_W | An Axiom |
| disj-02 | ⊦ MODE_R ≠ MODE_RW | An Axiom |
| disj-03 | ⊦ MODE_W ≠ MODE_RW | An Axiom |
| case | ⊦ mode = MODE_R ∨ mode = MODE_W ∨ mode = MODE_RW | An Axiom |
| gen | An Axiom |