type __ = Obj.t
let __ = let rec f _ = Obj.repr f in Obj.repr f

type nat =
  | O
  | S of nat

type ('a, 'b) prod =
  | Pair of 'a * 'b

type 'a sig0 = 'a
  (* singleton inductive, whose constructor was exist *)

(** val plus : nat -> nat -> nat **)

let rec plus n m =
  match n with
    | O -> m
    | S p -> S (plus p m)

type 'a list =
  | Nil
  | Cons of 'a * 'a list

(** val app : 'a1 list -> 'a1 list -> 'a1 list **)

let rec app l m =
  match l with
    | Nil -> m
    | Cons (a, l1) -> Cons (a, (app l1 m))

type 'x compare =
  | Lt
  | Eq
  | Gt

module type OrderedType = 
 sig 
  type t 
  
  val compare : t -> t -> t compare
 end

module MoreOrderedType = 
 functor (O:OrderedType) ->
 struct 
  (** val eq_dec : O.t -> O.t -> bool **)
  
  let eq_dec x y =
    match O.compare x y with
      | Lt -> false
      | Eq -> true
      | Gt -> false
  
  (** val lt_dec : O.t -> O.t -> bool **)
  
  let lt_dec x y =
    match O.compare x y with
      | Lt -> true
      | Eq -> false
      | Gt -> false
 end

type positive =
  | XI of positive
  | XO of positive
  | XH

type z =
  | ZERO
  | POS of positive
  | NEG of positive

type relation =
  | EGAL
  | INFERIEUR
  | SUPERIEUR

(** val add_un : positive -> positive **)

let rec add_un = function
  | XI x' -> XO (add_un x')
  | XO x' -> XI x'
  | XH -> XO XH

(** val add : positive -> positive -> positive **)

let rec add x y =
  match x with
    | XI x' ->
        (match y with
           | XI y' -> XO (add_carry x' y')
           | XO y' -> XI (add x' y')
           | XH -> XO (add_un x'))
    | XO x' ->
        (match y with
           | XI y' -> XI (add x' y')
           | XO y' -> XO (add x' y')
           | XH -> XI x')
    | XH ->
        (match y with
           | XI y' -> XO (add_un y')
           | XO y' -> XI y'
           | XH -> XO XH)

(** val add_carry : positive -> positive -> positive **)

and add_carry x y =
  match x with
    | XI x' ->
        (match y with
           | XI y' -> XI (add_carry x' y')
           | XO y' -> XO (add_carry x' y')
           | XH -> XI (add_un x'))
    | XO x' ->
        (match y with
           | XI y' -> XO (add_carry x' y')
           | XO y' -> XI (add x' y')
           | XH -> XO (add_un x'))
    | XH ->
        (match y with
           | XI y' -> XI (add_un y')
           | XO y' -> XO (add_un y')
           | XH -> XI XH)

(** val double_moins_un : positive -> positive **)

let rec double_moins_un = function
  | XI x' -> XI (XO x')
  | XO x' -> XI (double_moins_un x')
  | XH -> XH

(** val compare0 : positive -> positive -> relation -> relation **)

let rec compare0 x y r =
  match x with
    | XI x' ->
        (match y with
           | XI y' -> compare0 x' y' r
           | XO y' -> compare0 x' y' SUPERIEUR
           | XH -> SUPERIEUR)
    | XO x' ->
        (match y with
           | XI y' -> compare0 x' y' INFERIEUR
           | XO y' -> compare0 x' y' r
           | XH -> SUPERIEUR)
    | XH ->
        (match y with
           | XI y' -> INFERIEUR
           | XO y' -> INFERIEUR
           | XH -> r)

type entier =
  | Nul
  | Pos of positive

(** val un_suivi_de : entier -> entier **)

let un_suivi_de = function
  | Nul -> Pos XH
  | Pos p -> Pos (XI p)

(** val zero_suivi_de : entier -> entier **)

let zero_suivi_de = function
  | Nul -> Nul
  | Pos p -> Pos (XO p)

(** val double_moins_deux : positive -> entier **)

let double_moins_deux = function
  | XI x' -> Pos (XO (XO x'))
  | XO x' -> Pos (XO (double_moins_un x'))
  | XH -> Nul

(** val sub_pos : positive -> positive -> entier **)

