Theory "enumeral"

Signature

Definitions

bl_TY_DEF

|- ∃rep.
     TYPE_DEFINITION
       (λa0'.
          ∀'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) ∧
                  '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) ∧
                  'bl' a2) ⇒
               'bl' a0') ⇒
            'bl' a0') rep

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_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))

bt_TY_DEF

|- ∃rep.
     TYPE_DEFINITION
       (λa0'.
          ∀'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) ∧ 'bt' a0 ∧ 'bt' a2) ⇒
               'bt' a0') ⇒
            'bt' a0') rep

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

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)

BL_CONS

|- ∀a bl. BL_CONS a bl = BL_ACCUM a nt bl

list_to_bl

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

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_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_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)

K2

|- ∀a. K2 a = 2

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_to_bt

|- bl_to_bt = bl_rev nt

bt_to_bl

|- ∀t. bt_to_bl t = bt_rev t nbl

list_to_bt

|- ∀l. list_to_bt l = bl_to_bt (list_to_bl l)

OL

|- (∀cmp. OL cmp [] ⇔ T) ∧
   ∀cmp a l. OL cmp (a::l) ⇔ OL cmp l ∧ ∀p. MEM p l ⇒ (apto cmp a p = LESS)

smerge_tupled_primitive

|- smerge_tupled =
   WFREC
     (@R.
        WF R ∧
        (∀m l y x cmp. (apto cmp x y = EQUAL) ⇒ R (cmp,l,m) (cmp,x::l,y::m)) ∧
        (∀m l y x cmp.
           (apto cmp x y = GREATER) ⇒ R (cmp,x::l,m) (cmp,x::l,y::m)) ∧
        ∀m l y x cmp. (apto cmp x y = LESS) ⇒ R (cmp,l,y::m) (cmp,x::l,y::m))
     (λsmerge_tupled a.
        case a of
          (cmp,[],[]) => I []
        | (cmp,[],y::m) => I (y::m)
        | (cmp,x::l,[]) => I (x::l)
        | (cmp,x::l,y'::m') =>
            I
              (case apto cmp x y' of
                 LESS => x::smerge_tupled (cmp,l,y'::m')
               | EQUAL => x::smerge_tupled (cmp,l,m')
               | GREATER => y'::smerge_tupled (cmp,x::l,m')))

smerge_curried

|- ∀x x1 x2. smerge x x1 x2 = smerge_tupled (x,x1,x2)

OL_sublists_tupled_primitive

|- OL_sublists_tupled =
   WFREC
     (@R.
        WF R ∧ (∀lol cmp. R (cmp,lol) (cmp,NONE::lol)) ∧
        ∀m lol cmp. R (cmp,lol) (cmp,SOME m::lol))
     (λOL_sublists_tupled a.
        case a of
          (cmp,[]) => I T
        | (cmp,NONE::lol) => I (OL_sublists_tupled (cmp,lol))
        | (cmp,SOME m::lol) => I (OL cmp m ∧ OL_sublists_tupled (cmp,lol)))

OL_sublists_curried

|- ∀x x1. OL_sublists x x1 ⇔ OL_sublists_tupled (x,x1)

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

incr_smerge_tupled_primitive

|- incr_smerge_tupled =
   WFREC
     (@R. WF R ∧ ∀lol m l cmp. R (cmp,smerge cmp l m,lol) (cmp,l,SOME m::lol))
     (λincr_smerge_tupled a.
        case a of
          (cmp,l,[]) => I [SOME l]
        | (cmp,l,NONE::lol) => I (SOME l::lol)
        | (cmp,l,SOME m::lol) =>
            I (NONE::incr_smerge_tupled (cmp,smerge cmp l m,lol)))

incr_smerge_curried

|- ∀x x1 x2. incr_smerge x x1 x2 = incr_smerge_tupled (x,x1,x2)

smerge_out_tupled_primitive

|- smerge_out_tupled =
   WFREC
     (@R.
        WF R ∧ (∀lol l cmp. R (cmp,l,lol) (cmp,l,NONE::lol)) ∧
        ∀lol m l cmp. R (cmp,smerge cmp l m,lol) (cmp,l,SOME m::lol))
     (λsmerge_out_tupled a.
        case a of
          (cmp,l,[]) => I l
        | (cmp,l,NONE::lol) => I (smerge_out_tupled (cmp,l,lol))
        | (cmp,l,SOME m::lol) =>
            I (smerge_out_tupled (cmp,smerge cmp l m,lol)))

smerge_out_curried

|- ∀x x1 x2. smerge_out x x1 x2 = smerge_out_tupled (x,x1,x2)

