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