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: |
|---|---|---|
| sel-01 | ⊦ Action(ag, cmd, ag0) .to = ag0 | An Axiom |
| sel-02 | ⊦ Action(ag, cmd, ag0) .cmd = cmd | An Axiom |
| sel-03 | ⊦ Action(ag, cmd, ag0) .from = ag | An Axiom |
| inj | ⊦ Action(ag, cmd, ag0) = Action(ag1, cmd0, ag2) ↔ ag = ag1 ∧ cmd = cmd0 ∧ ag0 = ag2 | An Axiom |
| case | ⊦ Action(a .from, a .cmd, a .to) = a | An Axiom |
| elim | ⊦ ag = a .from ∧ cmd = a .cmd ∧ ag0 = a .to ↔ a = Action(ag, cmd, ag0) | An Axiom |
| gen | An Axiom |