Theory "enumeral"

Parents toto res_quan

Signature

Type	Arity
bl	1
bt	1
Constant	Type
BL_ACCUM	:α -> α bt -> α bl -> α bl
BL_CONS	:α -> α bl -> α bl
ENUMERAL	:α toto -> α bt -> α -> bool
K2	:α -> num
LESS_ALL	:α toto -> α -> (α -> bool) -> bool
OL	:α toto -> α list -> bool
OL_bt	:α toto -> α bt -> bool
OL_bt_lb	:α toto -> α -> α bt -> bool
OL_bt_lb_ub	:α toto -> α -> α bt -> α -> bool
OL_bt_ub	:α toto -> α bt -> α -> bool
OL_sublists	:α toto -> α list option list -> bool
OU	:α toto -> (α -> bool) -> (α -> bool) -> α -> bool
OWL	:α toto -> (α -> bool) -> α list -> bool
UO	:α toto -> (α -> bool) -> (α -> bool) -> α -> bool
bl_CASE	:α bl -> β -> (α bl -> β) -> (α -> α bt -> α bl -> β) -> β
bl_rev	:α bt -> α bl -> α bt
bl_size	:(α -> num) -> α bl -> num
bl_to_bt	:α bl -> α bt
bl_to_set	:α toto -> α bl -> α -> bool
bt_CASE	:α bt -> β -> (α bt -> α -> α bt -> β) -> β
bt_rev	:α bt -> α bl -> α bl
bt_size	:(α -> num) -> α bt -> num
bt_to_bl	:α bt -> α bl
bt_to_list	:α bt -> α list
bt_to_list_ac	:α bt -> α list -> α list
bt_to_ol	:α toto -> α bt -> α list
bt_to_ol_ac	:α toto -> α bt -> α list -> α list
bt_to_ol_lb	:α toto -> α -> α bt -> α list
bt_to_ol_lb_ac	:α toto -> α -> α bt -> α list -> α list
bt_to_ol_lb_ub	:α toto -> α -> α bt -> α -> α list
bt_to_ol_lb_ub_ac	:α toto -> α -> α bt -> α -> α list -> α list
bt_to_ol_ub	:α toto -> α bt -> α -> α list
bt_to_ol_ub_ac	:α toto -> α bt -> α -> α list -> α list
bt_to_set_lb	:α toto -> α -> α bt -> α -> bool
bt_to_set_lb_ub	:α toto -> α -> α bt -> α -> α -> bool
bt_to_set_ub	:α toto -> α bt -> α -> α -> bool
incr_sbuild	:α toto -> α list -> α list option list
incr_smerge	:α toto -> α list -> α list option list -> α list option list
incr_ssort	:α toto -> α list -> α list
list_to_bl	:α list -> α bl
list_to_bt	:γ list -> γ bt
lol_set	:α list option list -> α -> bool
nbl	:α bl
node	:α bt -> α -> α bt -> α bt
nt	:α bt
onebl	:α -> α bt -> α bl -> α bl
sdiff	:α toto -> α list -> α list -> α list
sinter	:α toto -> α list -> α list -> α list
smerge	:α toto -> α list -> α list -> α list
smerge_out	:α toto -> α list -> α list option list -> α list
zerbl	:α bl -> α bl

Definitions

UO

⊢ ∀cmp s t. UO cmp s t = s ∪ {y | y ∈ t ∧ ∀z. z ∈ s ⇒ (apto cmp z y = Less)}

OWL

⊢ ∀cmp s l. OWL cmp s l ⇔ (s = LIST_TO_SET l) ∧ OL cmp l

OU

⊢ ∀cmp t u. OU cmp t u = {x | x ∈ t ∧ ∀z. z ∈ u ⇒ (apto cmp x z = Less)} ∪ u

OL_bt_ub