incr_sbuild

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

incr_ssort

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

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

|- (∀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_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

|- (∀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_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_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_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_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)

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

UO

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

LESS_ALL

|- ∀cmp x s. LESS_ALL cmp x s ⇔ ∀y. y ∈ s ⇒ (apto cmp x y = LESS)

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)

sinter_tupled_primitive

|- sinter_tupled =
   WFREC
     (@R.
        WF R ∧
        (∀m l y x cmp. (apto cmp x y = EQUAL) ⇒ R (cmp,l,m) (cmp,x::l,y::m)) ∧
        (∀m l y x cmp.
           (apto cmp x y = GREATER) ⇒ R (cmp,x::l,m) (cmp,x::l,y::m)) ∧
        ∀m l y x cmp. (apto cmp x y = LESS) ⇒ R (cmp,l,y::m) (cmp,x::l,y::m))
     (λsinter_tupled a.
        case a of
          (cmp,x::l,y::m) =>
            I
              (case apto cmp x y of
                 LESS => sinter_tupled (cmp,l,y::m)
               | EQUAL => x::sinter_tupled (cmp,l,m)
               | GREATER => sinter_tupled (cmp,x::l,m))
        | _ => I [])

sinter_curried

|- ∀x x1 x2. sinter x x1 x2 = sinter_tupled (x,x1,x2)

sdiff_tupled_primitive

|- sdiff_tupled =
   WFREC
     (@R.
        WF R ∧
        (∀m l y x cmp. (apto cmp x y = EQUAL) ⇒ R (cmp,l,m) (cmp,x::l,y::m)) ∧
        (∀m l y x cmp.
           (apto cmp x y = GREATER) ⇒ R (cmp,x::l,m) (cmp,x::l,y::m)) ∧
        ∀m l y x cmp. (apto cmp x y = LESS) ⇒ R (cmp,l,y::m) (cmp,x::l,y::m))
     (λsdiff_tupled a.
        case a of
          (cmp,[],v3) => I []
        | (cmp,x::l,[]) => I (x::l)
        | (cmp,x::l,y::m) =>
            I
              (case apto cmp x y of
                 LESS => x::sdiff_tupled (cmp,l,y::m)
               | EQUAL => sdiff_tupled (cmp,l,m)
               | GREATER => sdiff_tupled (cmp,x::l,m)))

sdiff_curried

|- ∀x x1 x2. sdiff x x1 x2 = sdiff_tupled (x,x1,x2)

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

|- (∀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

Theorems

bt_distinct

|- ∀a2 a1 a0. nt ≠ node 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_nchotomy

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

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_induction

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

datatype_bl

|- DATATYPE (bl nbl zerbl onebl)

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')

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_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_nchotomy

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

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_induction

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

bt_11

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

datatype_bt

|- DATATYPE (bt nt node)

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_to_list_thm

|- ∀t. bt_to_list t = bt_to_list_ac t []

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

smerge_nil

|- ∀cmp l. (smerge cmp l [] = l) ∧ (smerge cmp [] l = l)

smerge_OL

|- ∀cmp l m. OL cmp l ∧ OL cmp m ⇒ OL cmp (smerge cmp l 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

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

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

incr_smerge_OL

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

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

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)

NOT_IN_nt

|- ∀cmp y. y ∈ ENUMERAL cmp nt ⇔ F

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

ol_set

|- ∀cmp t. ENUMERAL cmp t = LIST_TO_SET (bt_to_ol cmp t)

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_ub

|- ∀cmp t ub. OL cmp (bt_to_ol_ub cmp t ub)

OL_bt_to_ol

|- ∀cmp t. OL cmp (bt_to_ol cmp t)

OWL_bt_to_ol

|- ∀cmp t. OWL cmp (ENUMERAL cmp t) (bt_to_ol cmp t)

EMPTY_OU

|- ∀cmp sl. OU cmp ∅ sl = sl

OU_EMPTY

|- ∀cmp t. OU cmp t ∅ = t

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_OU

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

OU_ASSOC

|- ∀cmp a b c. OU cmp a (OU cmp b c) = OU cmp (OU cmp a b) c

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)

bt_to_ol_ID_IMP

|- ∀cmp l. OL cmp l ⇒ (bt_to_ol cmp (list_to_bt l) = l)

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)

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

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)

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

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)

ENUMERAL_set

|- ∀cmp l. LIST_TO_SET l = ENUMERAL cmp (list_to_bt (incr_ssort cmp l))

OL_ENUMERAL

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

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)

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 []

set_OWL_thm

|- ∀cmp l. OWL cmp (LIST_TO_SET l) (incr_ssort cmp l)