type elt = Elt


let compare = fun (x y : elt) => 0


type bool = True
       | False


type t = Empty
       | Node of t * elt * t * int


let rec invalid_arg : forall 'a. 'a = invalid_arg


let height = fun (t : t) => match t with
                 | Empty => 0
                 | Node(_,_,_,h) => h
               end


let create =
      fun (l : t) (v : elt) (r : t) =>
        let hl = height l in
        let hr = height r in
        Node(l,v,r,
        (match gte hl hr with
           | True => plus hl 1
           | False => plus hr 1
         end))


let bal =
      fun (l : t) (v : elt) (r : t) =>
        let hl = height l in
        let hr = height r in
        match gt hl (plus hr 2) with
          | True =>
            match l with
              | Empty => invalid_arg [t]
              | Node(ll,lv,lr,_) =>
                match gte (height ll) (height lr) with
                  | True => create ll lv (create lr v r)
                  | False =>
                    match lr with
                      | Empty => invalid_arg [t]
                      | Node(lrl,lrv,lrr,_) => create (create ll lv lrl) lrv
                        (create lrr v r)
                    end
                end
            end
          | False =>
            match gt hr (plus hl 2) with
              | True =>
                match r with
                  | Empty => invalid_arg [t]
                  | Node(rl,rv,rr,_) =>
                    match gte (height rr) (height rl) with
                      | True => create (create l v rl) rv rr
                      | False =>
                        match rl with
                          | Empty => invalid_arg [t]
                          | Node(rll,rlv,rlr,_) => create (create l v rll)
                            rlv (create rlr rv rr)
                        end
                    end
                end
              | False => Node(l,v,r,
                (match gte hl hr with
                   | True => plus hl 1
                   | False => plus hr 1
                 end))
            end
        end


let rec add : elt -> t -> t =
          fun (x : elt) (s : t) =>
            match s with
              | Empty => Node(Empty,x,Empty,1)
              | Node(l,v,r,h) =>
                let c = compare x v in
                match eq c 0 with
                  | True => Node(l,v,r,h)
                  | False =>
                    match lt c 0 with
                      | True => bal (add x l) v r
                      | False => bal l v (add x r)
                    end
                end
            end


let singleton = fun (x : elt) => Node(Empty,x,Empty,1)


let rec add_min_element : elt -> t -> t =
          fun (v : elt) (s : t) =>
            match s with
              | Empty => singleton v
              | Node(l,x,r,_) => bal (add_min_element v l) x r
            end


let rec add_max_element : elt -> t -> t =
          fun (v : elt) (s : t) =>
            match s with
              | Empty => singleton v
              | Node(l,x,r,_) => bal l x (add_max_element v r)
            end


let rec join : t -> elt -> t -> t =
          fun (l : t) (v : elt) (r : t) =>
            match l with
              | Empty => add_min_element v r
              | Node(ll,lv,lr,lh) =>
                match r with
                  | Empty => add_max_element v l
                  | Node(rl,rv,rr,rh) =>
                    match gt lh (plus rh 2) with
                      | True => bal ll lv (join lr v r)
                      | False =>
                        match gt rh (plus lh 2) with
                          | True => bal (join l v rl) rv rr
                          | False => create l v r
                        end
                    end
                end
            end


let rec min_elt : t -> elt =
          fun (s : t) =>
            match s with
              | Empty => invalid_arg [elt]
              | Node(l,v,_,_) =>
                match l with
                  | Empty => v
                  | Node(_,_,_,_) => min_elt l
                end
            end


let rec max_elt : t -> elt =
          fun (s : t) =>
            match s with
              | Empty => invalid_arg [elt]
              | Node(_,v,r,_) =>
                match r with
                  | Empty => v
                  | Node(_,_,_,_) => max_elt r
                end
            end


let rec remove_min_elt : t -> t =
          fun (s : t) =>
            match s with
              | Empty => invalid_arg [t]
              | Node(l,v,r,_) =>
                match r with
                  | Empty => r
                  | Node(_,_,_,_) => bal (remove_min_elt l) v r
                end
            end


let merge =
      fun (t0 t1 : t) =>
        match t0 with
          | Empty => t1
          | Node(_,_,_,_) =>
            match t1 with
              | Empty => t0
              | Node(_,_,_,_) => bal t0 (min_elt t1) (remove_min_elt t1)
            end
        end


