anchor.diff:      let rec add value (tree : CharDiet) : CharDiet =
           // Preconditions
           assert (dietInvariant tree)
  +        assert (fst <| intervalsDisjoint tree Set.empty)
   
           match tree with
           | Empty ->
               singleton value
  -            |> tap (fun x -> assert (dietInvariant x))
  +            |> tap (fun x ->
  +                assert (dietInvariant x)
  +                assert (fst <| intervalsDisjoint x Set.empty))
           | Node (left, right, (x, y), h) ->
               if value >= x then
                   if value <= y then
                       // The value is already in [x, y] so the tree
                       // does not need to be modified.
                       tree
  -                    |> tap (fun x -> assert (dietInvariant x))
  +                    |> tap (fun x ->
  +                        assert (dietInvariant x)
  +                        assert (fst <| intervalsDisjoint x Set.empty))
                   elif value > succ y then
                       // The value is above the interval and is not adjacent
                       // to it, so recurse down the right subtree to add the value
                       // then join the result with the left subtree.
                       CharDiet.Join (comparer, left, add value right, (x, y))
  -                    |> tap (fun x -> assert (dietInvariant x))
  +                    |> tap (fun x ->
  +                        assert (dietInvariant x)
  +                        assert (fst <| intervalsDisjoint x Set.empty))
                   else
                       match right with
                       | Empty ->
                           CharDiet.Create ((x, value), left, Empty)
  -                        |> tap (fun x -> assert (dietInvariant x))
  +                        |> tap (fun x ->
  +                            assert (dietInvariant x)
  +                            assert (fst <| intervalsDisjoint x Set.empty))
                       | _ ->
                           let (u, v), r = CharDiet.DeleteMin right
                           if pred u = value then
                               CharDiet.Join (comparer, left, r, (x, v))
  -                            |> tap (fun x -> assert (dietInvariant x))
  +                            |> tap (fun x ->
  +                                assert (dietInvariant x)
  +                                assert (fst <| intervalsDisjoint x Set.empty))
                           else
                               CharDiet.Create ((x, value), left, right)
  -                            |> tap (fun x -> assert (dietInvariant x))
  +                            |> tap (fun x ->
  +                                assert (dietInvariant x)
  +                                assert (fst <| intervalsDisjoint x Set.empty))
   
               elif value < pred x then
                   CharDiet.Join (comparer, add value left, right, (x, y))
  -                |> tap (fun x -> assert (dietInvariant x))
  +                |> tap (fun x ->
  +                    assert (dietInvariant x)
  +                    assert (fst <| intervalsDisjoint x Set.empty))
               else
                   match left with
                   | Empty ->
                       CharDiet.Create ((value, y), Empty, right)
  -                    |> tap (fun x -> assert (dietInvariant x))
  +                    |> tap (fun x ->
  +                        assert (dietInvariant x)
  +                        assert (fst <| intervalsDisjoint x Set.empty))
                   | _ ->
                       let (u, v), l = CharDiet.DeleteMax left
                       if succ v = value then
                           CharDiet.Join (comparer, l, right, (u, y))
  -                        |> tap (fun x -> assert (dietInvariant x))
  +                        |> tap (fun x ->
  +                            assert (dietInvariant x)
  +                            assert (fst <| intervalsDisjoint x Set.empty))
                       else
                           CharDiet.Create ((value, y), left, right)
  -                        |> tap (fun x -> assert (dietInvariant x))
  +                        |> tap (fun x ->
  +                            assert (dietInvariant x)
  +                            assert (fst <| intervalsDisjoint x Set.empty))
   
       /// Returns a new set with the specified range of values added to the set.
       /// No exception is thrown if any of the values are already contained in the set.
  
positive.code:     let maxElement (tree : CharDiet) : char =
          // Preconditions
          assert (dietInvariant tree)
  
          match tree with
          | Empty ->
  
negative.code:     let rec internal (*private*) find_del_right p (tree : CharDiet) : char * CharDiet =
          // Preconditions
          assert (dietInvariant tree)
          assert (fst <| intervalsDisjoint tree Set.empty)
  
          match tree with
          | Empty ->
  