anchor.diff:        | Branch(p,b,l,r) ->
             if k land (b - 1) <> p then newbranch p t k (Leaf(k,[x,y]))
             else if k land b = 0 then Branch(p,b,upd l,r)
  -          else Branch(p,b,l,upd r) in
  -    upd in
  +          else Branch(p,b,l,upd r)
  +    upd
     let rec combine op z t1 t2 =
       match (t1,t2) with
         Empty,_ -> t2
       | _,Empty -> t1
       | Leaf(h1,l1),Leaf(h2,l2) ->
             if h1 = h2 then
  -            let l = combine_list op z l1 l2 in
  +            let l = combine_list op z l1 l2
               if l = [] then Empty else Leaf(h1,l)
             else newbranch h1 t1 h2 t2
       | (Leaf(k,lis) as lf),(Branch(p,b,l,r) as br) ->
  
positive.code: *)
  
  /// Various useful general library functions.
  module NHol.lib
  
  open FSharp.Compatibility.OCaml
  
  
  let fail() = raise <| exn ()
  
  (* ------------------------------------------------------------------------- *)
  (* Combinators.                                                              *)
  (* ------------------------------------------------------------------------- *)
  
  let curry f x y = f(x,y)
  
  let uncurry f (x,y) = f x y
  
  let I x = x
  
  let K x y = x
  
  let C f x y = f y x
  
  let W f x = f x x
  
  // NOTE : Replaced all uses of (o) with (<<) since F# does not allow (o) to be used as an infix operator.
  
  let (F_F) = fun f g (x,y) -> (f x, g y)
  
  (* ------------------------------------------------------------------------- *)
  (* List basics.                                                              *)
  (* ------------------------------------------------------------------------- *)
  
  // OPTIMIZE : Make this an alias for List.head.
  let hd l =
    match l with
     h::t -> h
    | _ -> failwith "hd";;
  
  // OPTIMIZE : Make this an alias for List.tail.
  let tl l =
    match l with
     h::t -> t
    | _ -> failwith "tl";;
  
  // OPTIMIZE : Make this an alias for List.map.
  let map f =
    let rec mapf l =
      match l with
        [] -> []
      | (x::t) -> let y = f x in y::(mapf t) in
    mapf;;
  
  // OPTIMIZE : Make this an alias for List.last.
  let rec last l =
    match l with
      [x] -> x
    | (h::t) -> last t
    | [] -> failwith "last";;
  
  // OPTIMIZE : Make this an alias for List.dropLast.
  let rec butlast l =
    match l with
      [_] -> []
    | (h::t) -> h::(butlast t)
    | [] -> failwith "butlast";;
  
  // OPTIMIZE : Make this an alias for List.nth.
  let rec el n l =
    if n = 0 then hd l else el (n - 1) (tl l);;
  
  // OPTIMIZE : Make this an alias for List.rev.
  let rev =
    let rec rev_append acc l =
      match l with
        [] -> acc
      | h::t -> rev_append (h::acc) t in
    fun l -> rev_append [] l;;
  
  // OPTIMIZE : Make this an alias for List.map2.
  let rec map2 f l1 l2 =
    match (l1,l2) with
      [],[] -> []
    | (h1::t1),(h2::t2) -> let h = f h1 h2 in h::(map2 f t1 t2)
    | _ -> failwith "map2: length mismatch";;
  
  (* ------------------------------------------------------------------------- *)
  (* Attempting function or predicate applications.                            *)
  (* ------------------------------------------------------------------------- *)
  
  let can f x = try (f x; true) with Failure _ -> false;;
  
  let check p x = if p x then x else failwith "check";;
  
  (* ------------------------------------------------------------------------- *)
  (* Repetition of a function.                                                 *)
  (* ------------------------------------------------------------------------- *)
  
  let rec funpow n f x =
    if n < 1 then x else funpow (n-1) f (f x);;
  
  let rec repeat f x =
    try let y = f x in repeat f y with Failure _ -> x;;
  
  (* ------------------------------------------------------------------------- *)
  (* To avoid consing in various situations, we propagate this exception.      *)
  (* I should probably eliminate this and use pointer EQ tests instead.        *)
  (* ------------------------------------------------------------------------- *)
  
  exception Unchanged;;
  
  (* ------------------------------------------------------------------------- *)
  (* Various versions of list iteration.                                       *)
  (* ------------------------------------------------------------------------- *)
  
  // OPTIMIZE : Make this an alias for List.fold.
  let rec itlist f l b =
    match l with
      [] -> b
    | (h::t) -> f h (itlist f t b);;
  
  // OPTIMIZE : Make this an alias for List.foldBack.
  let rec rev_itlist f l b =
    match l with
      [] -> b
    | (h::t) -> rev_itlist f t (f h b);;
  
  // OPTIMIZE : Make this an alias for List.reduceBack.
  let rec end_itlist f l =
    match l with
          []     -> failwith "end_itlist"
        | [x]    -> x
        | (h::t) -> f h (end_itlist f t);;
  
  // OPTIMIZE : Make this an alias for List.fold2.
  let rec itlist2 f l1 l2 b =
    match (l1,l2) with
      ([],[]) -> b
    | (h1::t1,h2::t2) -> f h1 h2 (itlist2 f t1 t2 b)
    | _ -> failwith "itlist2";;
  
  // OPTIMIZE : Make this an alias for List.foldBack2.
  let rec rev_itlist2 f l1 l2 b =
     match (l1,l2) with
       ([],[]) -> b
     | (h1::t1,h2::t2) -> rev_itlist2 f t1 t2 (f h1 h2 b)
        | _ -> failwith "rev_itlist2";;
  
  (* ------------------------------------------------------------------------- *)
  (* Iterative splitting (list) and stripping (tree) via destructor.           *)
  (* ------------------------------------------------------------------------- *)
  
  let rec splitlist dest x =
    try let l,r = dest x in
        let ls,res = splitlist dest r in
        (l::ls,res)
    with Failure _ -> ([],x);;
  
  let rev_splitlist dest =
    let rec rsplist ls x =
      try let l,r = dest x in
          rsplist (r::ls) l
      with Failure _ -> (x,ls) in
    fun x -> rsplist [] x;;
  
  let striplist dest =
    let rec strip x acc =
      try let l,r = dest x in
          strip l (strip r acc)
      with Failure _ -> x::acc in
    fun x -> strip x [];;
  
  (* ------------------------------------------------------------------------- *)
  (* Apply a destructor as many times as elements in list.                     *)
  (* ------------------------------------------------------------------------- *)
  
  let rec nsplit dest clist x =
    if clist = [] then [],x else
    let l,r = dest x in
    let ll,y = nsplit dest (tl clist) r in
    l::ll,y;;
  
  (* ------------------------------------------------------------------------- *)
  (* Replication and sequences.                                                *)
  (* ------------------------------------------------------------------------- *)
  
  // OPTIMIZE : Make this an alias for List.replicate.
  let rec replicate x n =
      if n < 1 then []
      else x::(replicate x (n - 1));;
  
  // OPTIMIZE : Make this an alias for [m..n]
  let rec (--) = fun m n -> if m > n then [] else m::((m + 1) -- n);;
  
  (* ------------------------------------------------------------------------- *)
  (* Various useful list operations.                                           *)
  (* ------------------------------------------------------------------------- *)
  
  // OPTIMIZE : Make this an alias for List.forall.
  let rec forall p l =
    match l with
      [] -> true
    | h::t -> p(h) & forall p t;;
  
  // OPTIMIZE : Make this an alias for List.forall2.
  let rec forall2 p l1 l2 =
    match (l1,l2) with
      [],[] -> true
    | (h1::t1,h2::t2) -> p h1 h2 && forall2 p t1 t2
    | _ -> false;;
  
  // OPTIMIZE : Make this an alias for List.exists.
  let rec exists p l =
    match l with
      [] -> false
    | h::t -> p(h) || exists p t;;
  
  // OPTIMIZE : Make this an alias for List.length.
  let length =
    let rec len k l =
      if l = [] then k else len (k + 1) (tl l) in
    fun l -> len 0 l;;
  
  // OPTIMIZE : Make this an alias for List.filter.
  let rec filter p l =
    match l with
      [] -> l
    | h::t -> let t' = filter p t in
              if p(h) then if t'==t then l else h::t'
              else t';;
  
  // OPTIMIZE : Make this an alias for List.partition.
  let rec partition p l =
    match l with
      [] -> [],l
    | h::t -> let yes,no = partition p t in
              if p(h) then (if yes == t then l,[] else h::yes,no)
              else (if no == t then [],l else yes,h::no);;
  
  // OPTIMIZE : Make this an alias for List.choose.
  let rec mapfilter f l =
    match l with
      [] -> []
    | (h::t) -> let rest = mapfilter f t in
                try (f h)::rest with Failure _ -> rest;;
  
  // OPTIMIZE : Make this an alias for List.find.
  let rec find p l =
    match l with
        [] -> failwith "find"
      | (h::t) -> if p(h) then h else find p t;;
  
  // OPTIMIZE : Make this an alias for List.tryFind.
  let rec tryfind f l =
    match l with
        [] -> failwith "tryfind"
      | (h::t) -> try f h with Failure _ -> tryfind f t;;
  
  // OPTIMIZE : Make this an alias for List.concat.
  let flat l = itlist (@) l [];;
  
  // OPTIMIZE : Rewrite this function using a list-based zipper.
  // This way the function will be tail-recursive and much faster.
  let rec remove p l =
    match l with
      [] -> failwith "remove"
    | (h::t) -> if p(h) then h,t else
                let y,n = remove p t in y,h::n;;
  
  // OPTIMIZE : Make this an alias for List.take.
  let rec chop_list n l =
    if n = 0 then [],l else
    try let m,l' = chop_list (n-1) (tl l) in (hd l)::m,l'
    with Failure _ -> failwith "chop_list";;
  
  // OPTIMIZE : Make this an alias for List.findIndex.
  let index x =
    let rec ind n l =
      match l with
        [] -> failwith "index"
      | (h::t) -> if compare x h = 0 then n else ind (n + 1) t in
    ind 0;;
  
  (* ------------------------------------------------------------------------- *)
  (* "Set" operations on lists.                                                *)
  (* ------------------------------------------------------------------------- *)
  
  let rec mem x lis =
    match lis with
      [] -> false
    | (h::t) -> compare x h = 0 || mem x t;;
  
  let insert x l =
    if mem x l then l else x::l;;
  
  let union l1 l2 = itlist insert l1 l2;;
  
  let unions l = itlist union l [];;
  
  let intersect l1 l2 = filter (fun x -> mem x l2) l1;;
  
  let subtract l1 l2 = filter (fun x -> not (mem x l2)) l1;;
  
  let subset l1 l2 = forall (fun t -> mem t l2) l1;;
  
  let set_eq l1 l2 = subset l1 l2 && subset l2 l1;;
  
  (* ------------------------------------------------------------------------- *)
  (* Association lists.                                                        *)
  (* ------------------------------------------------------------------------- *)
  
  let rec assoc a l =
    match l with
      (x,y)::t -> if compare x a = 0 then y else assoc a t
    | [] -> failwith "find";;
  
  let rec rev_assoc a l =
    match l with
      (x,y)::t -> if compare y a = 0 then x else rev_assoc a t
    | [] -> failwith "find";;
  
  (* ------------------------------------------------------------------------- *)
  (* Zipping, unzipping etc.                                                   *)
  (* ------------------------------------------------------------------------- *)
  
  // OPTIMIZE : Make this an alias for List.zip.
  let rec zip l1 l2 =
    match (l1,l2) with
          ([],[]) -> []
        | (h1::t1,h2::t2) -> (h1,h2)::(zip t1 t2)
        | _ -> failwith "zip";;
  
  // OPTIMIZE : Make this an alias for List.unzip.
  let rec unzip =
    function [] -> [],[]
           | ((a,b)::rest) -> let alist,blist = unzip rest in
                              (a::alist,b::blist);;
  
  (* ------------------------------------------------------------------------- *)
  (* Sharing out a list according to pattern in list-of-lists.                 *)
  (* ------------------------------------------------------------------------- *)
  
  let rec shareout pat all =
    if pat = [] then [] else
    let l,r = chop_list (length (hd pat)) all in
    l::(shareout (tl pat) r);;
  
  (* ------------------------------------------------------------------------- *)
  (* Iterating functions over lists.                                           *)
  (* ------------------------------------------------------------------------- *)
  
  // OPTIMIZE : Make this an alias for List.iter.
  let rec do_list f l =
    match l with
      [] -> ()
    | (h::t) -> (f h; do_list f t);;
  
  (* ------------------------------------------------------------------------- *)
  (* Sorting.                                                                  *)
  (* ------------------------------------------------------------------------- *)
  
  // OPTIMIZE : Make this an alias for List.sortWith.
  let rec sort cmp lis =
    match lis with
      [] -> []
    | piv::rest ->
        let r,l = partition (cmp piv) rest in
        (sort cmp l) @ (piv::(sort cmp r));;
  
  (* ------------------------------------------------------------------------- *)
  (* Removing adjacent (NB!) equal elements from list.                         *)
  (* ------------------------------------------------------------------------- *)
  
  let rec uniq l =
    match l with
    | x::(y::_ as t) -> let t' = uniq t in
                        if compare x y = 0 then t' else
                        if t'==t then l else x::t'
    | _ -> l;;
  
  (* ------------------------------------------------------------------------- *)
  (* Convert list into set by eliminating duplicates.                          *)
  (* ------------------------------------------------------------------------- *)
  
  let setify s = uniq (sort (fun x y -> compare x y <= 0) s);;
  
  (* ------------------------------------------------------------------------- *)
  (* String operations (surely there is a better way...)                       *)
  (* ------------------------------------------------------------------------- *)
  
  // OPTIMIZE : Make this an alias for List.sortWith.
  let implode l = itlist (^) l "";;
  
  let explode s =
    let rec exap n l =
        if n < 0 then l else
        exap (n - 1) ((String.sub s n 1)::l) in
    exap (String.length s - 1) [];;
  
  (* ------------------------------------------------------------------------- *)
  (* Greatest common divisor.                                                  *)
  (* ------------------------------------------------------------------------- *)
  
  let gcd =
    let rec gxd x y =
      if y = 0 then x else gxd y (x mod y) in
    fun x y ->
      let x' = abs x
      let y' = abs y in
      if x' < y' then gxd y' x' else gxd x' y';;
  
  (* ------------------------------------------------------------------------- *)
  (* Some useful functions on "num" type.                                      *)
  (* ------------------------------------------------------------------------- *)
  
  let num_0 = Int 0
  let num_1 = Int 1
  let num_2 = Int 2
  let num_10 = Int 10;;
  
  let pow2 n = power_num num_2 (Int n);;
  let pow10 n = power_num num_10 (Int n);;
  
  let numdom r =
    let r' = Ratio.normalize_ratio (ratio_of_num r) in
    num_of_big_int(Ratio.numerator_ratio r'),
    num_of_big_int(Ratio.denominator_ratio r');;
  
  let numerator = fst o numdom
  let denominator = snd o numdom;;
  
  let gcd_num n1 n2 =
    num_of_big_int(Big_int.gcd_big_int (big_int_of_num n1) (big_int_of_num n2));;
  
  let lcm_num x y =
    if x =/ num_0 & y =/ num_0 then num_0
    else abs_num((x */ y) / gcd_num x y);;
  
  (* ------------------------------------------------------------------------- *)
  (* All pairs arising from applying a function over two lists.                *)
  (* ------------------------------------------------------------------------- *)
  
  let rec allpairs f l1 l2 =
    match l1 with
     h1::t1 ->  itlist (fun x a -> f h1 x :: a) l2 (allpairs f t1 l2)
    | [] -> [];;
  
  (* ------------------------------------------------------------------------- *)
  (* Issue a report with a newline.                                            *)
  (* ------------------------------------------------------------------------- *)
  
  let report s =
    Format.print_string s; Format.print_newline();;
  
  (* ------------------------------------------------------------------------- *)
  (* Convenient function for issuing a warning.                                *)
  (* ------------------------------------------------------------------------- *)
  
  let warn cond s =
    if cond then report ("Warning: "^s) else ();;
  
  (* ------------------------------------------------------------------------- *)
  (* Flags to switch on verbose mode.                                          *)
  (* ------------------------------------------------------------------------- *)
  
  let verbose = ref true;;
  let report_timing = ref true;;
  
  (* ------------------------------------------------------------------------- *)
  (* Switchable version of "report".                                           *)
  (* ------------------------------------------------------------------------- *)
  
  let remark s =
    if !verbose then report s else ();;
  
  (* ------------------------------------------------------------------------- *)
  (* Time a function.                                                          *)
  (* ------------------------------------------------------------------------- *)
  
  let time f x =
    if not (!report_timing) then f x else
    let start_time = Sys.time() in
    try let result = f x in
        let finish_time = Sys.time() in
        report("CPU time (user): "^(string_of_float(finish_time -. start_time)));
        result
    with e ->
        let finish_time = Sys.time() in
        Format.print_string("Failed after (user) CPU time of "^
                            (string_of_float(finish_time -. start_time))^": ");
        raise e;;
  
  (* ------------------------------------------------------------------------- *)
  (* Versions of assoc and rev_assoc with default rather than failure.         *)
  (* ------------------------------------------------------------------------- *)
  
  let rec assocd a l d =
    match l with
      [] -> d
    | (x,y)::t -> if compare x a = 0 then y else assocd a t d;;
  
  let rec rev_assocd a l d =
    match l with
      [] -> d
    | (x,y)::t -> if compare y a = 0 then x else rev_assocd a t d;;
  
  (* ------------------------------------------------------------------------- *)
  (* Version of map that avoids rebuilding unchanged subterms.                 *)
  (* ------------------------------------------------------------------------- *)
  
  let rec qmap f l =
    match l with
      h::t ->
          let h' = f h
          let t' = qmap f t in
          if h' == h && t' == t then l else h'::t'
    | _ -> l;;
  
  (* ------------------------------------------------------------------------- *)
  (* Merging and bottom-up mergesort.                                          *)
  (* ------------------------------------------------------------------------- *)
  
  let rec merge ord l1 l2 =
    match l1 with
      [] -> l2
    | h1::t1 -> match l2 with
                  [] -> l1
                | h2::t2 -> if ord h1 h2 then h1::(merge ord t1 l2)
                            else h2::(merge ord l1 t2);;
  
  let mergesort ord =
    let rec mergepairs l1 l2 =
      match (l1,l2) with
          ([s],[]) -> s
        | (l,[]) -> mergepairs [] l
        | (l,[s1]) -> mergepairs (s1::l) []
        | (l,(s1::s2::ss)) -> mergepairs ((merge ord s1 s2)::l) ss in
    fun l -> if l = [] then [] else mergepairs [] (map (fun x -> [x]) l);;
  
  (* ------------------------------------------------------------------------- *)
  (* Common measure predicates to use with "sort".                             *)
  (* ------------------------------------------------------------------------- *)
  
  let increasing f x y = compare (f x) (f y) < 0;;
  
  let decreasing f x y = compare (f x) (f y) > 0;;
  
  (* ------------------------------------------------------------------------- *)
  (* Polymorphic finite partial functions via Patricia trees.                  *)
  
negative.code:       [],_ -> l2
      | _,[] -> l1
      | ((x1,y1 as xy1)::t1,(x2,y2 as xy2)::t2) ->
            let c = Pervasives.compare x1 x2
            if c < 0 then xy1::(combine_list op z t1 l2)
            else if c > 0 then xy2::(combine_list op z l1 t2) else
            let rec y = op y1 y2 and l = combine_list op z t1 t2
            if z(y) then l else (x1,y)::l
  
    let (|->) x y =
      let k = Hashtbl.hash x
      let rec upd t =
        match t with
          Empty -> Leaf (k,[x,y])
  