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: |
|---|---|---|
| bst-branch | ⊦ bst(branch(t0, b, t1)) ↔ (∀ a. a ∈ t0 → a < b) ∧ (∀ a. a ∈ t1 → b < a) ∧ bst(t0) ∧ bst(t1) | An Axiom |
| bst-leaf | ⊦ bst(leaf) | An Axiom |
| in-branch | ⊦ a ∈ branch(t0, b, t1) ↔ ¬ ¬(a = b ∨ a ∈ t0 ∨ a ∈ t1) | An Axiom |
| in-leaf | ⊦ ¬ a ∈ leaf | An Axiom |
| leftmost | ⊦ branch(t0, a, t1).leftmost = (t0 = leaf ⊃ a;t0.leftmost) | An Axiom |
| search_tree_delete_min | An Axiom | |
| butleftmost | ⊦ branch(t0, a, t1).butleftmost = (t0 = leaf ⊃ t1;branch(t0.butleftmost, a, t1)) | An Axiom |
| search_tree_insert | An Axiom | |
| search_tree_mknode | An Axiom | |
| insert-branch-right | ⊦ b < a → branch(t0, b, t1).insert(a) = branch(t0, b, t1.insert(a)) | An Axiom |
| insert-branch-left | ⊦ a < b → branch(t0, b, t1).insert(a) = branch(t0.insert(a), b, t1) | An Axiom |
| insert-branch-same | ⊦ branch(t0, a, t1).insert(a) = branch(t0, a, t1) | An Axiom |
| insert-leaf | ⊦ (leaf).insert(a) = branch(leaf, a, leaf) | An Axiom |
| bst-branch-rec | ⊦ bst(branch(t0, a, t1)) → bst(t0) ∧ bst(t1) | A User Theorem |
| bst-elem-in-branch | ⊦ bst(branch(t0, a, t1)) → ¬ a ∈ t0 ∧ ¬ a ∈ t1 | A User Theorem |
| bst-elem-order-left | ⊦ bst(branch(t0, a, t1)) ∧ b ∈ t0 → b < a | A User Theorem |
| bst-elem-order-right | ⊦ bst(branch(t0, a, t1)) ∧ b ∈ t1 → a < b | A User Theorem |
| butleftmost-bst | t ≠ leaf, bst(t) ⊦ ¬ bst(t.butleftmost) ↔ false | A User Theorem |
| butleftmost-in | ⊦ t ≠ leaf ∧ bst(t) → (a ∈ t.butleftmost ↔ a ∈ t ∧ a ≠ t.leftmost) | A User Theorem |
| delete-prepost | r ≠ null, ((tr(r, t) * P))(H) ⊦ ⟨search_tree_delete_min(; a, r, H)⟩ (((tr(r, t.butleftmost) * P))(H) ∧ a = t.leftmost) | A User Theorem |
| delete-prepost-loop | r ≠ null, ((tr(r, t) * P))(H) ⊦ [search_tree_delete_min(; a, r, H)] (((tr(r, t.butleftmost) * P))(H) ∧ a = t.leftmost) | A User Theorem |
| delete-prepost-min | r ≠ null, ((tr(r, t) * P))(H), bst(t) ⊦ ⟨search_tree_delete_min(; a, r, H)⟩ (((tr(r, t.butleftmost) * P))(H) ∧ bst(t.butleftmost) ∧ a = t.leftmost ∧ ¬ a ∈ t.butleftmost ∧ (∀ b. b ∈ t.butleftmost → a < b)) | A User Theorem |
| insert-bst | bst(t) ⊦ ¬ bst(t.insert(a)) ↔ false | A User Theorem |
| insert-in | ⊦ bst(t) → (a ∈ t.insert(b) ↔ ¬ ¬(a ∈ t ∨ a = b)) | A User Theorem |
| insert-prepost | ((tr(r, t) * P))(H) ⊦ ⟪search_tree_insert(a; r, H)⟫ ((tr(r, t.insert(a)) * P))(H) | A User Theorem |
| leftmost-in | ⊦ t ≠ leaf → t.leftmost ∈ t | A User Theorem |
| leftmost-ismin | ⊦ t ≠ leaf ∧ bst(t) ∧ b ≠ t.leftmost ∧ b ∈ t → (¬ t.leftmost < b ↔ false) | A User Theorem |
| mknode-prepost | P(H) ⊦ ⟪search_tree_mknode(r0, a, r1; r, H)⟫ ((r => mknode(r0, a, r1) * P))(H) | A User Theorem |
| root-nonnull | ⊦ r ≠ null ∧ ((tr(r, t) * P))(H) → (∃ t0, a, t1. t = branch(t0, a, t1)) | A User Theorem |