enrich
   linked-tree
, 
   gelem

with
   comment: (unbalanced) linked binary search trees with insertion and deletion of the minimum;

   
   
   functions  . .insert ( . ) : tree × elem → tree;
              . .leftmost : tree → elem;
              . .butleftmost : tree → tree;
   predicates  bst : tree;
              comment: search tree property on algebraic trees;
               . ∈ . : elem × tree;
   procedures search_tree_mknode ref, elem, ref : ref, heap nonfunctional nondeterministic;
              comment: allocate a new node with given initial fields;
              search_tree_insert elem : ref, heap nonfunctional nondeterministic;
              search_tree_delete_min  : elem, ref, heap nonfunctional ;
   

   

   axioms insert-leaf :  ⊦ (leaf).insert(a) = branch(leaf, a, leaf);
          used for: s, ls;
          insert-branch-same :  ⊦ branch(t0, a, t1).insert(a) = branch(t0, a, t1);
          used for: s, ls;
          insert-branch-left :  ⊦ a < b → branch(t0, b, t1).insert(a) = branch(t0.insert(a), b, t1);
          used for: s, ls, lc;
          insert-branch-right :  ⊦ b < a → branch(t0, b, t1).insert(a) = branch(t0, b, t1.insert(a));
          used for: s, ls, lc;
          butleftmost :  ⊦ branch(t0, a, t1).butleftmost = (t0 = leaf ⊃ t1;branch(t0.butleftmost, a, t1));
          used for: s, ls;
          in-leaf :  ⊦ ¬ a ∈ leaf;
          used for: s, ls;
          in-branch :  ⊦ a ∈ branch(t0, b, t1) ↔ ¬ ¬(a = b ∨ a ∈ t0 ∨ a ∈ t1);
          used for: s, ls;
          bst-leaf :  ⊦ bst(leaf);
          used for: s, ls;
          leftmost :  ⊦ branch(t0, a, t1).leftmost = (t0 = leaf ⊃ a;t0.leftmost);
          used for: s, ls;
          bst-branch :  ⊦ bst(branch(t0, b, t1)) ↔ (∀ a. a ∈ t0 → a < b) ∧ (∀ a. a ∈ t1 → b < a) ∧ bst(t0) ∧ bst(t1);
          used for: s, ls;

   

   declaration search_tree_delete_min
               : search_tree_delete_min(; a, r, H)
                 {let r0 = H[r].left
                  in if r0 = null
                     then {a := H[r].val; r := H[r].right, H := H -- r}
                     else let r1 = r, r2 = H[r0].left
                          in {while r2 ≠ null do {r1 := r0; r0 := r2; r2 := H[r0].left}; a := H[r0].val; r2 := H[r0].right; H := H -- r0; 
                              H := H[r1, H[r1].left:= r2]}
                 }
               ;
               search_tree_mknode
               : search_tree_mknode(r0, a, r1; r, H){alloc(; r, H); H := H[r, H[r].left:= r0]; H := H[r, H[r].right:= r1]; H := H[r, H[r].val:= a]}
               ;
               search_tree_insert
               : search_tree_insert(a; r, H)
                 {if r = null
                  then search_tree_mknode(null, a, null; r, H)
                  else let r1 = r, r0 = null
                       in while a ≠ H[r1].val
                          do if a < H[r1].val
                             then {if H[r1].left = null then {search_tree_mknode(null, a, null; r0, H); H := H[r1, H[r1].left:= r0]}; r1 := H[r1].left}
                             else if H[r1].val < a
                                  then {if H[r1].right = null then {search_tree_mknode(null, a, null; r0, H); H := H[r1, H[r1].right:= r0]}; 
                                        r1 := H[r1].right}
                 }
               ;
end enrich