| Name: | Sequent: | Type: |
|---|---|---|
| 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 | |
| updsel-05 | ⊦ (nd .left:= r) .left = r | An Axiom |
| updsel-06 | ⊦ (nd .val:= a) .left = nd .left | An Axiom |
| updsel-07 | ⊦ (nd .right:= r0) .left = nd .left | An Axiom |
| updsel-08 | ⊦ (nd .left:= r) .val = nd .val | An Axiom |
| updsel-09 | ⊦ (nd .val:= a) .val = a | An Axiom |
| updsel-10 | ⊦ (nd .right:= r0) .val = nd .val | An Axiom |
| updsel-11 | ⊦ (nd .left:= r) .right = nd .right | An Axiom |
| updsel-12 | ⊦ (nd .val:= a) .right = nd .right | An Axiom |
| updsel-13 | ⊦ (nd .right:= r0) .right = r0 | An Axiom |
| upd-03 | ⊦ mknode(r, a, r0) .left:= r1 = mknode(r1, a, r0) | An Axiom |
| upd-04 | ⊦ mknode(r, a, r0) .val:= a0 = mknode(r, a0, r0) | An Axiom |
| upd-05 | ⊦ mknode(r, a, r0) .right:= r2 = mknode(r, a, r2) | An Axiom |
| sel-03 | ⊦ mknode(r, a, r0) .left = r | An Axiom |
| sel-04 | ⊦ mknode(r, a, r0) .val = a | An Axiom |
| sel-05 | ⊦ mknode(r, a, r0) .right = r0 | An Axiom |