| Name: | Sequent: | Type: |
|---|---|---|
| tr-base | ⊦ tr(r, leaf) = (emp ∧ ⌜r = null⌝ ) | An Axiom |
| tr-rec | ⊦ tr(r, branch(t0, a, t1)) = _∃ λ r0, r1. r => mknode(r0, a, r1) * tr(r0, t0) * tr(r1, t1) | An Axiom |
| tr-fold | ⊦ (r => mknode(r0, a, r1) * tr(r0, t0) * tr(r1, t1) * P)(H) ↔ (tr(r, branch(t0, a, t1)) * P)(H) ∧ True(H[r] = mknode(r0, a, r1)) | A User Theorem |
| tr-null | ⊦ tr(null, t) = (emp ∧ ⌜t = leaf⌝ ) | A User Theorem |