enrich
   linked-tree-list
with
   procedures size# ref × heap :  : nat  ;
              size_iter# ref × heap :  : nat  ;
              dll_to_bst# ref : heap : ref nonfunctional ;
              dll_to_bst_iter# ref : heap : ref nonfunctional ;
              dll_to_bst_rec# ref × nat : heap : ref × ref nonfunctional ;
   variables 
       h : heap;
       r : ref;
       root : ref;
       right : ref;
       left : ref;
       head : ref;
       next : ref;
       temp : ref;
       a : elem;
       b : elem;
       c : elem;
       n : nat;
       m : nat;
       k : nat;
       size : nat;
       count : nat;
       mid : nat;
       half : nat;
       x : list;
       y : list;
       z : list;
       t : tree;
       hP : heap → bool;
   
   
   theorems 
      dll_to_bst_correct: 
      dll(head, x)(h), ordered≤(x) ⊦ ⟪dll_to_bst#(head; h; root)⟫ ∃ t. tr(root, t)(h) ∧ t.toList = x ∧ ordered≤(t) ∧ balanced(t);
      
      dll-size-correct: ((hP * dlls(head, r0, null, x)))(h) ⊦ ⟪size#(head, h; count)⟫ (count = # x);
      
      dll_to_bst_rec_correct: 
      n ≤ # x, ¬ null ∈ h, ((hP * dlls(head, r0, null, x)))(h)
      ⊦ ⟪dll_to_bst_rec#(head, n; h; root, right)⟫ 
           (¬ null ∈ h ∧ (∃ t, r1. ((hP * tr(root, t) * dlls(right, r1, null, restn(n, x))))(h) ∧ t.toList = firstn(n, x) ∧ balanced(t)));
      
      dll-size-iter-correct: ((hP * dlls(head, r0, null, x)))(h) ⊦ ⟪size_iter#(head, h; count)⟫ (count = # x);
      
      dll_to_bst_iter_correct: 
      dll(head, x)(h), ordered≤(x) ⊦ ⟪dll_to_bst_iter#(head; h; root)⟫ ∃ t. tr(root, t)(h) ∧ t.toList = x ∧ ordered≤(t) ∧ balanced(t);
   
   declarations 
      size: 
      size#(head, h; count){if head ≠ null then {let next = h[head].right in size#(next, h; count); count := count + 1} else count := 0};
      
      
      dll_to_bst: 
      dll_to_bst#(head; h; root){let right = null, n = 0 in {size#(head, h; n); dll_to_bst_rec#(head, n; h; root, right)}};
      
      
      dll_to_bst_rec: 
      dll_to_bst_rec#(head, n; h; root, right)
      {if n > 0
       then {let m = n / 2, left = null in {dll_to_bst_rec#(head, m; h; left, root); h[root].left := left}; 
             let m = n - n / 2 - 1, temp = null, next = h[root].right in {dll_to_bst_rec#(next, m; h; temp, right); h[root].right := temp}}
       else {root := null; right := head}
      };
      
      
      size_iter: 
      size_iter#(head, h; count){count := 0; while head ≠ null do {head := h[head].right; count := count + 1}};
      
      
      dll_to_bst_iter: 
      dll_to_bst_iter#(head; h; root){let right = null, n = 0 in {size_iter#(head, h; n); dll_to_bst_rec#(head, n; h; root, right)}};
      
      
   
   
end enrich