let concat =
      fun (t0 t1 : t) =>
        match t0 with
          | Empty => t1
          | Node(_,_,_,_) =>
            match t1 with
              | Empty => t0
              | Node(_,_,_,_) => join t0 (min_elt t1) (remove_min_elt t1)
            end
        end


type split_set = SplitSet of t * bool * t


let rec split : elt -> t -> split_set =
          fun (x : elt) (s : t) =>
            match s with
              | Empty => SplitSet(Empty,False,Empty)
              | Node(l,v,r,_) =>
                let c = compare x v in
                match eq c 0 with
                  | True => SplitSet(l,True,r)
                  | False =>
                    match lt c 0 with
                      | True =>
                        match split x l with
                          | SplitSet(ll,pres,rl) => SplitSet(ll,pres,join rl
                            v r)
                        end
                      | False =>
                        match split x r with
                          | SplitSet(lr,pres,rr) => SplitSet(join l v lr,
                            pres,rr)
                        end
                    end
                end
            end


let empty = Empty


let is_empty =
      fun (s : t) => match s with
          | Empty => True
          | Node(_,_,_,_) => False
        end


let rec mem : elt -> t -> bool =
          fun (x : elt) (s : t) =>
            match s with
              | Empty => False
              | Node(l,v,r,_) =>
                let c = compare x v in
                match eq c 0 with
                  | True => True
                  | False => mem x
                    (match lt c 0 with
                       | True => l
                       | False => r
                     end)
                end
            end


let rec mem2 : elt -> t -> bool =
          fun (x : elt) (s : t) =>
            match s with
              | Empty => False
              | Node(l,v,r,_) =>
                let c = compare x v in
                match eq c 0 with
                  | True => True
                  | False => mem2 x
                    (match lt c 0 with
                       | True => l
                       | False => r
                     end)
                end
            end


let rec remove : elt -> t -> t =
          fun (x : elt) (s : t) =>
            match s with
              | Empty => Empty
              | Node(l,v,r,_) =>
                let c = compare x v in
                match eq c 0 with
                  | True => merge l r
                  | False =>
                    match lt c 0 with
                      | True => bal (remove x l) v r
                      | False => bal l v (remove x r)
                    end
                end
            end


let rec cardinal : t -> int =
          fun (s : t) =>
            match s with
              | Empty => 0
              | Node(l,_,r,_) => plus (cardinal l) (plus 1 (cardinal r))
            end


