anchor.diff:      /// Node.
       // Left-Child, Right-Child, Value, Height
       | Node of AvlTree<'T> * AvlTree<'T> * 'T * uint32
  -
  -    /// 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
  -
  -    /// 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>) =
  -        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 Rebalance (t1, t2, k) : AvlTree<'T> =
  -        let t1h = AvlTree.Height t1
  -        let t2h = AvlTree.Height t2
  -        if t2h > t1h + balanceTolerance then // right is heavier than left
  -            match t2 with
  -            | Node (t2l, t2r, t2k, _) ->
  -                // one of the nodes must have height > height t1 + 1
  -                if AvlTree.Height t2l > t1h + 1u then  // balance left: combination
  -                    match t2l with
  -                    | Node (t2ll, t2lr, t2lk, _) ->
  -                        AvlTree.Create (
  -                            t2lk,
  -                            AvlTree.Create (k, t1, t2ll),
  -                            AvlTree.Create (t2k, t2lr, t2r))
  -                    | _ -> failwith "rebalance"
  -                else // rotate left
  -                    AvlTree.Create (
  -                        t2k,
  -                        AvlTree.Create (k, t1, t2l),
  -                        t2r)
  -            | _ -> failwith "rebalance"
  -
  -        elif t1h > t2h + balanceTolerance then // left is heavier than right
  -            match t1 with
  -            | Node (t1l, t1r, t1k, _) ->
  -                // one of the nodes must have height > height t2 + 1
  -                if AvlTree.Height t1r > t2h + 1u then
  -                    // balance right: combination
  -                    match t1r with
  -                    | Node (t1rl, t1rr, t1rk, _) ->
  -                        AvlTree.Create (
  -                            t1rk,
  -                            AvlTree.Create (t1k, t1l, t1rl),
  -                            AvlTree.Create (k, t1rr, t2))
  -                    | _ -> failwith "rebalance"
  -                else
  -                    AvlTree.Create (
  -                        t1k,
  -                        t1l,
  -                        AvlTree.Create (k, t1r, t2))
  -            | _ -> failwith "rebalance"
  -
  -        else
  -            AvlTree.Create (k, t1, t2)
  -
  -    // Given t1 < k < t2 where t1 and t2 are "balanced",
  -    // return a balanced tree for <t1,k,t2>.
  -    // Recall: balance means subtrees heights differ by at most "tolerance"
  -    static member Balance (comparer : IComparer<'T>, t1, t2, k) =
  -        // Preconditions
  -        assert (AvlTree.AvlInvariant t1)
  -        assert (AvlTree.AvlInvariant t2)
  -
  -        match t1, t2 with
  -        // TODO : The first two patterns can be merged to use the same handler.
  -        | Empty, t2 ->
  -            // drop t1 = empty
  -            AvlTree.Insert (comparer, t2, k)
  -        | t1, Empty ->
  -            // drop t2 = empty
  -            AvlTree.Insert (comparer, t1, k)
  -
  -        // TODO : The next two patterns can be merged to use the same handler.
  -        | Node (Empty, Empty, k1, _), t2 ->
  -            let t' = AvlTree.Insert (comparer, t2, k1)
  -            AvlTree.Insert (comparer, t', k)
  -        | t1, Node (Empty, Empty, k2, _) ->
  -            let t' = AvlTree.Insert (comparer, t1, k2)
  -            AvlTree.Insert (comparer, t', k)
  -
  -        | Node (t11, t12, k1, h1), Node (t21, t22, k2, h2) ->
  -            // Have:  (t11 < k1 < t12) < k < (t21 < k2 < t22)
  -            // Either (a) h1,h2 differ by at most 2 - no rebalance needed.
  -            //        (b) h1 too small, i.e. h1+2 < h2
  -            //        (c) h2 too small, i.e. h2+2 < h1
  -            if   h1+balanceTolerance < h2 then
  -                // case: b, h1 too small
  -                // push t1 into low side of t2, may increase height by 1 so rebalance
  -                AvlTree.Rebalance (AvlTree.Balance (comparer, t1, t21, k), t22, k2)
  -            elif h2+balanceTolerance < h1 then
  -                // case: c, h2 too small
  -                // push t2 into high side of t1, may increase height by 1 so rebalance
  -                AvlTree.Rebalance (t11, AvlTree.Balance (comparer, t12, t2, k), k1)
  -            else
  -                // case: a, h1 and h2 meet balance requirement
  -                AvlTree.Create (k, t1, t2)
   
       //
       static member private CompareStacks (comparer : IComparer<'T>, l1 : AvlTree<'T> list, l2 : AvlTree<'T> list) : int =
  
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.
  