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: |
|---|---|---|
| in-set | ⊦ a ∈ t.set ↔ a ∈ t | An Axiom |
| refine-delete-min | s ≠ ∅, bst(t), s = t.set, ((tr(r, t) * P))(H) ⊦ ⟪search_tree_delete_min(; a, r, H)⟫ ⟨ordered_set_delete_min(; b, s)⟩ ⟨t := t.butleftmost⟩ (s = t.set ∧ a = b ∧ ((tr(r, t) * P))(H) ∧ bst(t)) | A User Theorem |
| refine-insert | bst(t), s = t.set, ((tr(r, t) * P))(H) ⊦ ⟪search_tree_insert(a; r, H)⟫ ⟨ordered_set_insert(a; s)⟩ ⟨t := t.insert(a)⟩ (s = t.set ∧ ((tr(r, t) * P))(H) ∧ bst(t)) | A User Theorem |
| set-branch | ⊦ branch(t0, a, t1).set = t0.set ∪ (t1.set ++ a) | A User Theorem |
| set-butmin | ⊦ t ≠ leaf ∧ bst(t) → t.set.butmin = t.butleftmost.set | A User Theorem |
| set-insert | ⊦ bst(t) → t.set ++ a = (t.insert(a)).set | A User Theorem |
| set-leaf | ⊦ leaf.set = ∅ | A User Theorem |
| set-min | ⊦ t ≠ leaf ∧ bst(t) → t.set.min = t.leftmost | A User Theorem |