type ('a) m = MEmpty
       | MNode of 'a m * elt * 'a * 'a m * int


let rec orn_m_t : forall 'a. 'a m -> t =
          fun ['a] (m : 'a m) =>
            match m with
              | MEmpty => Empty
              | MNode(l,k,_,r,h) => Node(orn_m_t ['a] l,k,orn_m_t ['a] r,h)
            end


type ('a) option = Some of 'a
       | None


let is_some =
      fun ['a] (x : 'a option) =>
        match x with
          | Some(_) => True
          | None => False
        end


type ('a) split_map = SplitMap of 'a m * 'a option * 'a m


let rec orn_split : forall 'a. 'a split_map -> split_set =
          fun ['a] (s : 'a split_map) =>
            match s with
              | SplitMap(l,v,r) => SplitSet(orn_m_t ['a] l,is_some ['a] v,
                orn_m_t ['a] r)
            end


let forall 'a ornament orn_m_t ['a] : 'a m -> t
  and orn_split ['a] : 'a split_map -> split_set
  and is_some ['a] : 'a option -> bool
  

let rec mheight : forall 'a. 'a m -> ??? =
          fun ['a] (t : 'a m) =>
            match t with
              | MEmpty => 0
              | MNode(_,_,_,_,h) => h
            end
and mcreate : forall 'a. 'a m -> ??? -> 'a -> 'a m -> 'a m =
      fun ['a] (l : 'a m) (v : ???) (x : 'a) (r : 'a m) =>
        let hl = mheight [???] l in
        let hr = mheight [???] r in
        MNode['a](l,v,??v__14__20??,r,
        (match gte hl hr with
           | True => plus hl 1
           | False => plus hr 1
         end))
and mbal : forall 'a. 'a m -> ??? -> 'a -> 'a m -> 'a m =
      fun ['a] (l0 : 'a m) (v : ???) (x : 'a) (r0 : 'a m) =>
        let hl = mheight [???] l0 in
        let hr = mheight [???] r0 in
        match gt hl (plus hr 2) with
          | True =>
            match l0 with
              | MEmpty => invalid_arg ['a m]
              | MNode(l1,k0,_,r1,_) =>
                match gte (mheight [???] l1) (mheight [???] r1) with
                  | True => mcreate [???] l1 k0 ????
                    (mcreate [???] r1 v ???? r0)
                  | False =>
                    match r1 with
                      | MEmpty => invalid_arg ['a m]
                      | MNode(l2,k1,_,r2,_) => mcreate [???]
                        (mcreate [???] l1 k0 ???? l2) k1 ????
                        (mcreate [???] r2 v ???? r0)
                    end
                end
            end
          | False =>
            match gt hr (plus hl 2) with
              | True =>
                match r0 with
                  | MEmpty => invalid_arg ['a m]
                  | MNode(l1,k0,_,r1,_) =>
                    match gte (mheight [???] r1) (mheight [???] l1) with
                      | True => mcreate [???] (mcreate [???] l0 v ???? l1) k0
                        ???? r1
                      | False =>
                        match l1 with
                          | MEmpty => invalid_arg ['a m]
                          | MNode(l2,k1,_,r2,_) => mcreate [???]
                            (mcreate [???] l0 v ???? l2) k1 ????
                            (mcreate [???] r2 k0 ???? r1)
                        end
                    end
                end
              | False => MNode['a](l0,v,??v__55__61??,r0,
                (match gte hl hr with
                   | True => plus hl 1
                   | False => plus hr 1
                 end))
            end
        end
and madd : forall 'a. elt -> 'a -> 'a m -> 'a m =
      fun ['a] (x0 : elt) (x1 : 'a) (s : 'a m) =>
        match s with
          | MEmpty => MNode['a](MEmpty['a],x0,??v__77__83??,MEmpty['a],1)
          | MNode(l,k,_,r,h) =>
            let c = compare x0 k in
            match eq c 0 with
              | True => MNode['a](l,k,??v__116__122??,r,h)
              | False =>
                match lt c 0 with
                  | True => mbal [???] (madd [???] x0 ???? l) k ???? r
                  | False => mbal [???] l k ???? (madd [???] x0 ???? r)
                end
            end
        end
and msingleton : forall 'a. elt -> 'a -> 'a m =
      fun ['a] (x0 : elt) (x1 : 'a) => MNode['a](MEmpty['a],x0,
        ??v__131__137??,MEmpty['a],1)
and madd_min_element : forall 'a. elt -> 'a -> 'a m -> 'a m =
      fun ['a] (v : elt) (x : 'a) (s : 'a m) =>
        match s with
          | MEmpty => msingleton [???] v ????
          | MNode(l,k,_,r,_) => mbal [???] (madd_min_element [???] v ???? l)
            k ???? r
        end
and madd_max_element : forall 'a. elt -> 'a -> 'a m -> 'a m =
      fun ['a] (v : elt) (x : 'a) (s : 'a m) =>
        match s with
          | MEmpty => msingleton [???] v ????
          | MNode(l,k,_,r,_) => mbal [???] l k ????
            (madd_max_element [???] v ???? r)
        end
and mjoin : forall 'a. 'a m -> elt -> 'a -> 'a m -> 'a m =
      fun ['a] (l0 : 'a m) (v : elt) (x : 'a) (r0 : 'a m) =>
        match l0 with
          | MEmpty => madd_min_element [???] v ???? r0
          | MNode(l1,k0,_,r1,h0) =>
            match r0 with
              | MEmpty => madd_max_element [???] v ???? l0
              | MNode(l2,k1,_,r2,h1) =>
                match gt h0 (plus h1 2) with
                  | True => mbal [???] l1 k0 ???? (mjoin [???] r1 v ???? r0)
                  | False =>
                    match gt h1 (plus h0 2) with
                      | True => mbal [???] (mjoin [???] l0 v ???? l2) k1 ????
                        r2
                      | False => mcreate [???] l0 v ???? r0
                    end
                end
            end
        end
and mmin_elt : forall 'a. 'a m -> elt =
      fun ['a] (s : 'a m) =>
        match s with
          | MEmpty => invalid_arg [elt]
          | MNode(l,k,_,_,_) =>
            match l with
              | MEmpty => k
              | MNode(_,_,_,_,_) => mmin_elt [???] l
            end
        end
and mmax_elt : forall 'a. 'a m -> elt =
      fun ['a] (s : 'a m) =>
        match s with
          | MEmpty => invalid_arg [elt]
          | MNode(_,k,_,r,_) =>
            match r with
              | MEmpty => k
              | MNode(_,_,_,_,_) => mmax_elt [???] r
            end
        end
and mremove_min_elt : forall 'a. 'a m -> 'a m =
      fun ['a] (s : 'a m) =>
        match s with
          | MEmpty => invalid_arg ['a m]
          | MNode(l,k,_,r,_) =>
            match r with
              | MEmpty => r
              | MNode(_,_,_,_,_) => mbal [???] (mremove_min_elt [???] l) k
                ???? r
            end
        end
and mmerge : forall 'a. 'a m -> 'a m -> 'a m =
      fun ['a] (t0 t1 : 'a m) =>
        match t0 with
          | MEmpty => t1
          | MNode(_,_,_,_,_) =>
            match t1 with
              | MEmpty => t0
              | MNode(_,_,_,_,_) => mbal [???] t0 (mmin_elt [???] t1) ????
                (mremove_min_elt [???] t1)
            end
        end
and mconcat : forall 'a. 'a m -> 'a m -> 'a m =
      fun ['a] (t0 t1 : 'a m) =>
        match t0 with
          | MEmpty => t1
          | MNode(_,_,_,_,_) =>
            match t1 with
              | MEmpty => t0
              | MNode(_,_,_,_,_) => mjoin [???] t0 (mmin_elt [???] t1) ????
                (mremove_min_elt [???] t1)
            end
        end
and msplit : forall 'a. elt -> 'a m -> 'a split_map =
      fun ['a] (x : elt) (s : 'a m) =>
        match s with
          | MEmpty => SplitMap['a](MEmpty['a],None['a],MEmpty['a])
          | MNode(l0,k,_,r0,_) =>
            let c = compare x k in
            match eq c 0 with
              | True => SplitMap['a](l0,Some['a](??y__327__329??),r0)
              | False =>
                match lt c 0 with
                  | True =>
                    match msplit [???] x l0 with
                      | SplitMap(l1,v,r1) => SplitMap['a](l1,v,mjoin [???] r1
                        k ???? r0)
                    end
                  | False =>
                    match msplit [???] x r0 with
                      | SplitMap(l1,v,r1) => SplitMap['a](mjoin [???] l0 k
                        ???? l1,v,r1)
                    end
                end
            end
        end
and mempty : forall 'a. 'a m = fun ['a] => MEmpty['a]
and mis_empty : forall 'a. 'a m -> bool =
      fun ['a] (s : 'a m) =>
        match s with
          | MEmpty => True
          | MNode(_,_,_,_,_) => False
        end
and mmem : forall 'a. elt -> 'a m -> bool =
      fun ['a] (x : elt) (s : 'a m) =>
        match s with
          | MEmpty => False
          | MNode(l,k,_,r,_) =>
            let c = compare x k in
            match eq c 0 with
              | True => True
              | False => mmem [???] x
                (match lt c 0 with
                   | True => l
                   | False => r
                 end)
            end
        end
and mfind : forall 'a. elt -> 'a m -> 'a option =
      fun ['a] (x : elt) (s : 'a m) =>
        match s with
          | MEmpty => None['a]
          | MNode(l,k,_,r,_) =>
            let c = compare x k in
            match eq c 0 with
              | True => Some['a](??y__399__401??)
              | False => mfind [???] x
                (match lt c 0 with
                   | True => l
                   | False => r
                 end)
            end
        end
and mremove : forall 'a. elt -> 'a m -> 'a m =
      fun ['a] (x : elt) (s : 'a m) =>
        match s with
          | MEmpty => MEmpty['a]
          | MNode(l,k,_,r,_) =>
            let c = compare x k in
            match eq c 0 with
              | True => mmerge [???] l r
              | False =>
                match lt c 0 with
                  | True => mbal [???] (mremove [???] x l) k ???? r
                  | False => mbal [???] l k ???? (mremove [???] x r)
                end
            end
        end
and mcardinal : forall 'a. 'a m -> int =
      fun ['a] (s : 'a m) =>
        match s with
          | MEmpty => 0
          | MNode(l,_,_,r,_) => plus (mcardinal [???] l)
            (plus 1 (mcardinal [???] r))
        end