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: |
|---|---|---|
| InitValue-def | ⊦ InitValue = wrapMessage2Data(mkMessage([], mkConfirm)) | An Axiom |
| getSingleSelection-def | ⊦ getSingleSelection(dl, n) = get(dl, n) | An Axiom |