⊢ (∀cmp ub. OL_bt_ub cmp nt ub ⇔ T) ∧
  ∀cmp l x r ub.
      OL_bt_ub cmp (node l x r) ub ⇔ OL_bt_ub cmp l x ∧ OL_bt_lb_ub cmp x r ub

OL_bt_lb_ub

⊢ (∀cmp lb ub. OL_bt_lb_ub cmp lb nt ub ⇔ (apto cmp lb ub = Less)) ∧
  ∀cmp lb l x r ub.
      OL_bt_lb_ub cmp lb (node l x r) ub ⇔
      OL_bt_lb_ub cmp lb l x ∧ OL_bt_lb_ub cmp x r ub

OL_bt_lb

⊢ (∀cmp lb. OL_bt_lb cmp lb nt ⇔ T) ∧
  ∀cmp lb l x r.
      OL_bt_lb cmp lb (node l x r) ⇔ OL_bt_lb_ub cmp lb l x ∧ OL_bt_lb cmp x r

OL_bt

⊢ (∀cmp. OL_bt cmp nt ⇔ T) ∧
  ∀cmp l x r. OL_bt cmp (node l x r) ⇔ OL_bt_ub cmp l x ∧ OL_bt_lb cmp x r

OL

⊢ (∀cmp. OL cmp [] ⇔ T) ∧
  ∀cmp a l. OL cmp (a::l) ⇔ OL cmp l ∧ ∀p. MEM p l ⇒ (apto cmp a p = Less)

lol_set_primitive

⊢ lol_set =
  WFREC (@R. WF R ∧ (∀lol. R lol (NONE::lol)) ∧ ∀m lol. R lol (SOME m::lol))
    (λlol_set a.
         case a of
           [] => I ∅
         | NONE::lol => I (lol_set lol)
         | SOME m::lol => I (LIST_TO_SET m ∪ lol_set lol))

list_to_bt

⊢ ∀l. list_to_bt l = bl_to_bt (list_to_bl l)

list_to_bl

⊢ (list_to_bl [] = nbl) ∧ ∀a l. list_to_bl (a::l) = BL_CONS a (list_to_bl l)

LESS_ALL

⊢ ∀cmp x s. LESS_ALL cmp x s ⇔ ∀y. y ∈ s ⇒ (apto cmp x y = Less)

K2

⊢ ∀a. K2 a = 2

incr_ssort

⊢ ∀cmp l. incr_ssort cmp l = smerge_out cmp [] (incr_sbuild cmp l)

incr_sbuild

⊢ (∀cmp. incr_sbuild cmp [] = []) ∧
  ∀cmp x l. incr_sbuild cmp (x::l) = incr_smerge cmp [x] (incr_sbuild cmp l)

bt_TY_DEF

