```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

```