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 | ⊦ (r -- sk) .ref = r | An Axiom |
| sel-02 | ⊦ (r -- sk) .key = sk | An Axiom |
| inj | ⊦ r -- sk = r0 -- sk0 ↔ r = r0 ∧ sk = sk0 | An Axiom |
| case | ⊦ rk .ref -- rk .key = rk | An Axiom |
| elim | ⊦ r = rk .ref ∧ sk = rk .key ↔ rk = r -- sk | An Axiom |
| gen | An Axiom | |
| inj-01 | ⊦ r -- sk = r0 -- sk0 ↔ ¬ ¬ (r = r0 ∧ sk = sk0) | A User Theorem |
| same | ⊦ r -- sk = r -- sk0 ↔ sk = sk0 | A User Theorem |
| same-01 | ⊦ r -- sk = r0 -- sk ↔ r = r0 | A User Theorem |