⊢ ∃rep.
      TYPE_DEFINITION
        (λa0'.
             ∀ $var$('bt').
                 (∀a0'.
                      (a0' = ind_type$CONSTR 0 ARB (λn. ind_type$BOTTOM)) ∨
                      (∃a0 a1 a2.
                           (a0' =
                            (λa0 a1 a2.
                                 ind_type$CONSTR (SUC 0) a1
                                   (ind_type$FCONS a0
                                      (ind_type$FCONS a2 (λn. ind_type$BOTTOM))))
                              a0 a1 a2) ∧ $var$('bt') a0 ∧ $var$('bt') a2) ⇒
                      $var$('bt') a0') ⇒
                 $var$('bt') a0') rep

bt_to_set_ub

⊢ ∀cmp t ub.
      bt_to_set_ub cmp t ub =
      {x | x ∈ ENUMERAL cmp t ∧ (apto cmp x ub = Less)}

bt_to_set_lb_ub

⊢ ∀cmp lb t ub.
      bt_to_set_lb_ub cmp lb t ub =
      {x |
       x ∈ ENUMERAL cmp t ∧ (apto cmp lb x = Less) ∧ (apto cmp x ub = Less)}

bt_to_set_lb

⊢ ∀cmp lb t.
      bt_to_set_lb cmp lb t =
      {x | x ∈ ENUMERAL cmp t ∧ (apto cmp lb x = Less)}

bt_to_set

⊢ (∀cmp. ENUMERAL cmp nt = ∅) ∧
  ∀cmp l x r.
      ENUMERAL cmp (node l x r) =
      {y | y ∈ ENUMERAL cmp l ∧ (apto cmp y x = Less)} ∪ {x} ∪
      {z | z ∈ ENUMERAL cmp r ∧ (apto cmp x z = Less)}

bt_to_ol_ub_ac

⊢ (∀cmp ub m. bt_to_ol_ub_ac cmp nt ub m = m) ∧
  ∀cmp l x r ub m.
      bt_to_ol_ub_ac cmp (node l x r) ub m =
      if apto cmp x ub = Less then
        bt_to_ol_ub_ac cmp l x (x::bt_to_ol_lb_ub_ac cmp x r ub m)
      else bt_to_ol_ub_ac cmp l ub m

bt_to_ol_ub

⊢ (∀cmp ub. bt_to_ol_ub cmp nt ub = []) ∧
  ∀cmp l x r ub.
      bt_to_ol_ub cmp (node l x r) ub =
      if apto cmp x ub = Less then
        bt_to_ol_ub cmp l x ++ [x] ++ bt_to_ol_lb_ub cmp x r ub
      else bt_to_ol_ub cmp l ub

bt_to_ol_lb_ub_ac

⊢ (∀cmp lb ub m. bt_to_ol_lb_ub_ac cmp lb nt ub m = m) ∧
  ∀cmp lb l x r ub m.
      bt_to_ol_lb_ub_ac cmp lb (node l x r) ub m =
      if apto cmp lb x = Less then
        if apto cmp x ub = Less then
          bt_to_ol_lb_ub_ac cmp lb l x (x::bt_to_ol_lb_ub_ac cmp x r ub m)
        else bt_to_ol_lb_ub_ac cmp lb l ub m
      else bt_to_ol_lb_ub_ac cmp lb r ub m

bt_to_ol_lb_ub

⊢ (∀cmp lb ub. bt_to_ol_lb_ub cmp lb nt ub = []) ∧
  ∀cmp lb l x r ub.
      bt_to_ol_lb_ub cmp lb (node l x r) ub =
      if apto cmp lb x = Less then
        if apto cmp x ub = Less then
          bt_to_ol_lb_ub cmp lb l x ++ [x] ++ bt_to_ol_lb_ub cmp x r ub
        else bt_to_ol_lb_ub cmp lb l ub
      else bt_to_ol_lb_ub cmp lb r ub

bt_to_ol_lb_ac

⊢ (∀cmp lb m. bt_to_ol_lb_ac cmp lb nt m = m) ∧
  ∀cmp lb l x r m.
      bt_to_ol_lb_ac cmp lb (node l x r) m =
      if apto cmp lb x = Less then
        bt_to_ol_lb_ub_ac cmp lb l x (x::bt_to_ol_lb_ac cmp x r m)
      else bt_to_ol_lb_ac cmp lb r m

bt_to_ol_lb

⊢ (∀cmp lb. bt_to_ol_lb cmp lb nt = []) ∧
  ∀cmp lb l x r.
      bt_to_ol_lb cmp lb (node l x r) =
      if apto cmp lb x = Less then
        bt_to_ol_lb_ub cmp lb l x ++ [x] ++ bt_to_ol_lb cmp x r
      else bt_to_ol_lb cmp lb r

bt_to_ol_ac

⊢ (∀cmp m. bt_to_ol_ac cmp nt m = m) ∧
  ∀cmp l x r m.
      bt_to_ol_ac cmp (node l x r) m =
      bt_to_ol_ub_ac cmp l x (x::bt_to_ol_lb_ac cmp x r m)

bt_to_ol

⊢ (∀cmp. bt_to_ol cmp nt = []) ∧
  ∀cmp l x r.
      bt_to_ol cmp (node l x r) =
      bt_to_ol_ub cmp l x ++ [x] ++ bt_to_ol_lb cmp x r

bt_to_list_ac

⊢ (∀m. bt_to_list_ac nt m = m) ∧
  ∀l x r m.
      bt_to_list_ac (node l x r) m = bt_to_list_ac l (x::bt_to_list_ac r m)

bt_to_list

⊢ (bt_to_list nt = []) ∧
  ∀l x r. bt_to_list (node l x r) = bt_to_list l ++ [x] ++ bt_to_list r

bt_to_bl

⊢ ∀t. bt_to_bl t = bt_rev t nbl

bt_size_def

⊢ (∀f. bt_size f nt = 0) ∧
  ∀f a0 a1 a2.
      bt_size f (node a0 a1 a2) = 1 + (bt_size f a0 + (f a1 + bt_size f a2))

bt_rev

⊢ (∀bl. bt_rev nt bl = bl) ∧
  ∀lft r rft bl. bt_rev (node lft r rft) bl = bt_rev lft (onebl r rft bl)

bl_TY_DEF

⊢ ∃rep.
      TYPE_DEFINITION
        (λa0'.
             ∀ $var$('bl').
                 (∀a0'.
                      (a0' = ind_type$CONSTR 0 (ARB,ARB) (λn. ind_type$BOTTOM)) ∨
                      (∃a.
                           (a0' =
                            (λa.
                                 ind_type$CONSTR (SUC 0) (ARB,ARB)
                                   (ind_type$FCONS a (λn. ind_type$BOTTOM))) a) ∧
                           $var$('bl') a) ∨
                      (∃a0 a1 a2.
                           (a0' =
                            (λa0 a1 a2.
                                 ind_type$CONSTR (SUC (SUC 0)) (a0,a1)
                                   (ind_type$FCONS a2 (λn. ind_type$BOTTOM)))
                              a0 a1 a2) ∧ $var$('bl') a2) ⇒
                      $var$('bl') a0') ⇒
                 $var$('bl') a0') rep

bl_to_set

⊢ (∀cmp. bl_to_set cmp nbl = ∅) ∧
  (∀cmp b. bl_to_set cmp (zerbl b) = bl_to_set cmp b) ∧
  ∀cmp x t b.
      bl_to_set cmp (onebl x t b) =
      OU cmp ({x} ∪ {y | y ∈ ENUMERAL cmp t ∧ (apto cmp x y = Less)})
        (bl_to_set cmp b)

bl_to_bt

⊢ bl_to_bt = bl_rev nt

bl_size_def

⊢ (∀f. bl_size f nbl = 0) ∧ (∀f a. bl_size f (zerbl a) = 1 + bl_size f a) ∧
  ∀f a0 a1 a2.
      bl_size f (onebl a0 a1 a2) = 1 + (f a0 + (bt_size f a1 + bl_size f a2))

bl_rev

⊢ (∀ft. bl_rev ft nbl = ft) ∧ (∀ft b. bl_rev ft (zerbl b) = bl_rev ft b) ∧
  ∀ft a f b. bl_rev ft (onebl a f b) = bl_rev (node ft a f) b

BL_CONS

⊢ ∀a bl. BL_CONS a bl = BL_ACCUM a nt bl

bl_case_def

⊢ (∀v f f1. bl_CASE nbl v f f1 = v) ∧
  (∀a v f f1. bl_CASE (zerbl a) v f f1 = f a) ∧
  ∀a0 a1 a2 v f f1. bl_CASE (onebl a0 a1 a2) v f f1 = f1 a0 a1 a2

BL_ACCUM

⊢ (∀a ac. BL_ACCUM a ac nbl = onebl a ac nbl) ∧
  (∀a ac bl. BL_ACCUM a ac (zerbl bl) = onebl a ac bl) ∧
  ∀a ac r rft bl.
      BL_ACCUM a ac (onebl r rft bl) = zerbl (BL_ACCUM a (node ac r rft) bl)

Theorems

smerge_out_ind

⊢ ∀P.
      (∀cmp l. P cmp l []) ∧ (∀cmp l lol. P cmp l lol ⇒ P cmp l (NONE::lol)) ∧
      (∀cmp l m lol. P cmp (smerge cmp l m) lol ⇒ P cmp l (SOME m::lol)) ⇒
      ∀v v1 v2. P v v1 v2

smerge_out

⊢ (∀l cmp. smerge_out cmp l [] = l) ∧
  (∀lol l cmp. smerge_out cmp l (NONE::lol) = smerge_out cmp l lol) ∧
  ∀m lol l cmp.
      smerge_out cmp l (SOME m::lol) = smerge_out cmp (smerge cmp l m) lol

smerge_OL

⊢ ∀cmp l m. OL cmp l ∧ OL cmp m ⇒ OL cmp (smerge cmp l m)

smerge_nil

⊢ ∀cmp l. (smerge cmp l [] = l) ∧ (smerge cmp [] l = l)

smerge_ind

⊢ ∀P.
      (∀cmp. P cmp [] []) ∧ (∀cmp x l. P cmp (x::l) []) ∧
      (∀cmp y m. P cmp [] (y::m)) ∧
      (∀cmp x l y m.
           ((apto cmp x y = Equal) ⇒ P cmp l m) ∧
           ((apto cmp x y = Greater) ⇒ P cmp (x::l) m) ∧
           ((apto cmp x y = Less) ⇒ P cmp l (y::m)) ⇒
           P cmp (x::l) (y::m)) ⇒
      ∀v v1 v2. P v v1 v2

smerge

⊢ (∀cmp. smerge cmp [] [] = []) ∧ (∀x l cmp. smerge cmp (x::l) [] = x::l) ∧
  (∀y m cmp. smerge cmp [] (y::m) = y::m) ∧
  ∀y x m l cmp.
      smerge cmp (x::l) (y::m) =
      case apto cmp x y of
        Less => x::smerge cmp l (y::m)
      | Equal => x::smerge cmp l m
      | Greater => y::smerge cmp (x::l) m

sinter_ind

⊢ ∀P.
      (∀cmp. P cmp [] []) ∧ (∀cmp x l. P cmp (x::l) []) ∧
      (∀cmp y m. P cmp [] (y::m)) ∧
      (∀cmp x l y m.
           ((apto cmp x y = Equal) ⇒ P cmp l m) ∧
           ((apto cmp x y = Greater) ⇒ P cmp (x::l) m) ∧
           ((apto cmp x y = Less) ⇒ P cmp l (y::m)) ⇒
           P cmp (x::l) (y::m)) ⇒
      ∀v v1 v2. P v v1 v2

sinter

⊢ (∀cmp. sinter cmp [] [] = []) ∧ (∀x l cmp. sinter cmp (x::l) [] = []) ∧
  (∀y m cmp. sinter cmp [] (y::m) = []) ∧
  ∀y x m l cmp.
      sinter cmp (x::l) (y::m) =
      case apto cmp x y of
        Less => sinter cmp l (y::m)
      | Equal => x::sinter cmp l m
      | Greater => sinter cmp (x::l) m

set_OWL_thm

⊢ ∀cmp l. OWL cmp (LIST_TO_SET l) (incr_ssort cmp l)

sdiff_ind

⊢ ∀P.
      (∀cmp. P cmp [] []) ∧ (∀cmp x l. P cmp (x::l) []) ∧
      (∀cmp y m. P cmp [] (y::m)) ∧
      (∀cmp x l y m.
           ((apto cmp x y = Equal) ⇒ P cmp l m) ∧
           ((apto cmp x y = Greater) ⇒ P cmp (x::l) m) ∧
           ((apto cmp x y = Less) ⇒ P cmp l (y::m)) ⇒
           P cmp (x::l) (y::m)) ⇒
      ∀v v1 v2. P v v1 v2

sdiff

⊢ (∀cmp. sdiff cmp [] [] = []) ∧ (∀x l cmp. sdiff cmp (x::l) [] = x::l) ∧
  (∀y m cmp. sdiff cmp [] (y::m) = []) ∧
  ∀y x m l cmp.
      sdiff cmp (x::l) (y::m) =
      case apto cmp x y of
        Less => x::sdiff cmp l (y::m)
      | Equal => sdiff cmp l m
      | Greater => sdiff cmp (x::l) m

OWL_UNION_THM

⊢ ∀cmp s l t m. OWL cmp s l ∧ OWL cmp t m ⇒ OWL cmp (s ∪ t) (smerge cmp l m)

OWL_INTER_THM

⊢ ∀cmp s l t m. OWL cmp s l ∧ OWL cmp t m ⇒ OWL cmp (s ∩ t) (sinter cmp l m)

OWL_DIFF_THM

⊢ ∀cmp s l t m. OWL cmp s l ∧ OWL cmp t m ⇒ OWL cmp (s DIFF t) (sdiff cmp l m)

OWL_bt_to_ol

⊢ ∀cmp t. OWL cmp (ENUMERAL cmp t) (bt_to_ol cmp t)

OU_EMPTY

⊢ ∀cmp t. OU cmp t ∅ = t

OU_ASSOC

⊢ ∀cmp a b c. OU cmp a (OU cmp b c) = OU cmp (OU cmp a b) c

OL_UNION_IMP

⊢ ∀cmp l.
      OL cmp l ⇒
      ∀m.
          OL cmp m ⇒
          OL cmp (smerge cmp l m) ∧
          (LIST_TO_SET (smerge cmp l m) = LIST_TO_SET l ∪ LIST_TO_SET m)

OL_sublists_ind

⊢ ∀P.
      (∀cmp. P cmp []) ∧ (∀cmp lol. P cmp lol ⇒ P cmp (NONE::lol)) ∧
      (∀cmp m lol. P cmp lol ⇒ P cmp (SOME m::lol)) ⇒
      ∀v v1. P v v1

OL_sublists

⊢ (∀cmp. OL_sublists cmp [] ⇔ T) ∧
  (∀lol cmp. OL_sublists cmp (NONE::lol) ⇔ OL_sublists cmp lol) ∧
  ∀m lol cmp. OL_sublists cmp (SOME m::lol) ⇔ OL cmp m ∧ OL_sublists cmp lol

ol_set

⊢ ∀cmp t. ENUMERAL cmp t = LIST_TO_SET (bt_to_ol cmp t)

OL_INTER_IMP

⊢ ∀cmp l.
      OL cmp l ⇒
      ∀m.
          OL cmp m ⇒
          OL cmp (sinter cmp l m) ∧
          (LIST_TO_SET (sinter cmp l m) = LIST_TO_SET l ∩ LIST_TO_SET m)

OL_ENUMERAL

⊢ ∀cmp l. OL cmp l ⇒ (LIST_TO_SET l = ENUMERAL cmp (list_to_bt l))

OL_DIFF_IMP

⊢ ∀cmp l.
      OL cmp l ⇒
      ∀m.
          OL cmp m ⇒
          OL cmp (sdiff cmp l m) ∧
          (LIST_TO_SET (sdiff cmp l m) = LIST_TO_SET l DIFF LIST_TO_SET m)

OL_bt_to_ol_ub

⊢ ∀cmp t ub. OL cmp (bt_to_ol_ub cmp t ub)

OL_bt_to_ol_lb_ub

⊢ ∀cmp t lb ub. OL cmp (bt_to_ol_lb_ub cmp lb t ub)

OL_bt_to_ol_lb

⊢ ∀cmp t lb. OL cmp (bt_to_ol_lb cmp lb t)

OL_bt_to_ol

⊢ ∀cmp t. OL cmp (bt_to_ol cmp t)

NOT_IN_nt

⊢ ∀cmp y. y ∈ ENUMERAL cmp nt ⇔ F

lol_set_ind

⊢ ∀P.
      P [] ∧ (∀lol. P lol ⇒ P (NONE::lol)) ∧ (∀m lol. P lol ⇒ P (SOME m::lol)) ⇒
      ∀v. P v

lol_set

⊢ (lol_set [] = ∅) ∧ (∀lol. lol_set (NONE::lol) = lol_set lol) ∧
  ∀m lol. lol_set (SOME m::lol) = LIST_TO_SET m ∪ lol_set lol

LESS_UO_LEM

⊢ ∀cmp x y s.
      (∀z. z ∈ UO cmp {x} s ⇒ (apto cmp y z = Less)) ⇔ (apto cmp y x = Less)

LESS_ALL_UO_LEM

⊢ ∀cmp a s. LESS_ALL cmp a s ⇒ (UO cmp {a} s = a INSERT s)

LESS_ALL_OU_UO_LEM

⊢ ∀cmp a s t.
      LESS_ALL cmp a s ∧ LESS_ALL cmp a t ⇒
      (OU cmp (UO cmp {a} s) t = a INSERT OU cmp s t)

LESS_ALL_OU

⊢ ∀cmp x u v.
      LESS_ALL cmp x (OU cmp u v) ⇔ LESS_ALL cmp x u ∧ LESS_ALL cmp x v

incr_smerge_OL

⊢ ∀cmp lol l.
      OL_sublists cmp lol ∧ OL cmp l ⇒ OL_sublists cmp (incr_smerge cmp l lol)

incr_smerge_ind

⊢ ∀P.
      (∀cmp l. P cmp l []) ∧ (∀cmp l lol. P cmp l (NONE::lol)) ∧
      (∀cmp l m lol. P cmp (smerge cmp l m) lol ⇒ P cmp l (SOME m::lol)) ⇒
      ∀v v1 v2. P v v1 v2

incr_smerge

⊢ (∀l cmp. incr_smerge cmp l [] = [SOME l]) ∧
  (∀lol l cmp. incr_smerge cmp l (NONE::lol) = SOME l::lol) ∧
  ∀m lol l cmp.
      incr_smerge cmp l (SOME m::lol) =
      NONE::incr_smerge cmp (smerge cmp l m) lol

IN_node

⊢ ∀cmp x l y r.
      x ∈ ENUMERAL cmp (node l y r) ⇔
      case apto cmp x y of
        Less => x ∈ ENUMERAL cmp l
      | Equal => T
      | Greater => x ∈ ENUMERAL cmp r

IN_bt_to_set

⊢ (∀cmp y. y ∈ ENUMERAL cmp nt ⇔ F) ∧
  ∀cmp l x r y.
      y ∈ ENUMERAL cmp (node l x r) ⇔
      y ∈ ENUMERAL cmp l ∧ (apto cmp y x = Less) ∨ (y = x) ∨
      y ∈ ENUMERAL cmp r ∧ (apto cmp x y = Less)

ENUMERAL_set

⊢ ∀cmp l. LIST_TO_SET l = ENUMERAL cmp (list_to_bt (incr_ssort cmp l))

EMPTY_OU

⊢ ∀cmp sl. OU cmp ∅ sl = sl

datatype_bt

⊢ DATATYPE (bt nt node)

datatype_bl

⊢ DATATYPE (bl nbl zerbl onebl)

bt_to_ol_ID_IMP

⊢ ∀cmp l. OL cmp l ⇒ (bt_to_ol cmp (list_to_bt l) = l)

bt_to_list_thm

⊢ ∀t. bt_to_list t = bt_to_list_ac t []

bt_nchotomy

⊢ ∀bb. (bb = nt) ∨ ∃b a b0. bb = node b a b0

bt_induction

⊢ ∀P. P nt ∧ (∀b b0. P b ∧ P b0 ⇒ ∀a. P (node b a b0)) ⇒ ∀b. P b

bt_distinct

⊢ ∀a2 a1 a0. nt ≠ node a0 a1 a2

bt_case_eq

⊢ (bt_CASE x v f = v') ⇔
  (x = nt) ∧ (v = v') ∨ ∃b a b0. (x = node b a b0) ∧ (f b a b0 = v')

bt_case_def

⊢ (∀v f. bt_CASE nt v f = v) ∧
  ∀a0 a1 a2 v f. bt_CASE (node a0 a1 a2) v f = f a0 a1 a2

bt_case_cong

⊢ ∀M M' v f.
      (M = M') ∧ ((M' = nt) ⇒ (v = v')) ∧
      (∀a0 a1 a2. (M' = node a0 a1 a2) ⇒ (f a0 a1 a2 = f' a0 a1 a2)) ⇒
      (bt_CASE M v f = bt_CASE M' v' f')

bt_Axiom

⊢ ∀f0 f1.
      ∃fn.
          (fn nt = f0) ∧
          ∀a0 a1 a2. fn (node a0 a1 a2) = f1 a1 a0 a2 (fn a0) (fn a2)

bt_11

⊢ ∀a0 a1 a2 a0' a1' a2'.
      (node a0 a1 a2 = node a0' a1' a2') ⇔
      (a0 = a0') ∧ (a1 = a1') ∧ (a2 = a2')

bl_nchotomy

⊢ ∀bb. (bb = nbl) ∨ (∃b. bb = zerbl b) ∨ ∃a b0 b. bb = onebl a b0 b

bl_induction

⊢ ∀P.
      P nbl ∧ (∀b. P b ⇒ P (zerbl b)) ∧ (∀b. P b ⇒ ∀b0 a. P (onebl a b0 b)) ⇒
      ∀b. P b

bl_distinct

⊢ (∀a. nbl ≠ zerbl a) ∧ (∀a2 a1 a0. nbl ≠ onebl a0 a1 a2) ∧
  ∀a2 a1 a0 a. zerbl a ≠ onebl a0 a1 a2

bl_case_eq

⊢ (bl_CASE x v f f1 = v') ⇔
  (x = nbl) ∧ (v = v') ∨ (∃b. (x = zerbl b) ∧ (f b = v')) ∨
  ∃a b0 b. (x = onebl a b0 b) ∧ (f1 a b0 b = v')

bl_case_cong

⊢ ∀M M' v f f1.
      (M = M') ∧ ((M' = nbl) ⇒ (v = v')) ∧
      (∀a. (M' = zerbl a) ⇒ (f a = f' a)) ∧
      (∀a0 a1 a2. (M' = onebl a0 a1 a2) ⇒ (f1 a0 a1 a2 = f1' a0 a1 a2)) ⇒
      (bl_CASE M v f f1 = bl_CASE M' v' f' f1')

bl_Axiom

⊢ ∀f0 f1 f2.
      ∃fn.
          (fn nbl = f0) ∧ (∀a. fn (zerbl a) = f1 a (fn a)) ∧
          ∀a0 a1 a2. fn (onebl a0 a1 a2) = f2 a0 a1 a2 (fn a2)

bl_11

⊢ (∀a a'. (zerbl a = zerbl a') ⇔ (a = a')) ∧
  ∀a0 a1 a2 a0' a1' a2'.
      (onebl a0 a1 a2 = onebl a0' a1' a2') ⇔
      (a0 = a0') ∧ (a1 = a1') ∧ (a2 = a2')

better_bt_to_ol

⊢ ∀cmp t.
      bt_to_ol cmp t =
      if OL_bt cmp t then bt_to_list_ac t [] else bt_to_ol_ac cmp t []