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: |
|---|---|---|
| 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-branch | ⊦ (tr(r, t) * P)(H) ∧ r ≠ null → t ≠ leaf | A User Theorem |
| tr-fold | ⊦ (r => mknode(r0, a, r1) * tr(r0, t0) * tr(r1, t1) * P)(H) → (¬ (tr(r, branch(t0, a, t1)) * P)(H) ↔ false) | A User Theorem |
| tr-fold-singleton | ⊦ r => mknode(null, a, null) = tr(r, branch(leaf, a, leaf)) | A User Theorem |
| tr-fold-t | ⊦ (r => mknode(r0, a, r1) * tr(r0, t0) * tr(r1, t1) * P0 * P1)(H) → (¬ (tr(r, branch(t0, a, t1)) * P0 * true)(H) ↔ false) | A User Theorem |
| tr-null | ⊦ tr(null, t) = (emp ∧ ⌜t = leaf⌝ ) | A User Theorem |
| tr-unfold | ⊦ r ≠ null → (¬ ¬ (tr(r, t) * P)(H) ↔ (∃ t0, t1, a, r0, r1. t = branch(t0, a, t1) ∧ (r => mknode(r0, a, r1) * tr(r0, t0) * tr(r1, t1) * P)(H))) | A User Theorem |