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 | ⊦ (a × r) .nxt = r | An Axiom |
| sel-02 | ⊦ (a × r) .val = a | An Axiom |
| upd-01 | ⊦ (a × r) .nxt:= r0 = a × r0 | An Axiom |
| upd-02 | ⊦ (a × r) .val:= a0 = a0 × r | An Axiom |
| updsel-01 | ⊦ (ce .nxt:= r) .nxt = r | An Axiom |
| updsel-02 | ⊦ (ce .val:= a) .nxt = ce .nxt | An Axiom |
| updsel-03 | ⊦ (ce .nxt:= r) .val = ce .val | An Axiom |
| updsel-04 | ⊦ (ce .val:= a) .val = a | An Axiom |
| inj | ⊦ a × r = a0 × r0 ↔ a = a0 ∧ r = r0 | An Axiom |
| case | ⊦ ce .val × ce .nxt = ce | An Axiom |
| elim | ⊦ a = ce .val ∧ r = ce .nxt ↔ ce = a × r | An Axiom |
| gen | An Axiom |