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

type nat =
  | O
  | S of nat

type ('a, 'b) sum =
  | Inl of 'a
  | Inr of 'b

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

(** val fst : ('a1, 'a2) prod -> 'a1 **)

let fst = function
  | Pair (x, y) -> x

(** val snd : ('a1, 'a2) prod -> 'a2 **)

let snd = function
  | Pair (x, y) -> y

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

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

type 'x compare =
  | Lt
  | Eq
  | Gt

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

module type S = 
 sig 
  module E : 
   OrderedType
  
  type elt = E.t
  
  type t 
  
  val empty : t
  
  val is_empty : t -> bool
  
  val mem : elt -> t -> bool
  
  val add : elt -> t -> t
  
  val singleton : elt -> t
  
  val remove : elt -> t -> t
  
  val union : t -> t -> t
  
  val inter : t -> t -> t
  
  val diff : t -> t -> t
  
  val compare : t -> t -> t compare
  
  val equal : t -> t -> bool
  
  val subset : t -> t -> bool
  
  val fold : (elt -> 'a1 -> 'a1) -> t -> 'a1 -> 'a1
  
  val for_all : (elt -> bool) -> t -> bool
  
  val exists : (elt -> bool) -> t -> bool
  
  val filter : (elt -> bool) -> t -> t
  
  val partition : (elt -> bool) -> t -> (t, t) prod
  
  val cardinal : t -> nat
  
  val elements : t -> elt list
  
  val min_elt : t -> elt option
  
  val max_elt : t -> elt option
  
  val choose : t -> elt option
 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

module DepOfNodep = 
 functor (M:S) ->
 struct 
  module ME = MoreOrderedType(M.E)
  
  (** val empty : M.t sig0 **)
  
  let empty =
    M.empty
  
  (** val is_empty : M.t -> bool **)
  
  let is_empty s =
    match M.is_empty s with
      | true -> true
      | false -> false
  
  (** val mem : M.elt -> M.t -> bool **)
  
  let mem x s =
    match M.mem x s with
      | true -> true
      | false -> false
  
  (** val add : M.elt -> M.t -> M.t sig0 **)
  
  let add x s =
    M.add x s
  
  (** val singleton : M.elt -> M.t sig0 **)
  
  let singleton x =
    M.singleton x
  
  (** val remove : M.elt -> M.t -> M.t sig0 **)
  
  let remove x s =
    M.remove x s
  
  (** val union : M.t -> M.t -> M.t sig0 **)
  
  let union s s' =
    M.union s s'
  
  (** val inter : M.t -> M.t -> M.t sig0 **)
  
  let inter s s' =
    M.inter s s'
  
  (** val diff : M.t -> M.t -> M.t sig0 **)
  
  let diff s s' =
    M.diff s s'
  
  (** val equal : M.t -> M.t -> bool **)
  
  let equal s s' =
    match M.equal s s' with
      | true -> true
      | false -> false
  
  (** val subset : M.t -> M.t -> bool **)
  
  let subset s s' =
    match M.subset s s' with
      | true -> true
      | false -> false
  
  (** val fold : (M.elt -> 'a1 -> 'a1) -> M.t -> 'a1 -> 'a1 sig0 **)
  
  let fold f s i =
    M.fold f s i
  
  (** val cardinal : M.t -> nat sig0 **)
  
  let cardinal s =
    M.cardinal s
  
  (** val fdec : (M.elt -> bool) -> M.elt -> bool **)
  
  let fdec pdec x =
    match pdec x with
      | true -> true
      | false -> false
  
  (** val filter : (M.elt -> bool) -> M.t -> M.t sig0 **)
  
  let filter pdec s =
    M.filter (fun x ->
      match pdec x with
        | true -> true
        | false -> false) s
  
  (** val for_all : (M.elt -> bool) -> M.t -> bool **)
  
  let for_all pdec s =
    match M.for_all (fun x ->
            match pdec x with
              | true -> true
              | false -> false) s with
      | true -> true
      | false -> false
  
  (** val exists : (M.elt -> bool) -> M.t -> bool **)
  
  let exists pdec s =
    match M.exists (fun x ->
            match pdec x with
              | true -> true
              | false -> false) s with
      | true -> true
      | false -> false
  
  (** val partition : (M.elt -> bool) -> M.t -> (M.t, M.t) prod sig0 **)
  
  let partition pdec s =
    M.partition (fun x ->
      match pdec x with
        | true -> true
        | false -> false) s
  
  (** val choose : M.t -> M.elt sig0 option **)
  
  let choose s =
    match M.choose s with
      | Some e -> Some e
      | None -> None
  
  (** val elements : M.t -> M.elt list sig0 **)
  
  let elements s =
    M.elements s
  
  (** val min_elt : M.t -> M.elt sig0 option **)
  
  let min_elt s =
    match M.min_elt s with
      | Some e -> Some e
      | None -> None
  
  (** val max_elt : M.t -> M.elt sig0 option **)
  
  let max_elt s =
    match M.max_elt s with
      | Some e -> Some e
      | None -> None
  
  module E = M.E
  
  type elt = M.elt
  
  type t = M.t
  
  (** val compare : M.t -> M.t -> M.t compare **)
  
  let compare s s' =
    M.compare s s'
 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 add0 : positive -> positive -> positive **)

let rec add0 x y =
  match x with
    | XI x' ->
        (match y with
           | XI y' -> XO (add_carry x' y')
           | XO y' -> XI (add0 x' y')
           | XH -> XO (add_un x'))
    | XO x' ->
        (match y with
           | XI y' -> XI (add0 x' y')
           | XO y' -> XO (add0 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 (add0 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 (add0 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 (add0 x' y'))

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

let zopp = function
  | ZERO -> ZERO
  | POS x0 -> NEG x0
  | NEG x0 -> POS x0

(** 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 zs : z -> z **)

let zs x =
  zplus x (POS XH)

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

let zpred x =
  zplus x (NEG XH)

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

let zminus m n =
  zplus m (zopp n)

(** 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 zeven_odd_dec : z -> bool **)

let zeven_odd_dec = function
  | ZERO -> true
  | POS p ->
      (match p with
         | XI p0 -> false
         | XO p0 -> true
         | XH -> false)
  | NEG p ->
      (match p with
         | XI p0 -> false
         | XO p0 -> true
         | XH -> false)

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

let zdiv2_pos = function
  | XI p -> p
  | XO p -> p
  | XH -> XH

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

let zdiv2 = function
  | ZERO -> ZERO
  | POS p ->
      (match p with
         | XI p0 -> POS (zdiv2_pos p)
         | XO p0 -> POS (zdiv2_pos p)
         | XH -> ZERO)
  | NEG p ->
      (match p with
         | XI p0 -> NEG (zdiv2_pos p)
         | XO p0 -> NEG (zdiv2_pos p)
         | XH -> ZERO)

(** val z_modulo_2 : z -> (z sig0, z sig0) sum **)

let z_modulo_2 x =
  match zeven_odd_dec x with
    | true -> Inl (zdiv2 x)
    | false -> Inr
        (match x with
           | ZERO -> assert false (* absurd case *)
           | POS p -> zdiv2 (POS p)
           | NEG p -> zdiv2 (zpred (NEG p)))

(** val zsplit2 : z -> (z, z) prod sig0 **)

let zsplit2 x =
  match z_modulo_2 x with
    | Inl x0 -> Pair (x0, x0)
    | Inr x0 -> Pair (x0, (zplus x0 (POS XH)))

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 Raw = Raw(X)
  
  type slist =
    Raw.t
    (* singleton inductive, whose constructor was Build_slist *)
  
  (** val slist_rect : (Raw.t -> __ -> 'a1) -> slist -> 'a1 **)
  
  let slist_rect f s =
    f s __
  
  (** val slist_rec : (Raw.t -> __ -> 'a1) -> slist -> 'a1 **)
  
  let slist_rec f s =
    f s __
  
  (** val this : slist -> Raw.t **)
  
  let this s =
    s
  
  type t = slist
  
  type elt = X.t
  
  (** val mem : elt -> t -> bool **)
  
  let mem x s =
    Raw.mem x (this s)
  
  (** val add : Raw.elt -> slist -> slist **)
  
  let add x s =
    Raw.add x (this s)
  
  (** val remove : Raw.elt -> slist -> slist **)
  
  let remove x s =
    Raw.remove x (this s)
  
  (** val singleton : Raw.elt -> slist **)
  
  let singleton x =
    Raw.singleton x
  
  (** val union : t -> t -> slist **)
  
  let union s s' =
    Raw.union (this s) (this s')
  
  (** val inter : t -> t -> slist **)
  
  let inter s s' =
    Raw.inter (this s) (this s')
  
  (** val diff : t -> t -> slist **)
  
  let diff s s' =
    Raw.diff (this s) (this s')
  
  (** val equal : t -> t -> bool **)
  
  let equal s s' =
    Raw.equal (this s) (this s')
  
  (** val subset : t -> t -> bool **)
  
  let subset s s' =
    Raw.subset (this s) (this s')
  
  (** val empty : slist **)
  
  let empty =
    Raw.empty
  
  (** val is_empty : t -> bool **)
  
  let is_empty s =
    Raw.is_empty (this s)
  
  (** val elements : t -> Raw.elt list **)
  
  let elements s =
    Raw.elements (this s)
  
  (** val min_elt : t -> Raw.elt option **)
  
  let min_elt s =
    Raw.min_elt (this s)
  
  (** val max_elt : t -> Raw.elt option **)
  
  let max_elt s =
    Raw.max_elt (this s)
  
  (** val choose : t -> Raw.elt option **)
  
  let choose s =
    min_elt s
  
  (** val fold : (elt -> 'a1 -> 'a1) -> t -> 'a1 -> 'a1 **)
  
  let fold f s x =
    Raw.fold f (this s) x
  
  (** val cardinal : t -> nat **)
  
  let cardinal s =
    Raw.cardinal (this s)
  
  (** val filter : (elt -> bool) -> t -> slist **)
  
  let filter f s =
    Raw.filter f (this s)
  
  (** val for_all : (elt -> bool) -> t -> bool **)
  
  let for_all f s =
    Raw.for_all f (this s)
  
  (** val exists : (elt -> bool) -> t -> bool **)
  
  let exists f s =
    Raw.exists f (this s)
  
  (** val partition : (elt -> bool) -> t -> (slist, slist) prod **)
  
  let partition f s =
    let p = Raw.partition f (this s) in Pair ((fst p), (snd p))
  
  (** val compare : t -> t -> t compare **)
  
  let compare s s' =
    match Raw.compare (this s) (this s') with
      | Lt -> Lt
      | Eq -> Eq
      | Gt -> Gt
 end

(** val zlength_aux : z -> 'a1 list -> z **)

let rec zlength_aux acc = function
  | Nil -> acc
  | Cons (a, l0) -> zlength_aux (zs acc) l0

(** val zlength : 'a1 list -> z **)

let zlength l =
  zlength_aux ZERO l

(** val log_inf : positive -> z **)

let rec log_inf = function
  | XI q -> zs (log_inf q)
  | XO q -> zs (log_inf q)
  | XH -> ZERO

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

let n_digits = function
  | ZERO -> ZERO
  | POS p -> log_inf p
  | NEG p -> log_inf p

module Coq_Make = 
 functor (X:OrderedType) ->
 struct 
  module E = X
  
  module ME = MoreOrderedType(X)
  
  type elt = X.t
  
  type color =
    | Coq_red
    | Coq_black
  
  (** val color_rect : 'a1 -> 'a1 -> color -> 'a1 **)
  
  let color_rect f f0 = function
    | Coq_red -> f
    | Coq_black -> f0
  
  (** val color_rec : 'a1 -> 'a1 -> color -> 'a1 **)
  
  let color_rec f f0 = function
    | Coq_red -> f
    | Coq_black -> f0
  
  type tree =
    | Leaf
    | Node of color * tree * X.t * tree
  
  (** val tree_rect : 'a1 -> (color -> tree -> 'a1 -> X.t -> tree ->
                      'a1 -> 'a1) -> tree -> 'a1 **)
  
  let rec tree_rect f f0 = function
    | Leaf -> f
    | Node (c, t1, t2, t3) ->
        f0 c t1 (tree_rect f f0 t1) t2 t3 (tree_rect f f0 t3)
  
  (** val tree_rec : 'a1 -> (color -> tree -> 'a1 -> X.t -> tree -> 'a1
                     -> 'a1) -> tree -> 'a1 **)
  
  let rec tree_rec f f0 = function
    | Leaf -> f
    | Node (c, t1, t2, t3) ->
        f0 c t1 (tree_rec f f0 t1) t2 t3 (tree_rec f f0 t3)
  
  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 (c, t0, t1, t2) -> false
  
  (** val mem : elt -> t -> bool **)
  
  let rec mem x = function
    | Leaf -> false
    | Node (c, t0, t1, t2) ->
        (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 (Coq_red, Leaf, x, Leaf)
  
  (** val singleton : elt -> t sig0 **)
  
  let singleton x =
    singleton_tree x
  
  type coq_Conflict =
    | NoConflict
    | RedRedConflict of tree * tree * tree * elt * elt
  
  (** val coq_Conflict_rect : tree -> (__ -> 'a1) -> (tree -> tree ->
                              tree -> elt -> elt -> __ -> __ -> __ ->
                              __ -> __ -> __ -> __ -> __ -> __ -> __ ->
                              'a1) -> coq_Conflict -> 'a1 **)
  
  let coq_Conflict_rect s f f0 = function
    | NoConflict -> f __
    | RedRedConflict (x, x0, x1, x2, x3) ->
        f0 x x0 x1 x2 x3 __ __ __ __ __ __ __ __ __ __
  
  (** val coq_Conflict_rec : tree -> (__ -> 'a1) -> (tree -> tree ->
                             tree -> elt -> elt -> __ -> __ -> __ -> __
                             -> __ -> __ -> __ -> __ -> __ -> __ ->
                             'a1) -> coq_Conflict -> 'a1 **)
  
  let coq_Conflict_rec s f f0 = function
    | NoConflict -> f __
    | RedRedConflict (x, x0, x1, x2, x3) ->
        f0 x x0 x1 x2 x3 __ __ __ __ __ __ __ __ __ __
  
  (** val conflict : tree -> coq_Conflict **)
  
  let conflict = function
    | Leaf -> NoConflict
    | Node (c, t0, t1, t2) ->
        (match c with
           | Coq_red ->
               (match t0 with
                  | Leaf ->
                      (match t2 with
                         | Leaf -> NoConflict
                         | Node (c0, t3, t4, t5) ->
                             (match c0 with
                                | Coq_red -> RedRedConflict (Leaf, t3,
                                    t5, t1, t4)
                                | Coq_black -> NoConflict))
                  | Node (c0, t3, t4, t5) ->
                      (match c0 with
                         | Coq_red -> RedRedConflict (t3, t5, t2, t4,
                             t1)
                         | Coq_black ->
                             (match t2 with
                                | Leaf -> NoConflict
                                | Node (c1, t6, t7, t8) ->
                                    (match c1 with
                                       | Coq_red -> RedRedConflict
                                           ((Node (Coq_black, t3, t4,
                                           t5)), t6, t8, t1, t7)
                                       | Coq_black -> NoConflict))))
           | Coq_black -> NoConflict)
  
  (** val lbalance : tree -> elt -> tree -> tree sig0 **)
  
  let lbalance l x r =
    match conflict l with
      | NoConflict -> Node (Coq_black, l, x, r)
      | RedRedConflict (a, b, c, x0, y) -> Node (Coq_red, (Node
          (Coq_black, a, x0, b)), y, (Node (Coq_black, c, x, r)))
  
  (** val rbalance : tree -> elt -> tree -> tree sig0 **)
  
  let rbalance l x r =
    match conflict r with
      | NoConflict -> Node (Coq_black, l, x, r)
      | RedRedConflict (a, b, c, x0, y) -> Node (Coq_red, (Node
          (Coq_black, l, x, a)), x0, (Node (Coq_black, b, y, c)))
  
  (** val insert : elt -> t -> tree sig0 **)
  
  let rec insert x = function
    | Leaf -> singleton_tree x
    | Node (c, t0, t1, t2) ->
        (match c with
           | Coq_red ->
               (match X.compare x t1 with
                  | Lt -> Node (Coq_red, (insert x t0), t1, t2)
                  | Eq -> Node (Coq_red, t0, t1, t2)
                  | Gt -> Node (Coq_red, t0, t1, (insert x t2)))
           | Coq_black ->
               (match X.compare x t1 with
                  | Lt -> lbalance (insert x t0) t1 t2
                  | Eq -> Node (Coq_black, t0, t1, t2)
                  | Gt -> rbalance t0 t1 (insert x t2)))
  
  (** val add : elt -> t -> t sig0 **)
  
  let add x s =
    match insert x s with
      | Leaf -> assert false (* absurd case *)
      | Node (c, t0, t1, t2) -> Node (Coq_black, t0, t1, t2)
  
  (** val unbalanced_left : tree -> (tree, bool) prod sig0 **)
  
  let unbalanced_left = function
    | Leaf -> Pair (Leaf, false)
    | Node (c, x, x0, x1) ->
        (match c with
           | Coq_red ->
               (match x with
                  | Leaf -> Pair ((Node (Coq_black, Leaf, x0, x1)),
                      false)
                  | Node (c0, x2, x3, x4) ->
                      (match c0 with
                         | Coq_red -> Pair ((Node (Coq_black, (Node
                             (Coq_red, x2, x3, x4)), x0, x1)), false)
                         | Coq_black -> Pair
                             ((lbalance (Node (Coq_red, x2, x3, x4)) x0
                                x1), false)))
           | Coq_black ->
               (match x with
                  | Leaf -> Pair ((Node (Coq_black, Leaf, x0, x1)),
                      false)
                  | Node (c0, x2, x3, x4) ->
                      (match c0 with
                         | Coq_red ->
                             (match x4 with
                                | Leaf -> Pair ((Node (Coq_black, (Node
                                    (Coq_red, x2, x3, Leaf)), x0, x1)),
                                    false)
                                | Node (c1, x5, x6, x7) ->
                                    (match c1 with
                                       | Coq_red -> Pair ((Node
                                           (Coq_black, (Node (Coq_red,
                                           x2, x3, (Node (Coq_red, x5,
                                           x6, x7)))), x0, x1)), false)
                                       | Coq_black -> Pair ((Node
                                           (Coq_black, x2, x3,
                                           (lbalance (Node (Coq_red,
                                             x5, x6, x7)) x0 x1))),
                                           false)))
                         | Coq_black -> Pair
                             ((lbalance (Node (Coq_red, x2, x3, x4)) x0
                                x1), true))))
  
  (** val unbalanced_right : tree -> (tree, bool) prod sig0 **)
  
  let unbalanced_right = function
    | Leaf -> Pair (Leaf, false)
    | Node (c, x, x0, x1) ->
        (match c with
           | Coq_red ->
               (match x1 with
                  | Leaf -> Pair ((Node (Coq_black, x, x0, Leaf)),
                      false)
                  | Node (c0, x2, x3, x4) ->
                      (match c0 with
                         | Coq_red -> Pair ((Node (Coq_black, x, x0,
                             (Node (Coq_red, x2, x3, x4)))), false)
                         | Coq_black -> Pair
                             ((rbalance x x0 (Node (Coq_red, x2, x3,
                                x4))), false)))
           | Coq_black ->
               (match x1 with
                  | Leaf -> Pair ((Node (Coq_black, x, x0, Leaf)),
                      false)
                  | Node (c0, x2, x3, x4) ->
                      (match c0 with
                         | Coq_red ->
                             (match x2 with
                                | Leaf -> Pair ((Node (Coq_black, x,
                                    x0, (Node (Coq_red, Leaf, x3,
                                    x4)))), false)
                                | Node (c1, x5, x6, x7) ->
                                    (match c1 with
                                       | Coq_red -> Pair ((Node
                                           (Coq_black, x, x0, (Node
                                           (Coq_red, (Node (Coq_red,
                                           x5, x6, x7)), x3, x4)))),
                                           false)
                                       | Coq_black -> Pair ((Node
                                           (Coq_black,
                                           (rbalance x x0 (Node
                                             (Coq_red, x5, x6, x7))),
                                           x3, x4)), false)))
                         | Coq_black -> Pair
                             ((rbalance x x0 (Node (Coq_red, x2, x3,
                                x4))), true))))
  
  (** val remove_min : tree -> (tree, (elt, bool) prod) prod sig0 **)
  
  let rec remove_min = function
    | Leaf -> assert false (* absurd case *)
    | Node (c, t1, t2, t3) ->
        (match t1 with
           | Leaf ->
               (match c with
                  | Coq_red -> Pair (t3, (Pair (t2, false)))
                  | Coq_black ->
                      (match t3 with
                         | Leaf -> Pair (Leaf, (Pair (t2, true)))
                         | Node (c0, t4, t5, t6) -> Pair ((Node
                             (Coq_black, t4, t5, t6)), (Pair (t2,
                             false)))))
           | Node (c0, t4, t5, t6) ->
               let Pair (l', p) = remove_min t1 in
               let Pair (m, d) = p in
               (match d with
                  | true ->
                      let Pair (t', d') =
                        unbalanced_right (Node (c, l', t2, t3))
                      in
                      Pair (t', (Pair (m, d')))
                  | false -> Pair ((Node (c, l', t2, t3)), (Pair (m,
                      false)))))
  
  (** val blackify : tree -> (tree, bool) prod sig0 **)
  
  let blackify = function
    | Leaf -> Pair (Leaf, true)
    | Node (c, t0, t1, t2) ->
        (match c with
           | Coq_red -> Pair ((Node (Coq_black, t0, t1, t2)), false)
           | Coq_black -> Pair ((Node (Coq_black, t0, t1, t2)), true))
  
  (** val remove_aux : elt -> tree -> (tree, bool) prod sig0 **)
  
  let rec remove_aux x = function
    | Leaf -> Pair (Leaf, false)
    | Node (c, t0, t1, t2) ->
        (match X.compare x t1 with
           | Lt ->
               let Pair (l', d) = remove_aux x t0 in
               (match d with
                  | true ->
                      let Pair (s', d') =
                        unbalanced_right (Node (c, l', t1, t2))
                      in
                      Pair (s', d')
                  | false -> Pair ((Node (c, l', t1, t2)), false))
           | Eq ->
               (match t2 with
                  | Leaf ->
                      (match c with
                         | Coq_red -> Pair (t0, false)
                         | Coq_black ->
                             let Pair (s', d) = blackify t0 in
                             Pair (s', d))
                  | Node (c0, t3, t4, t5) ->
                      let Pair (r', p) =
                        remove_min (Node (c0, t3, t4, t5))
                      in
                      let Pair (m, d) = p in
                      (match d with
                         | true ->
                             let Pair (s', d0) =
                               unbalanced_left (Node (c, t0, m, r'))
                             in
                             Pair (s', d0)
                         | false -> Pair ((Node (c, t0, m, r')), false)))
           | Gt ->
               let Pair (r', d) = remove_aux x t2 in
               (match d with
                  | true ->
                      let Pair (s', d') =
                        unbalanced_left (Node (c, t0, t1, r'))
                      in
                      Pair (s', d')
                  | false -> Pair ((Node (c, t0, t1, r')), false)))
  
  (** val remove : elt -> t -> t sig0 **)
  
  let remove x s =
    let Pair (s', b) = remove_aux x s in s'
  
  (** val of_list_aux_Invariant_rect : z -> z -> elt list -> elt list
                                       -> tree -> (__ -> __ -> __ -> __
                                       -> __ -> __ -> 'a1) -> 'a1 **)
  
  let of_list_aux_Invariant_rect k n l l' r f =
    f __ __ __ __ __ __
  
  (** val of_list_aux_Invariant_rec : z -> z -> elt list -> elt list ->
                                      tree -> (__ -> __ -> __ -> __ ->
                                      __ -> __ -> 'a1) -> 'a1 **)
  
  let of_list_aux_Invariant_rec k n l l' r f =
    f __ __ __ __ __ __
  
  (** val of_list_aux : z -> z -> elt list -> (tree, elt list) prod
                        sig0 **)
  
  let rec of_list_aux x n l =
    match x with
      | ZERO ->
          (match z_eq_dec ZERO n with
             | true -> Pair (Leaf, l)
             | false ->
                 (match l with
                    | Nil -> assert false (* absurd case *)
                    | Cons (x0, l') -> Pair ((Node (Coq_red, Leaf, x0,
                        Leaf)), l')))
      | POS p ->
          let Pair (n1, n2) = zsplit2 (zminus n (POS XH)) in
          let Pair (lft, l') = of_list_aux (zpred (POS p)) n1 l in
          (match l' with
             | Nil -> assert false (* absurd case *)
             | Cons (x0, l'') ->
                 let Pair (rht, l''') =
                   of_list_aux (zpred (POS p)) n2 l''
                 in
                 Pair ((Node (Coq_black, lft, x0, rht)), l'''))
      | NEG p -> assert false (* absurd case *)
  
  (** val of_list : elt list -> t sig0 **)
  
  let of_list l =
    let n = zlength l in
    let Pair (r, l') = of_list_aux (n_digits n) n l in r
  
  (** val elements_tree_aux : X.t list -> tree -> X.t list **)
  
  let rec elements_tree_aux acc = function
    | Leaf -> acc
    | Node (c, l, x, r) ->
        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
  
  module Lists = Make(X)
  
  (** val of_slist : Lists.t -> t sig0 **)
  
  let of_slist l =
    of_list l
  
  (** val to_slist : t -> Lists.t sig0 **)
  
  let to_slist s =
    elements s
  
  (** val union : t -> t -> t sig0 **)
  
  let union s s' =
    of_slist (Lists.union (to_slist s) (to_slist s'))
  
  (** val inter : t -> t -> t sig0 **)
  
  let inter s s' =
    of_slist (Lists.inter (to_slist s) (to_slist s'))
  
  (** val diff : t -> t -> t sig0 **)
  
  let diff s s' =
    of_slist (Lists.diff (to_slist s) (to_slist s'))
  
  (** val equal : t -> t -> bool **)
  
  let equal s s' =
    match Lists.equal (to_slist s) (to_slist s') with
      | true -> true
      | false -> false
  
  (** val subset : t -> t -> bool **)
  
  let subset s s' =
    match Lists.subset (to_slist s) (to_slist s') with
      | true -> true
      | false -> false
  
  (** val fold_tree : (elt -> 'a1 -> 'a1) -> tree -> 'a1 -> 'a1 **)
  
  let rec fold_tree f s x =
    match s with
      | Leaf -> x
      | Node (c, l, x0, r) -> 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 =
    Lists.Raw.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 cardinal : t -> nat sig0 **)
  
  let cardinal s =
    fold (fun x x0 -> S x0) s O
  
  module DLists = DepOfNodep(Lists)
  
  (** val filter : (elt -> bool) -> t -> t sig0 **)
  
  let filter pdec s =
    of_slist (DLists.filter pdec (to_slist s))
  
  (** val for_all : (elt -> bool) -> t -> bool **)
  
  let for_all pdec s =
    DLists.for_all pdec (to_slist s)
  
  (** val exists : (elt -> bool) -> t -> bool **)
  
  let exists pdec s =
    DLists.exists pdec (to_slist s)
  
  (** val partition : (elt -> bool) -> t -> (t, t) prod sig0 **)
  
  let partition pdec s =
    let Pair (l1, l2) = DLists.partition pdec (to_slist s) in
    Pair ((of_slist l1), (of_slist l2))
  
  (** val min_elt : t -> elt sig0 option **)
  
  let rec min_elt = function
    | Leaf -> None
    | Node (c, t1, t2, t3) ->
        (match t1 with
           | Leaf -> Some t2
           | Node (c0, t4, t5, t6) ->
               (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 (c, t1, t2, t3) ->
        (match t3 with
           | Leaf -> Some t2
           | Node (c0, t4, t5, t6) ->
               (match max_elt t3 with
                  | Some s -> Some s
                  | None -> None))
  
  (** val choose : t -> elt sig0 option **)
  
  let choose = function
    | Leaf -> None
    | Node (c, t0, t1, t2) -> Some t1
  
  (** val compare : t -> t -> t compare **)
  
  let compare s s' =
    match Lists.compare (to_slist s) (to_slist s') with
      | Lt -> Lt
      | Eq -> Eq
      | Gt -> Gt
 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 NatRBT = Coq_Make(Nat)