| Name: | Sequent: | Type: |
|---|---|---|
| disj | ⊦ leaf ≠ branch(t, a, t0) | An Axiom |
| sel-01 | ⊦ branch(t, a, t0) .right = t0 | An Axiom |
| sel-02 | ⊦ branch(t, a, t0) .val = a | An Axiom |
| sel-03 | ⊦ branch(t, a, t0) .left = t | An Axiom |
| upd-01 | ⊦ branch(t, a, t0) .right:= t2 = branch(t, a, t2) | An Axiom |
| upd-02 | ⊦ branch(t, a, t0) .val:= a0 = branch(t, a0, t0) | An Axiom |
| upd-03 | ⊦ branch(t, a, t0) .left:= t1 = branch(t1, a, t0) | An Axiom |
| updsel-01 | ⊦ t ≠ leaf → (t .right:= t1) .right = t1 | An Axiom |
| updsel-02 | ⊦ t ≠ leaf → (t .right:= t1) .val = t .val | An Axiom |
| updsel-03 | ⊦ t ≠ leaf → (t .right:= t1) .left = t .left | An Axiom |
| updsel-04 | ⊦ t ≠ leaf → (t .val:= a) .right = t .right | An Axiom |
| updsel-05 | ⊦ t ≠ leaf → (t .val:= a) .val = a | An Axiom |
| updsel-06 | ⊦ t ≠ leaf → (t .val:= a) .left = t .left | An Axiom |
| updsel-07 | ⊦ t ≠ leaf → (t .left:= t0) .right = t .right | An Axiom |
| updsel-08 | ⊦ t ≠ leaf → (t .left:= t0) .val = t .val | An Axiom |
| updsel-09 | ⊦ t ≠ leaf → (t .left:= t0) .left = t0 | An Axiom |
| inj | ⊦ branch(t, a, t0) = branch(t1, a0, t2) ↔ t = t1 ∧ a = a0 ∧ t0 = t2 | An Axiom |
| case | ⊦ t = leaf ∨ t = branch(t .left, t .val, t .right) | An Axiom |
| elim | ⊦ t ≠ leaf → (t0 = t .left ∧ a = t .val ∧ t1 = t .right ↔ t = branch(t0, a, t1)) | An Axiom |
| gen | An Axiom | |
| size-01 | ⊦ # leaf = 0 | An Axiom |
| size-02 | ⊦ # branch(t, a, t0) = (# t + # t0) +1 | An Axiom |