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 | ⊦ mkcell(r, r0, a).val = a | An Axiom |
| sel-02 | ⊦ mkcell(r, r0, a).right = r0 | An Axiom |
| sel-03 | ⊦ mkcell(r, r0, a).left = r | An Axiom |
| upd-01 | ⊦ mkcell(r, r0, a).val:= a0 = mkcell(r, r0, a0) | An Axiom |
| upd-02 | ⊦ mkcell(r, r0, a).right:= r2 = mkcell(r, r2, a) | An Axiom |
| upd-03 | ⊦ mkcell(r, r0, a).left:= r1 = mkcell(r1, r0, a) | An Axiom |
| updsel-01 | ⊦ (ce.val:= a).val = a | An Axiom |
| updsel-02 | ⊦ (ce.right:= r0).val = ce.val | An Axiom |
| updsel-03 | ⊦ (ce.left:= r).val = ce.val | An Axiom |
| updsel-04 | ⊦ (ce.val:= a).right = ce.right | An Axiom |
| updsel-05 | ⊦ (ce.right:= r0).right = r0 | An Axiom |
| updsel-06 | ⊦ (ce.left:= r).right = ce.right | An Axiom |
| updsel-07 | ⊦ (ce.val:= a).left = ce.left | An Axiom |
| updsel-08 | ⊦ (ce.right:= r0).left = ce.left | An Axiom |
| updsel-09 | ⊦ (ce.left:= r).left = r | An Axiom |
| inj | ⊦ mkcell(r, r0, a) = mkcell(r1, r2, a0) ↔ r = r1 ∧ r0 = r2 ∧ a = a0 | An Axiom |
| case | ⊦ mkcell(ce.left, ce.right, ce.val) = ce | An Axiom |
| elim | ⊦ (r = ce.left ∧ r0 = ce.right) ∧ a = ce.val ↔ ce = mkcell(r, r0, a) | An Axiom |
| gen | An Axiom |