let rec sub_pos x y =
  match x with
    | XI x' ->
        (match y with
           | XI y' -> zero_suivi_de (sub_pos x' y')
           | XO y' -> un_suivi_de (sub_pos x' y')
           | XH -> Pos (XO x'))
    | XO x' ->
        (match y with
           | XI y' -> un_suivi_de (sub_neg x' y')
           | XO y' -> zero_suivi_de (sub_pos x' y')
           | XH -> Pos (double_moins_un x'))
    | XH ->
        (match y with
           | XI y' -> Pos (double_moins_un y')
           | XO y' -> double_moins_deux y'
           | XH -> Nul)

(** val sub_neg : positive -> positive -> entier **)

and sub_neg x y =
  match x with
    | XI x' ->
        (match y with
           | XI y' -> un_suivi_de (sub_neg x' y')
           | XO y' -> zero_suivi_de (sub_pos x' y')
           | XH -> Pos (double_moins_un x'))
    | XO x' ->
        (match y with
           | XI y' -> zero_suivi_de (sub_neg x' y')
           | XO y' -> un_suivi_de (sub_neg x' y')
           | XH -> double_moins_deux x')
    | XH ->
        (match y with
           | XI y' -> Pos (XO y')
           | XO y' -> Pos (double_moins_un y')
           | XH -> Nul)

(** val op : relation -> relation **)

let op = function
  | EGAL -> EGAL
  | INFERIEUR -> SUPERIEUR
  | SUPERIEUR -> INFERIEUR

(** val zplus : z -> z -> z **)

let zplus x y =
  match x with
    | ZERO -> y
    | POS x' ->
        (match y with
           | ZERO -> x
           | POS y' -> POS (add x' y')
           | NEG y' ->
               (match compare0 x' y' EGAL with
                  | EGAL -> ZERO
                  | INFERIEUR -> NEG
                      (match sub_pos y' x' with
                         | Nul -> XH
                         | Pos z0 -> z0)
                  | SUPERIEUR -> POS
                      (match sub_pos x' y' with
                         | Nul -> XH
                         | Pos z0 -> z0)))
    | NEG x' ->
        (match y with
           | ZERO -> x
           | POS y' ->
               (match compare0 x' y' EGAL with
                  | EGAL -> ZERO
                  | INFERIEUR -> POS
                      (match sub_pos y' x' with
                         | Nul -> XH
                         | Pos z0 -> z0)
                  | SUPERIEUR -> NEG
                      (match sub_pos x' y' with
                         | Nul -> XH
                         | Pos z0 -> z0))
           | NEG y' -> NEG (add x' y'))

(** val times : positive -> positive -> positive **)

let rec times x y =
  match x with
    | XI x' -> add y (XO (times x' y))
    | XO x' -> XO (times x' y)
    | XH -> y

(** val zmult : z -> z -> z **)

let zmult x y =
  match x with
    | ZERO -> ZERO
    | POS x' ->
        (match y with
           | ZERO -> ZERO
           | POS y' -> POS (times x' y')
           | NEG y' -> NEG (times x' y'))
    | NEG x' ->
        (match y with
           | ZERO -> ZERO
           | POS y' -> NEG (times x' y')
           | NEG y' -> POS (times x' y'))

(** val zcompare : z -> z -> relation **)

let zcompare x y =
  match x with
    | ZERO ->
        (match y with
           | ZERO -> EGAL
           | POS y' -> INFERIEUR
           | NEG y' -> SUPERIEUR)
    | POS x' ->
        (match y with
           | ZERO -> SUPERIEUR
           | POS y' -> compare0 x' y' EGAL
           | NEG y' -> SUPERIEUR)
    | NEG x' ->
        (match y with
           | ZERO -> INFERIEUR
           | POS y' -> INFERIEUR
           | NEG y' -> op (compare0 x' y' EGAL))

(** val lt_eq_lt_dec : nat -> nat -> bool option **)

let rec lt_eq_lt_dec n m =
  match n with
    | O -> (match m with
              | O -> Some false
              | S n0 -> Some true)
    | S n0 ->
        (match m with
           | O -> None
           | S n1 ->
               (match lt_eq_lt_dec n0 n1 with
                  | Some x -> Some x
                  | None -> None))

(** val sumbool_not : bool -> bool **)

let sumbool_not = function
  | true -> false
  | false -> true

(** val dcompare_inf : relation -> bool option **)

let dcompare_inf = function
  | EGAL -> Some (sumbool_not (sumbool_not true))
  | INFERIEUR -> Some (sumbool_not (sumbool_not false))
  | SUPERIEUR -> None

(** val zcompare_rec : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
                       'a1) -> 'a1 **)

let zcompare_rec x y h1 h2 h3 =
  match dcompare_inf (zcompare x y) with
    | Some x0 -> (match x0 with
                    | true -> h1 __
                    | false -> h2 __)
    | None -> h3 __

(** val z_eq_dec : z -> z -> bool **)

let z_eq_dec x y =
  zcompare_rec x y (fun _ -> true) (fun _ -> false) (fun _ -> false)

(** val z_lt_dec : z -> z -> bool **)

let z_lt_dec x y =
  zcompare_rec x y (fun _ -> false) (fun _ -> true) (fun _ -> false)

(** val z_gt_dec : z -> z -> bool **)

let z_gt_dec x y =
  zcompare_rec x y (fun _ -> false) (fun _ -> false) (fun _ -> true)

(** val z_ge_dec : z -> z -> bool **)

let z_ge_dec x y =
  zcompare_rec x y (fun _ -> true) (fun _ -> false) (fun _ -> true)

(** val z_lt_ge_dec : z -> z -> bool **)

let z_lt_ge_dec x y =
  z_lt_dec x y

(** val z_gt_le_dec : z -> z -> bool **)

let z_gt_le_dec x y =
  z_gt_dec x y

(** val z_ge_lt_dec : z -> z -> bool **)

let z_ge_lt_dec x y =
  match z_ge_dec x y with
    | true -> sumbool_not (sumbool_not (sumbool_not false))
    | false -> false

module Raw = 
 functor (X:OrderedType) ->
 struct 
  module E = X
  
  module ME = MoreOrderedType(X)
  
  type elt = E.t
  
  type t = elt list
  
  (** val empty : t **)
  
  let empty =
    Nil
  
  (** val is_empty : t -> bool **)
  
  let is_empty = function
    | Nil -> true
    | Cons (x, x0) -> false
  
  (** val mem : elt -> t -> bool **)
  
  let rec mem x = function
    | Nil -> false
    | Cons (y, l) ->
        (match E.compare x y with
           | Lt -> false
           | Eq -> true
           | Gt -> mem x l)
  
  (** val add : elt -> t -> t **)
  
  let rec add x s = match s with
    | Nil -> Cons (x, Nil)
    | Cons (y, l) ->
        (match E.compare x y with
           | Lt -> Cons (x, s)
           | Eq -> s
           | Gt -> Cons (y, (add x l)))
  
  (** val singleton : elt -> t **)
  
  let singleton x =
    Cons (x, Nil)
  
  (** val remove : elt -> t -> t **)
  
  let rec remove x s = match s with
    | Nil -> Nil
    | Cons (y, l) ->
        (match E.compare x y with
           | Lt -> s
           | Eq -> l
           | Gt -> Cons (y, (remove x l)))
  
  (** val union : t -> t -> t **)
  
  let rec union s x =
    match s with
      | Nil -> x
      | Cons (x0, l) ->
          let rec union_aux s' = match s' with
            | Nil -> s
            | Cons (x', l') ->
                (match E.compare x0 x' with
                   | Lt -> Cons (x0, (union l s'))
                   | Eq -> Cons (x0, (union l l'))
                   | Gt -> Cons (x', (union_aux l')))
          in union_aux x
  
  (** val inter : t -> t -> t **)
  
  let rec inter s x =
    match s with
      | Nil -> Nil
      | Cons (x0, l) ->
          let rec inter_aux s' = match s' with
            | Nil -> Nil
            | Cons (x', l') ->
                (match E.compare x0 x' with
                   | Lt -> inter l s'
                   | Eq -> Cons (x0, (inter l l'))
                   | Gt -> inter_aux l')
          in inter_aux x
  
  (** val diff : t -> t -> t **)
  
  let rec diff s x =
    match s with
      | Nil -> Nil
      | Cons (x0, l) ->
          let rec diff_aux s' = match s' with
            | Nil -> s
            | Cons (x', l') ->
                (match E.compare x0 x' with
                   | Lt -> Cons (x0, (diff l s'))
                   | Eq -> diff l l'
                   | Gt -> diff_aux l')
          in diff_aux x
  
  (** val equal : t -> t -> bool **)
  
  let rec equal s s' =
    match s with
      | Nil -> (match s' with
                  | Nil -> true
                  | Cons (e, l) -> false)
      | Cons (x, l) ->
          (match s' with
             | Nil -> false
             | Cons (x', l') ->
                 (match E.compare x x' with
                    | Lt -> false
                    | Eq -> equal l l'
                    | Gt -> false))
  
  (** val subset : t -> t -> bool **)
  
  let rec subset s s' =
    match s with
      | Nil -> true
      | Cons (x, l) ->
          (match s' with
             | Nil -> false
             | Cons (x', l') ->
                 (match E.compare x x' with
                    | Lt -> false
                    | Eq -> subset l l'
                    | Gt -> subset s l'))
  
  (** val fold : (elt -> 'a1 -> 'a1) -> t -> 'a1 -> 'a1 **)
  
  let rec fold f s i =
    match s with
      | Nil -> i
      | Cons (x, l) -> f x (fold f l i)
  
  (** val filter : (elt -> bool) -> t -> t **)
  
  let rec filter f = function
    | Nil -> Nil
    | Cons (x, l) ->
        (match f x with
           | true -> Cons (x, (filter f l))
           | false -> filter f l)
  
  (** val for_all : (elt -> bool) -> t -> bool **)
  
  let rec for_all f = function
    | Nil -> true
    | Cons (x, l) ->
        (match f x with
           | true -> for_all f l
           | false -> false)
  
  (** val exists : (elt -> bool) -> t -> bool **)
  
  let rec exists f = function
    | Nil -> false
    | Cons (x, l) ->
        (match f x with
           | true -> true
           | false -> exists f l)
  
  (** val partition : (elt -> bool) -> t -> (t, t) prod **)
  
  let rec partition f = function
    | Nil -> Pair (Nil, Nil)
    | Cons (x, l) ->
        let Pair (s1, s2) = partition f l in
        (match f x with
           | true -> Pair ((Cons (x, s1)), s2)
           | false -> Pair (s1, (Cons (x, s2))))
  
  (** val cardinal : t -> nat **)
  
  let cardinal s =
    let rec fold0 f s0 i =
      match s0 with
        | Nil -> i
        | Cons (x, l) -> f x (fold0 f l i)
    in fold0 (fun x x0 -> S x0) s O
  
  (** val elements : t -> elt list **)
  
  let elements x =
    x
  
  (** val min_elt : t -> elt option **)
  
  let min_elt = function
    | Nil -> None
    | Cons (x, l) -> Some x
  
  (** val max_elt : t -> elt option **)
  
  let rec max_elt = function
    | Nil -> None
    | Cons (x, l) ->
        (match l with
           | Nil -> Some x
           | Cons (e, l0) -> max_elt l)
  
  (** val choose : t -> elt option **)
  
  let choose x =
    min_elt x
  
  (** val compare : t -> t -> t compare **)
  
  let rec compare l s' =
    match l with
      | Nil -> (match s' with
                  | Nil -> Eq
                  | Cons (e, l0) -> Lt)
      | Cons (a, l0) ->
          (match s' with
             | Nil -> Gt
             | Cons (a', l') ->
                 (match E.compare a a' with
                    | Lt -> Lt
                    | Eq ->
                        (match compare l0 l' with
                           | Lt -> Lt
                           | Eq -> Eq
                           | Gt -> Gt)
                    | Gt -> Gt))
 end

module Make = 
 functor (X:OrderedType) ->
 struct 
  module E = X
  
  module ME = MoreOrderedType(X)
  
  type elt = X.t
  
  type tree =
    | Leaf
    | Node of tree * X.t * tree * z
  
  (** val tree_rect : 'a1 -> (tree -> 'a1 -> X.t -> tree -> 'a1 -> z ->
                      'a1) -> tree -> 'a1 **)
  
  let rec tree_rect f f0 = function
    | Leaf -> f
    | Node (t1, t2, t3, z0) ->
        f0 t1 (tree_rect f f0 t1) t2 t3 (tree_rect f f0 t3) z0
  
  (** val tree_rec : 'a1 -> (tree -> 'a1 -> X.t -> tree -> 'a1 -> z ->
                     'a1) -> tree -> 'a1 **)
  
  let rec tree_rec f f0 = function
    | Leaf -> f
    | Node (t1, t2, t3, z0) ->
        f0 t1 (tree_rec f f0 t1) t2 t3 (tree_rec f f0 t3) z0
  
  (** val height : tree -> z **)
  
  let height = function
    | Leaf -> ZERO
    | Node (t0, t1, t2, h) -> h
  
  (** val max : z -> z -> z **)
  
  let max x y =
    match z_lt_ge_dec x y with
      | true -> y
      | false -> x
  
  type t_ =
    tree
    (* singleton inductive, whose constructor was t_intro *)
  
  (** val t__rect : (tree -> __ -> __ -> 'a1) -> t_ -> 'a1 **)
  
  let t__rect f t0 =
    f t0 __ __
  
  (** val t__rec : (tree -> __ -> __ -> 'a1) -> t_ -> 'a1 **)
  
  let t__rec f t0 =
    f t0 __ __
  
  (** val the_tree : t_ -> tree **)
  
  let the_tree t0 =
    t0
  
  type t = t_
  
  (** val t_empty : t **)
  
  let t_empty =
    Leaf
  
  (** val empty : t sig0 **)
  
  let empty =
    t_empty
  
  (** val is_empty : t -> bool **)
  
  let is_empty = function
    | Leaf -> true
    | Node (t0, t1, t2, z0) -> false
  
  (** val mem : elt -> t -> bool **)
  
  let rec mem x = function
    | Leaf -> false
    | Node (t0, t1, t2, z0) ->
        (match X.compare x t1 with
           | Lt -> mem x t0
           | Eq -> true
           | Gt -> mem x t2)
  
  (** val singleton_tree : elt -> tree **)
  
  let singleton_tree x =
    Node (Leaf, x, Leaf, (POS XH))
  
  (** val singleton : elt -> t sig0 **)
  
  let singleton x =
    singleton_tree x
  
  (** val create : tree -> elt -> tree -> tree sig0 **)
  
  let create l x r =
    Node (l, x, r, (zplus (max (height l) (height r)) (POS XH)))
  
  (** val bal : tree -> elt -> tree -> tree sig0 **)
  
  let bal l x r =
    match z_gt_le_dec (height l) (zplus (height r) (POS (XO XH))) with
      | true ->
          (match l with
             | Leaf -> assert false (* absurd case *)
             | Node (t0, t1, t2, z0) ->
                 (match z_ge_lt_dec (height t0) (height t2) with
                    | true -> create t0 t1 (create t2 x r)
                    | false ->
                        (match t2 with
                           | Leaf -> assert false (* absurd case *)
                           | Node (t3, t4, t5, z2) ->
                               create (create t0 t1 t3) t4
                                 (create t5 x r))))
      | false ->
          (match z_gt_le_dec (height r)
                   (zplus (height l) (POS (XO XH))) with
             | true ->
                 (match r with
                    | Leaf -> assert false (* absurd case *)
                    | Node (t0, t1, t2, z1) ->
                        (match z_ge_lt_dec (height t2) (height t0) with
                           | true -> create (create l x t0) t1 t2
                           | false ->
                               (match t0 with
                                  | Leaf -> assert false
                                      (* absurd case *)
                                  | Node (t3, t4, t5, z3) ->
                                      create (create l x t3) t4
                                        (create t5 t1 t2))))
             | false -> Node (l, x, r,
                 (zplus (max (height l) (height r)) (POS XH))))
  
  (** val add_tree : elt -> tree -> tree sig0 **)
  
  let rec add_tree x = function
    | Leaf -> Node (Leaf, x, Leaf, (POS XH))
    | Node (t0, t1, t2, z0) ->
        (match X.compare x t1 with
           | Lt -> bal (add_tree x t0) t1 t2
           | Eq -> Node (t0, t1, t2, z0)
           | Gt -> bal t0 t1 (add_tree x t2))
  
  (** val add : elt -> t -> t sig0 **)
  
  let add x s =
    add_tree x s
  
  (** val join : tree -> elt -> tree -> tree sig0 **)
  
  let rec join t0 x r =
    match t0 with
      | Leaf -> add_tree x r
      | Node (t1, t2, t3, z0) ->
          let rec f = function
            | Leaf -> add_tree x (Node (t1, t2, t3, z0))
            | Node (t5, t6, t7, z1) ->
                (match z_gt_le_dec z0 (zplus z1 (POS (XO XH))) with
                   | true ->
                       bal t1 t2 (join t3 x (Node (t5, t6, t7, z1)))
                   | false ->
                       (match z_gt_le_dec z1 (zplus z0 (POS (XO XH))) with
                          | true -> bal (f t5) t6 t7
                          | false ->
                              create (Node (t1, t2, t3, z0)) x (Node
                                (t5, t6, t7, z1))))
          in f r
  
  (** val remove_min : tree -> (tree, elt) prod sig0 **)
  
  let rec remove_min = function
    | Leaf -> assert false (* absurd case *)
    | Node (t1, t2, t3, z0) ->
        (match t1 with
           | Leaf -> Pair (t3, t2)
           | Node (t4, t5, t6, z1) ->
               let Pair (l', m) = remove_min t1 in
               Pair ((bal l' t2 t3), m))
  
  (** val remove_max : tree -> (tree, elt) prod sig0 **)
  
  let rec remove_max = function
    | Leaf -> assert false (* absurd case *)
    | Node (t1, t2, t3, z0) ->
        (match t3 with
           | Leaf -> Pair (t1, t2)
           | Node (t4, t5, t6, z1) ->
               let Pair (r', m) = remove_max t3 in
               Pair ((bal t1 t2 r'), m))
  
  (** val merge : tree -> tree -> tree sig0 **)
  
  let merge s1 s2 =
    match s1 with
      | Leaf -> s2
      | Node (t0, t1, t2, z0) ->
          (match s2 with
             | Leaf -> Node (t0, t1, t2, z0)
             | Node (t3, t4, t5, z1) ->
                 let Pair (s'2, m) = remove_min (Node (t3, t4, t5, z1))
                 in
                 bal (Node (t0, t1, t2, z0)) m s'2)
  
  (** val merge_bis : tree -> tree -> tree sig0 **)
  
  let merge_bis s1 s2 =
    match s1 with
      | Leaf -> s2
      | Node (t0, t1, t2, z0) ->
          (match s2 with
             | Leaf -> Node (t0, t1, t2, z0)
             | Node (t3, t4, t5, z1) ->
                 (match z_ge_lt_dec z0 z1 with
                    | true ->
                        let Pair (s'1, m) =
                          remove_max (Node (t0, t1, t2, z0))
                        in
                        create s'1 m (Node (t3, t4, t5, z1))
                    | false ->
                        let Pair (s'2, m) =
                          remove_min (Node (t3, t4, t5, z1))
                        in
                        create (Node (t0, t1, t2, z0)) m s'2))
  
  (** val remove_tree : elt -> tree -> tree sig0 **)
  
  let rec remove_tree x = function
    | Leaf -> Leaf
    | Node (t0, t1, t2, z0) ->
        (match X.compare x t1 with
           | Lt -> bal (remove_tree x t0) t1 t2
           | Eq -> merge t0 t2
           | Gt -> bal t0 t1 (remove_tree x t2))
  
  (** val remove : elt -> t -> t sig0 **)
  
  let remove x s =
    remove_tree x s
  
  (** val min_elt : t -> elt sig0 option **)
  
  let rec min_elt = function
    | Leaf -> None
    | Node (t1, t2, t3, z0) ->
        (match t1 with
           | Leaf -> Some t2
           | Node (t4, t5, t6, z1) ->
               (match min_elt t1 with
                  | Some s -> Some s
                  | None -> None))
  
  (** val max_elt : t -> elt sig0 option **)
  
  let rec max_elt = function
    | Leaf -> None
    | Node (t1, t2, t3, z0) ->
        (match t3 with
           | Leaf -> Some t2
           | Node (t4, t5, t6, z1) ->
               (match max_elt t3 with
                  | Some s -> Some s
                  | None -> None))
  
  (** val choose : t -> elt sig0 option **)
  
  let choose = function
    | Leaf -> None
    | Node (t0, t1, t2, z0) -> Some t1
  
  (** val concat : tree -> tree -> tree sig0 **)
  
  let concat s1 s2 =
    match s1 with
      | Leaf -> s2
      | Node (t0, t1, t2, z0) ->
          (match s2 with
             | Leaf -> Node (t0, t1, t2, z0)
             | Node (t3, t4, t5, z1) ->
                 let Pair (s'2, m) = remove_min (Node (t3, t4, t5, z1))
                 in
                 join (Node (t0, t1, t2, z0)) m s'2)
  
  (** val split : elt -> tree -> (tree, (bool, tree) prod) prod sig0 **)
  
  let rec split x = function
    | Leaf -> Pair (Leaf, (Pair (false, Leaf)))
    | Node (t0, t1, t2, z0) ->
        (match X.compare x t1 with
           | Lt ->
               let Pair (ll, p) = split x t0 in
               let Pair (pres, rl) = p in
               Pair (ll, (Pair (pres, (join rl t1 t2))))
           | Eq -> Pair (t0, (Pair (true, t2)))
           | Gt ->
               let Pair (lr, p) = split x t2 in
               let Pair (pres, rr) = p in
               Pair ((join t0 t1 lr), (Pair (pres, rr))))
  
  (** val inter : t -> t -> t sig0 **)
  
  let rec inter t0 s0 =
    match t0 with
      | Leaf -> Leaf
      | Node (t1, t2, t3, z0) ->
          (match s0 with
             | Leaf -> Leaf
             | Node (t4, t5, t6, z1) ->
                 let Pair (l2, p) = split t2 (Node (t4, t5, t6, z1)) in
                 let Pair (b, r2) = p in
                 (match b with
                    | true -> join (inter t1 l2) t2 (inter t3 r2)
                    | false -> concat (inter t1 l2) (inter t3 r2)))
  
  (** val diff : t -> t -> t sig0 **)
  
  let rec diff t0 s0 =
    match t0 with
      | Leaf -> Leaf
      | Node (t1, t2, t3, z0) ->
          (match s0 with
             | Leaf -> Node (t1, t2, t3, z0)
             | Node (t4, t5, t6, z1) ->
                 let Pair (l2, p) = split t2 (Node (t4, t5, t6, z1)) in
                 let Pair (b, r2) = p in
                 (match b with
                    | true -> concat (diff t1 l2) (diff t3 r2)
                    | false -> join (diff t1 l2) t2 (diff t3 r2)))
  
  (** val elements_tree_aux : X.t list -> tree -> X.t list **)
  
  let rec elements_tree_aux acc = function
    | Leaf -> acc
    | Node (l, x, r, z0) ->
        elements_tree_aux (Cons (x, (elements_tree_aux acc r))) l
  
  (** val elements_tree : tree -> X.t list **)
  
  let elements_tree t0 =
    elements_tree_aux Nil t0
  
  (** val elements : t -> elt list sig0 **)
  
  let elements s =
    elements_tree s
  
  (** val cardinal_tree : tree -> nat **)
  
  let rec cardinal_tree = function
    | Leaf -> O
    | Node (l, t0, r, z0) -> S
        (plus (cardinal_tree l) (cardinal_tree r))
  
  (** val cardinal : t -> nat sig0 **)
  
  let cardinal s =
    cardinal_tree s
  
  (** val cardinal_rec2 : (tree -> tree -> (tree -> tree -> __ -> 'a1)
                          -> 'a1) -> tree -> tree -> 'a1 **)
  
  let rec cardinal_rec2 h x x' =
    h x x' (fun y y' _ -> cardinal_rec2 h y y')
  
  (** val union : t -> t -> t sig0 **)
  
  let union s1 s2 =
    cardinal_rec2 (fun x x' h _ _ _ _ ->
      match x with
        | Leaf -> x'
        | Node (t0, t1, t2, z0) ->
            (match x' with
               | Leaf -> Node (t0, t1, t2, z0)
               | Node (t3, t4, t5, z1) ->
                   (match z_ge_lt_dec z0 z1 with
                      | true ->
                          (match z_eq_dec z1 (POS XH) with
                             | true ->
                                 add_tree t4 (Node (t0, t1, t2, z0))
                             | false ->
                                 let Pair (l2, p) =
                                   split t1 (Node (t3, t4, t5, z1))
                                 in
                                 let Pair (b, r2) = p in
                                 join (h t0 l2 __ __ __ __ __) t1
                                   (h t2 r2 __ __ __ __ __))
                      | false ->
                          (match z_eq_dec z0 (POS XH) with
                             | true ->
                                 add_tree t1 (Node (t3, t4, t5, z1))
                             | false ->
                                 let Pair (l1, p) =
                                   split t4 (Node (t0, t1, t2, z0))
                                 in
                                 let Pair (b, r1) = p in
                                 join (h l1 t3 __ __ __ __ __) t4
                                   (h r1 t5 __ __ __ __ __))))) s1 s2
      __ __ __ __
  
  (** val filter_acc : (elt -> bool) -> tree -> tree -> tree sig0 **)
  
  let rec filter_acc pdec s acc =
    match s with
      | Leaf -> acc
      | Node (t0, t1, t2, z0) ->
          (match pdec t1 with
             | true ->
                 filter_acc pdec t2
                   (filter_acc pdec t0 (add_tree t1 acc))
             | false -> filter_acc pdec t2 (filter_acc pdec t0 acc))
  
  (** val filter : (elt -> bool) -> t -> t sig0 **)
  
  let filter pdec s =
    filter_acc pdec s Leaf
  
  (** val partition_acc : (elt -> bool) -> tree -> tree -> tree ->
                          (tree, tree) prod sig0 **)
  
  let rec partition_acc pdec s acct accf =
    match s with
      | Leaf -> Pair (acct, accf)
      | Node (t0, t1, t2, z0) ->
          (match pdec t1 with
             | true ->
                 let Pair (acct'', accf') =
                   partition_acc pdec t0 (add_tree t1 acct) accf
                 in
                 let Pair (s1, s2) = partition_acc pdec t2 acct'' accf'
                 in
                 Pair (s1, s2)
             | false ->
                 let Pair (acct', accf'') =
                   partition_acc pdec t0 acct (add_tree t1 accf)
                 in
                 let Pair (s1, s2) = partition_acc pdec t2 acct' accf''
                 in
                 Pair (s1, s2))
  
  (** val partition : (elt -> bool) -> t -> (t, t) prod sig0 **)
  
  let partition pdec s =
    let Pair (s1, s2) = partition_acc pdec s Leaf Leaf in Pair (s1, s2)
  
  (** val subset : t -> t -> bool **)
  
  let subset s1 s2 =
    cardinal_rec2 (fun x x' h _ _ ->
      match x with
        | Leaf -> true
        | Node (t0, t1, t2, z0) ->
            (match x' with
               | Leaf -> false
               | Node (t3, t4, t5, z1) ->
                   (match X.compare t1 t4 with
                      | Lt ->
                          (match h (Node (t0, t1, Leaf, ZERO)) t3 __ __
                                   __ with
                             | true ->
                                 h t2 (Node (t3, t4, t5, z1)) __ __ __
                             | false -> false)
                      | Eq ->
                          (match h t0 t3 __ __ __ with
                             | true -> h t2 t5 __ __ __
                             | false -> false)
                      | Gt ->
                          (match h (Node (Leaf, t1, t2, ZERO)) t5 __ __
                                   __ with
                             | true ->
                                 h t0 (Node (t3, t4, t5, z1)) __ __ __
                             | false -> false)))) s1 s2 __ __
  
  (** val for_all : (elt -> bool) -> t -> bool **)
  
  let rec for_all pdec = function
    | Leaf -> true
    | Node (t0, t1, t2, z0) ->
        (match pdec t1 with
           | true ->
               (match for_all pdec t0 with
                  | true -> for_all pdec t2
                  | false -> false)
           | false -> false)
  
  (** val exists : (elt -> bool) -> t -> bool **)
  
  let rec exists pdec = function
    | Leaf -> false
    | Node (t0, t1, t2, z0) ->
        (match pdec t1 with
           | true -> true
           | false ->
               (match exists pdec t0 with
                  | true -> true
                  | false -> exists pdec t2))
  
  module L = Raw(E)
  
  (** val fold_tree : (elt -> 'a1 -> 'a1) -> tree -> 'a1 -> 'a1 **)
  
  let rec fold_tree f s x =
    match s with
      | Leaf -> x
      | Node (l, x0, r, z0) -> fold_tree f l (f x0 (fold_tree f r x))
  
  (** val fold_tree' : (elt -> 'a1 -> 'a1) -> tree -> 'a1 -> 'a1 **)
  
  let fold_tree' f s x =
    L.fold f (elements_tree s) x
  
  (** val fold : (elt -> 'a1 -> 'a1) -> t -> 'a1 -> 'a1 sig0 **)
  
  let fold f s i =
    fold_tree f (the_tree s) i
  
  (** val flatten : tree list -> elt list **)
  
  let rec flatten = function
    | Nil -> Nil
    | Cons (t0, r) -> app (elements_tree t0) (flatten r)
  
  (** val measure_t : tree -> z **)
  
  let rec measure_t = function
    | Leaf -> POS XH
    | Node (l, t0, r, z0) ->
        zplus (zplus (POS XH) (zmult (POS (XI XH)) (measure_t l)))
          (measure_t r)
  
  (** val measure_l : tree list -> z **)
  
  let rec measure_l = function
    | Nil -> ZERO
    | Cons (s, l0) -> zplus (measure_t s) (measure_l l0)
  
  (** val compare_rec2 : (tree list -> tree list -> (tree list -> tree
                         list -> __ -> 'a1) -> 'a1) -> tree list ->
                         tree list -> 'a1 **)
  
  let rec compare_rec2 h x x' =
    h x x' (fun y y' _ -> compare_rec2 h y y')
  
  (** val compare_aux : tree list -> tree list -> L.t compare **)
  
  let compare_aux l1 l2 =
    compare_rec2 (fun x x' h _ _ _ ->
      match x with
        | Nil -> (match x' with
                    | Nil -> Eq
                    | Cons (t0, l) -> Lt)
        | Cons (t0, l) ->
            (match x' with
               | Nil -> Gt
               | Cons (t1, l0) ->
                   (match t0 with
                      | Leaf ->
                          (match t1 with
                             | Leaf ->
                                 (match h l l0 __ __ __ __ with
                                    | Lt -> Lt
                                    | Eq -> Eq
                                    | Gt -> Gt)
                             | Node (t2, t3, t4, z0) ->
                                 (match t2 with
                                    | Leaf ->
                                        (match h l (Cons ((Node (Leaf,
                                                 t3, t4, z0)), l0)) __
                                                 __ __ __ with
                                           | Lt -> Lt
                                           | Eq -> Eq
                                           | Gt -> Gt)
                                    | Node (t5, t6, t7, z1) ->
                                        (match h (Cons (Leaf, l)) (Cons
                                                 ((Node (t5, t6, t7,
                                                 z1)), (Cons ((Node
                                                 (Leaf, t3, t4, z0)),
                                                 l0)))) __ __ __ __ with
                                           | Lt -> Lt
                                           | Eq -> Eq
                                           | Gt -> Gt)))
                      | Node (t2, t3, t4, z0) ->
                          (match t1 with
                             | Leaf ->
                                 (match t2 with
                                    | Leaf ->
                                        (match h (Cons ((Node (Leaf,
                                                 t3, t4, z0)), l)) l0
                                                 __ __ __ __ with
                                           | Lt -> Lt
                                           | Eq -> Eq
                                           | Gt -> Gt)
                                    | Node (t5, t6, t7, z1) ->
                                        (match h (Cons ((Node (t5, t6,
                                                 t7, z1)), (Cons ((Node
                                                 (Leaf, t3, t4, z0)),
                                                 l)))) (Cons (Leaf,
                                                 l0)) __ __ __ __ with
                                           | Lt -> Lt
                                           | Eq -> Eq
                                           | Gt -> Gt))
                             | Node (t5, t6, t7, z1) ->
                                 (match t2 with
                                    | Leaf ->
                                        (match t5 with
                                           | Leaf ->
                                               (match X.compare t3 t6 with
                                                  | Lt -> Lt
                                                  | Eq ->
                                                      (match h (Cons
                                                              (t4, l))
                                                              (Cons
                                                              (t7, l0))
                                                              __ __ __
                                                              __ with
                                                         | Lt -> Lt
                                                         | Eq -> Eq
                                                         | Gt -> Gt)
                                                  | Gt -> Gt)
                                           | Node (t8, t9, t10, z2) ->
                                               (match h (Cons ((Node
                                                        (Leaf, t3, t4,
                                                        z0)), l)) (Cons
                                                        ((Node (t8, t9,
                                                        t10, z2)),
                                                        (Cons ((Node
                                                        (Leaf, t6, t7,
                                                        z1)), l0)))) __
                                                        __ __ __ with
                                                  | Lt -> Lt
                                                  | Eq -> Eq
                                                  | Gt -> Gt))
                                    | Node (t8, t9, t10, z2) ->
                                        (match t5 with
                                           | Leaf ->
                                               (match h (Cons ((Node
                                                        (t8, t9, t10,
                                                        z2)), (Cons
                                                        ((Node (Leaf,
                                                        t3, t4, z0)),
                                                        l)))) (Cons
                                                        ((Node (Leaf,
                                                        t6, t7, z1)),
                                                        l0)) __ __ __
                                                        __ with
                                                  | Lt -> Lt
                                                  | Eq -> Eq
                                                  | Gt -> Gt)
                                           | Node (t11, t12, t13, z3) ->
                                               (match h (Cons ((Node
                                                        (t8, t9, t10,
                                                        z2)), (Cons
                                                        ((Node (Leaf,
                                                        t3, t4, z0)),
                                                        l)))) (Cons
                                                        ((Node ((Node
                                                        (t11, t12, t13,
                                                        z3)), t6, t7,
                                                        z1)), l0)) __
                                                        __ __ __ with
                                                  | Lt -> Lt
                                                  | Eq -> Eq
                                                  | Gt -> Gt))))))) l1
      l2 __ __ __
  
  (** val compare : t -> t -> t compare **)
  
  let compare s1 s2 =
    match compare_aux (Cons (s1, Nil)) (Cons (s2, Nil)) with
      | Lt -> Lt
      | Eq -> Eq
      | Gt -> Gt
  
  (** val equal : t -> t -> bool **)
  
  let equal s s' =
    match compare s s' with
      | Lt -> false
      | Eq -> true
      | Gt -> false
 end

module Nat = 
 struct 
  type t = nat
  
  (** val compare : t -> t -> nat compare **)
  
  let compare x y =
    match lt_eq_lt_dec x y with
      | Some s -> (match s with
                     | true -> Lt
                     | false -> Eq)
      | None -> Gt
 end

module NatAVL = Make(Nat)