anchor.diff:              AvlTree.Insert (comparer, l, root)
           | Node (ll, lr, lx, lh), Node (rl, rr, rx, rh) ->
               if lh > rh + balanceTolerance then
  -                AvlTree.Balance (comparer, ll, AvlTree.Join (comparer, lr, r, root), lx)
  +                AvlTree.Balance (ll, AvlTree.Join (comparer, lr, r, root), lx)
               else if rh > lh + balanceTolerance then
  -                AvlTree.Balance (comparer, AvlTree.Join (comparer, l, rl, root), rr, rx)
  +                AvlTree.Balance (AvlTree.Join (comparer, l, rl, root), rr, rx)
               else
                   AvlTree.Create (root, l, r)
   
  
positive.code:         // Preconditions
          assert (AvlTree.AvlInvariant l)
          assert (AvlTree.AvlInvariant r)
  
          match l, r with
          | Empty, Empty ->
  
negative.code:         | _ ->
              AvlTree<'T>.CompareStacks (comparer, [s1], [s2])
  
      /// Returns the height of a AvlTree.
      static member private ComputeHeight (tree : AvlTree<'T>) =
          match tree with
          | Empty -> 0u
          | Node (l, r, _, _) ->
              1u + max (AvlTree.ComputeHeight l) (AvlTree.ComputeHeight r)
          
      /// Determines if a AvlTree is correctly formed.
      /// It isn't necessary to call this at run-time, though it may be useful for asserting
      /// the correctness of functions which weren't extracted from the Isabelle/HOL theory.
      static member internal AvlInvariant (tree : AvlTree<'T>) =
          match tree with
          | Empty -> true
          | Node (l, r, x, h) ->
              let height_l = AvlTree.ComputeHeight l
              let height_r = AvlTree.ComputeHeight r
              height_l = height_r
              || (height_l = (1u + height_r) || height_r = (1u + height_l))
              && h = ((max height_l height_r) + 1u)
              && AvlTree.AvlInvariant l
              && AvlTree.AvlInvariant r
  
      /// Returns the height of a AvlTree.
      static member inline Height (tree : AvlTree<'T>) =
          match tree with
          | Empty -> 0u
          | Node (_,_,_,h) -> h
  
      /// Returns the absolute difference in heights between two AvlTrees.
      static member private HeightDiff (t1, t2 : AvlTree<'T>) =
          (max (AvlTree.Height t1) (AvlTree.Height t2)) - (min (AvlTree.Height t1) (AvlTree.Height t2))
  
      /// Determines if a AvlTree is empty.
      static member inline IsEmptyTree (tree : AvlTree<'T>) =
          match tree with
          | Empty -> true
          | Node (_,_,_,_) -> false
  
      /// Creates a AvlTree whose root node holds the specified value
      /// and the specified left and right subtrees.
      static member inline Create (value, l, r : AvlTree<'T>) =
          assert (AvlTree.AvlInvariant l)
          assert (AvlTree.AvlInvariant r)
          assert (AvlTree.HeightDiff (l, r) <= balanceTolerance)
          Node (l, r, value, (max (AvlTree.Height l) (AvlTree.Height r)) + 1u)
  
      /// Creates a AvlTree containing the specified value.
      static member Singleton value : AvlTree<'T> =
          AvlTree.Create (value, Empty, Empty)
  
      static member private mkt_bal_l (n, l, r : AvlTree<'T>) =
          if AvlTree.Height l = AvlTree.Height r + balanceTolerance then
              match l with
              | Empty ->
                  failwith "mkt_bal_l"
              | Node (ll, lr, ln, _) ->
                  if AvlTree.Height ll < AvlTree.Height lr then
                      match lr with
                      | Empty ->
                          failwith "mkt_bal_l"
                      | Node (lrl, lrr, lrn, _) ->
                          AvlTree.Create (lrn, AvlTree.Create (ln, ll, lrl), AvlTree.Create (n, lrr, r))
                  else
                      AvlTree.Create (ln, ll, AvlTree.Create (n, lr, r))
          else
              AvlTree.Create (n, l, r)
  
      static member private mkt_bal_r (n, l, r : AvlTree<'T>) =
          if AvlTree.Height r = AvlTree.Height l + balanceTolerance then
              match r with
              | Empty ->
                  failwith "mkt_bal_r"
              | Node (rl, rr, rn, _) ->
                  if AvlTree.Height rr < AvlTree.Height rl then
                      match rl with
                      | Empty ->
                          failwith "mkt_bal_r"
                      | Node (rll, rlr, rln, _) ->
                          AvlTree.Create (rln, AvlTree.Create (n, l, rll), AvlTree.Create (rn, rlr, rr))
                  else
                      AvlTree.Create (rn, AvlTree.Create (n, l, rl), rr)
          else
              AvlTree.Create (n, l, r)
  
      static member DeleteMax (tree : AvlTree<'T>) =
          match tree with
          | Empty ->
              invalidArg "tree" "Cannot delete the maximum value from an empty tree."
          | Node (l, Empty, n, _) ->
              n, l
          | Node (l, (Node (_,_,_,_) as right), n, _) ->
              let na, r = AvlTree.DeleteMax right
              na, AvlTree.mkt_bal_l (n, l, r)
  
      static member DeleteRoot (tree : AvlTree<'T>) =
          match tree with
          | Empty ->
              invalidArg "tree" "Cannot delete the root of an empty tree."
          | Node (Empty, r, _, _) -> r
          | Node ((Node (_,_,_,_) as left), Empty, _, _) ->
              left
          | Node ((Node (_,_,_,_) as left), (Node (_,_,_,_) as right), _, _) ->
              let new_n, l = AvlTree.DeleteMax left
              AvlTree.mkt_bal_r (new_n, l, right)
  
      /// Determines if a AvlTree contains a specified value.
      static member Contains (comparer : IComparer<'T>, tree : AvlTree<'T>, value : 'T) =
          match tree with
          | Empty ->
              false
          | Node (l, r, n, _) ->
              let comparison = comparer.Compare (value, n)
              if comparison = 0 then      // value = n
                  true
              elif comparison < 0 then    // value < n
                  AvlTree.Contains (comparer, l, value)
              else                        // value > n
                  AvlTree.Contains (comparer, r, value)
  
      /// Removes the specified value from the tree.
      /// If the tree doesn't contain the value, no exception is thrown;
      /// the tree will be returned without modification.
      static member Delete (comparer : IComparer<'T>, tree : AvlTree<'T>, value : 'T) =
          match tree with
          | Empty ->
              Empty
          | Node (l, r, n, _) ->
              let comparison = comparer.Compare (value, n)
              if comparison = 0 then              // x = n
                  AvlTree.DeleteRoot tree
              elif comparison < 0 then            // x < n
                  let la = AvlTree.Delete (comparer, l, value)
                  AvlTree.mkt_bal_r (n, la, r)
              else                                // x > n
                  let a = AvlTree.Delete (comparer, r, value)
                  AvlTree.mkt_bal_l (n, l, a)
  
      /// Adds a value to a AvlTree.
      /// If the tree already contains the value, no exception is thrown;
      /// the tree will be returned without modification.
      static member Insert (comparer : IComparer<'T>, tree : AvlTree<'T>, value : 'T) =
          match tree with
          | Empty ->
              Node (Empty, Empty, value, 1u)
          | Node (l, r, n, _) ->
              let comparison = comparer.Compare (value, n)
              if comparison = 0 then                              // x = n
                  tree
              elif comparison < 0 then                            // x < n
                  let l' = AvlTree.Insert (comparer, l, value)
                  AvlTree.mkt_bal_l (n, l', r)
              else                                                // x > n
                  let r' = AvlTree.Insert (comparer, r, value)
                  AvlTree.mkt_bal_r (n, l, r')
  
      /// Gets the maximum (greatest) value stored in the AvlTree.
      static member MaxElement (tree : AvlTree<'T>) =
          match tree with
          | Empty ->
              invalidArg "tree" "The tree is empty."
          | Node (_, Empty, n, _) ->
              n
          | Node (_, right, _, _) ->
              AvlTree.MaxElement right
  
      /// Gets the minimum (least) value stored in the AvlTree.
      static member MinElement (tree : AvlTree<'T>) =
          match tree with
          | Empty ->
              invalidArg "tree" "The tree is empty."
          | Node (Empty, _, n, _) ->
              n
          | Node (left, _, _, _) ->
              AvlTree.MinElement left
  
      /// Extracts the minimum (least) value from a AvlTree,
      /// returning the value along with the updated tree.
      static member ExtractMin (tree : AvlTree<'T>) =
          match tree with
          | Empty ->
              invalidArg "tree" "The tree is empty."
          | Node (Empty, r, n, _) ->
              n, r
          | Node (Node (left, mid, a, _), r, x, _) ->
              // Rebalance the tree at the same time we're traversing downwards
              // to find the minimum value. This avoids the need to perform a
              // second traversal to remove the element once it's found.
              let n = AvlTree.Create (x, mid, r)
              AvlTree.Create (a, left, n)
              |> AvlTree.ExtractMin
  
      /// Extracts the minimum (least) value from a AvlTree,
      /// returning the value along with the updated tree.
      /// No exception is thrown if the tree is empty.
      static member TryExtractMin (tree : AvlTree<'T>) =
          // Is the tree empty?
          if AvlTree.IsEmptyTree tree then
              None, tree
          else
              let minElement, tree = AvlTree.ExtractMin tree
              Some minElement, tree
  
      /// Extracts the maximum (greatest) value from a AvlTree,
      /// returning the value along with the updated tree.
      static member ExtractMax (tree : AvlTree<'T>) =
          match tree with
          | Empty ->
              invalidArg "tree" "The tree is empty."
          | Node (l, Empty, n, _) ->
              n, l
          | Node (l, Node (mid, right, a, _), x, _) ->
              // Rebalance the tree at the same time we're traversing downwards
              // to find the maximum value. This avoids the need to perform a
              // second traversal to remove the element once it's found.
              let n = AvlTree.Create (x, l, mid)
              AvlTree.Create (a, n, right)
              |> AvlTree.ExtractMax
  
      /// Extracts the maximum (greatest) value from a AvlTree,
      /// returning the value along with the updated tree.
      /// No exception is thrown if the tree is empty.
      static member TryExtractMax (tree : AvlTree<'T>) =
          // Is the tree empty?
          if AvlTree.IsEmptyTree tree then
              None, tree
          else
              let maxElement, tree = AvlTree.ExtractMax tree
              Some maxElement, tree
  
      /// Counts the number of elements in the tree.
      static member Count (tree : AvlTree<'T>) =
          match tree with
          | Empty -> 0u
          | Node (Empty, Empty, _, _) -> 1u
          | Node (l, r, _, _) ->
              /// Mutable stack. Holds the trees which still need to be traversed.
              let stack = Stack (defaultStackCapacity)
  
              /// The number of elements discovered in the tree so far.
              let mutable count = 1u   // Start at one (1) to include this root node.
  
              // Traverse the tree using the mutable stack, incrementing the counter at each node.
              stack.Push r
              stack.Push l
  
              while stack.Count > 0 do
                  match stack.Pop () with
                  | Empty -> ()
                  (* OPTIMIZATION: Handle a few of the cases specially here to avoid pushing empty
                     nodes on the stack. *)
                  | Node (Empty, Empty, _, _) ->
                      // Increment the element count.
                      count <- count + 1u
  
                  | Node (Empty, z, _, _)
                  | Node (z, Empty, _, _) ->
                      // Increment the element count.
                      count <- count + 1u
  
                      // Push the non-empty child onto the stack.
                      stack.Push z
  
                  | Node (l, r, _, _) ->
                      // Increment the element count.
                      count <- count + 1u
  
                      // Push the children onto the stack.
                      stack.Push r
                      stack.Push l
  
              // Return the element count.
              count
  
      //
      static member Iter (action : 'T -> unit) (tree : AvlTree<'T>) : unit =
          match tree with
          | Empty -> ()
          | Node (Empty, Empty, x, _) ->
              // Invoke the action with this single element.
              action x
          | Node (l, r, x, _) ->
              /// Mutable stack. Holds the trees which still need to be traversed.
              let stack = Stack (defaultStackCapacity)
  
              // Traverse the tree using the mutable stack, applying the folder function to
              // each value to update the state value.
              stack.Push r
              stack.Push <| AvlTree.Singleton x
              stack.Push l
  
              while stack.Count > 0 do
                  match stack.Pop () with
                  | Empty -> ()
                  | Node (Empty, Empty, x, _) ->
                      // Apply this value to the action function.
                      action x
  
                  | Node (Empty, z, x, _) ->
                      // Apply this value to the action function.
                      action x
  
                      // Push the non-empty child onto the stack.
                      stack.Push z
  
                  | Node (l, r, x, _) ->
                      // Push the children onto the stack.
                      // Also push a new Node onto the stack which contains the value from
                      // this Node, so it'll be processed in the correct order.
                      stack.Push r
                      stack.Push <| AvlTree.Singleton x
                      stack.Push l
  
      /// Applies the given accumulating function to all elements in a AvlTree.
      static member Fold (folder : 'State -> 'T -> 'State) (state : 'State) (tree : AvlTree<'T>) =
          match tree with
          | Empty -> state
          | Node (Empty, Empty, x, _) ->
              // Invoke the folder function on this single element and return the result.
              folder state x
          | Node (l, r, x, _) ->
              // Adapt the folder function since we'll always supply all of the arguments at once.
              let folder = FSharpFunc<_,_,_>.Adapt folder
  
              /// Mutable stack. Holds the trees which still need to be traversed.
              let stack = Stack (defaultStackCapacity)
  
              /// The current state value.
              let mutable state = state
  
              // Traverse the tree using the mutable stack, applying the folder function to
              // each value to update the state value.
              stack.Push r
              stack.Push <| AvlTree.Singleton x
              stack.Push l
  
              while stack.Count > 0 do
                  match stack.Pop () with
                  | Empty -> ()
                  | Node (Empty, Empty, x, _) ->
                      // Apply this value to the folder function.
                      state <- folder.Invoke (state, x)
  
                  | Node (Empty, z, x, _) ->
                      // Apply this value to the folder function.
                      state <- folder.Invoke (state, x)
  
                      // Push the non-empty child onto the stack.
                      stack.Push z
  
                  | Node (l, r, x, _) ->
                      // Push the children onto the stack.
                      // Also push a new Node onto the stack which contains the value from
                      // this Node, so it'll be processed in the correct order.
                      stack.Push r
                      stack.Push <| AvlTree.Singleton x
                      stack.Push l
  
              // Return the final state value.
              state
  
      /// Applies the given accumulating function to all elements in a AvlTree.
      static member FoldBack (folder : 'T -> 'State -> 'State) (state : 'State) (tree : AvlTree<'T>) =
          match tree with
          | Empty -> state
          | Node (Empty, Empty, x, _) ->
              // Invoke the folder function on this single element and return the result.
              folder x state
          | Node (l, r, x, _) ->
              // Adapt the folder function since we'll always supply all of the arguments at once.
              let folder = FSharpFunc<_,_,_>.Adapt folder
  
              /// Mutable stack. Holds the trees which still need to be traversed.
              let stack = Stack (defaultStackCapacity)
  
              /// The current state value.
              let mutable state = state
  
              // Traverse the tree using the mutable stack, applying the folder function to
              // each value to update the state value.
              stack.Push l
              stack.Push <| AvlTree.Singleton x
              stack.Push r
  
              while stack.Count > 0 do
                  match stack.Pop () with
                  | Empty -> ()
                  | Node (Empty, Empty, x, _) ->
                      // Apply this value to the folder function.
                      state <- folder.Invoke (x, state)
  
                  | Node (z, Empty, x, _) ->
                      // Apply this value to the folder function.
                      state <- folder.Invoke (x, state)
  
                      // Push the non-empty child onto the stack.
                      stack.Push z
  
                  | Node (l, r, x, _) ->
                      // Push the children onto the stack.
                      // Also push a new Node onto the stack which contains the value from
                      // this Node, so it'll be processed in the correct order.
                      stack.Push l
                      stack.Push <| AvlTree.Singleton x
                      stack.Push r
  
              // Return the final state value.
              state
  
      /// Tests if any element of the collection satisfies the given predicate.
      static member Exists (predicate : 'T -> bool) (tree : AvlTree<'T>) : bool =
          match tree with
          | Empty -> false
          | Node (Empty, Empty, x, _) ->
              // Apply the predicate function to this element and return the result.
              predicate x
          | Node (l, r, x, _) ->
              /// Mutable stack. Holds the trees which still need to be traversed.
              let stack = Stack (defaultStackCapacity)
  
              /// Have we found a matching element?
              let mutable foundMatch = false
  
              // Traverse the tree using the mutable stack, applying the folder function to
              // each value to update the state value.
              stack.Push r
              stack.Push <| AvlTree.Singleton x
              stack.Push l
  
              while stack.Count > 0 && not foundMatch do
                  match stack.Pop () with
                  | Empty -> ()
                  | Node (Empty, Empty, x, _) ->
                      // Apply the predicate to this element.
                      foundMatch <- predicate x
  
                  | Node (Empty, z, x, _) ->
                      // Apply the predicate to this element.
                      foundMatch <- predicate x
  
                      // Push the non-empty child onto the stack.
                      stack.Push z
  
                  | Node (l, r, x, _) ->
                      // Push the children onto the stack.
                      // Also push a new Node onto the stack which contains the value from
                      // this Node, so it'll be processed in the correct order.
                      stack.Push r
                      stack.Push <| AvlTree.Singleton x
                      stack.Push l
  
              // Return the value indicating whether or not a matching element was found.
              foundMatch
  
      /// Tests if all elements of the collection satisfy the given predicate.
      static member Forall (predicate : 'T -> bool) (tree : AvlTree<'T>) : bool =
          match tree with
          | Empty -> true
          | Node (Empty, Empty, x, _) ->
              // Apply the predicate function to this element and return the result.
              predicate x
          | Node (l, r, x, _) ->
              /// Mutable stack. Holds the trees which still need to be traversed.
              let stack = Stack (defaultStackCapacity)
  
              /// Have all of the elements we've seen so far matched the predicate?
              let mutable allElementsMatch = true
  
              // Traverse the tree using the mutable stack, applying the folder function to
              // each value to update the state value.
              stack.Push r
              stack.Push <| AvlTree.Singleton x
              stack.Push l
  
              while stack.Count > 0 && allElementsMatch do
                  match stack.Pop () with
                  | Empty -> ()
                  | Node (Empty, Empty, x, _) ->
                      // Apply the predicate to this element.
                      allElementsMatch <- predicate x
  
                  | Node (Empty, z, x, _) ->
                      // Apply the predicate to this element.
                      allElementsMatch <- predicate x
  
                      // Push the non-empty child onto the stack.
                      stack.Push z
  
                  | Node (l, r, x, _) ->
                      // Push the children onto the stack.
                      // Also push a new Node onto the stack which contains the value from
                      // this Node, so it'll be processed in the correct order.
                      stack.Push r
                      stack.Push <| AvlTree.Singleton x
                      stack.Push l
  
              // Return the value indicating if all elements matched the predicate.
              allElementsMatch
  
      /// Returns a sequence containing the elements stored
      /// in a AvlTree, ordered from least to greatest.
      static member ToSeq (tree : AvlTree<'T>) =
          seq {
          match tree with
          | Empty -> ()
          | Node (l, r, n, _) ->
              yield! AvlTree.ToSeq l
              yield n
              yield! AvlTree.ToSeq r
          }
  
      /// Returns a list containing the elements stored in
      /// a AvlTree, ordered from least to greatest. 
      static member ToList (tree : AvlTree<'T>) =
          ([], tree)
          ||> AvlTree.FoldBack (fun el lst ->
              el :: lst)
  
      /// Returns an array containing the elements stored in
      /// a AvlTree, ordered from least to greatest.
      static member ToArray (tree : AvlTree<'T>) =
          let elements = ResizeArray ()
          AvlTree.Iter elements.Add tree
          elements.ToArray ()
  
      //
      // TODO : This could be replaced by 'mkt_bal_l' and 'mkt_bal_r'.
      static member Balance (l, r, x) : AvlTree<'T> =
          // Preconditions
          assert (AvlTree.AvlInvariant l)
          assert (AvlTree.AvlInvariant r)
          assert (AvlTree.HeightDiff (l, r) <= (balanceTolerance + 1u))
  
          let hl = AvlTree.Height l
          let hr = AvlTree.Height r
          if hl > hr + balanceTolerance then // left is heavier than right
              match l with
              | Empty ->
                  failwith "rebalance"
              | Node (ll, lr, lx, _) ->
                  // one of the nodes must have height > height r + 1
                  if AvlTree.Height ll > AvlTree.Height lr then
                      AvlTree.Create (
                          lx,
                          ll,
                          AvlTree.Create (x, lr, r))
                  else
                      // balance right: combination
                      match lr with
                      | Empty ->
                          failwith "rebalance"
                      | Node (lrl, lrr, lrx, _) ->
                          AvlTree.Create (
                              lrx,
                              AvlTree.Create (lx, ll, lrl),
                              AvlTree.Create (x, lrr, r))
                      
          elif hr > hl + balanceTolerance then // right is heavier than left
              match r with
              | Empty ->
                  failwith "rebalance"
              | Node (rl, rr, rx, _) ->
                  // one of the nodes must have height > height t1 + 1
                  if AvlTree.Height rr > AvlTree.Height rl then
                      // rotate left
                      AvlTree.Create (
                          rx,
                          AvlTree.Create (x, l, rl),
                          rr)
                  else
                      // balance left: combination
                      match rl with
                      | Empty ->
                          failwith "rebalance"
                      | Node (rll, rlr, rlx, _) ->
                          AvlTree.Create (
                              rlx,
                              AvlTree.Create (x, l, rll),
                              AvlTree.Create (rx, rlr, rr))
          else
              AvlTree.Create (x, l, r)
  
      /// Join two trees together with the specified root element.
      /// Takes two trees representing disjoint sets and combines them, returning
      /// a new balanced tree representing the union of the two sets and the given root element.
  