Theory "fmapal"

Signature

Definitions

ORL_tupled_primitive

|- ORL_tupled =
   WFREC (@R. WF R ∧ ∀b a l cmp. R (cmp,l) (cmp,(a,b)::l))
     (λORL_tupled a'.
        case a' of
          (cmp,[]) => I T
        | (cmp,(a,b)::l) =>
            I
              (ORL_tupled (cmp,l) ∧
               ∀p q. MEM (p,q) l ⇒ (apto cmp a p = LESS)))

ORL_curried

|- ∀x x1. ORL x x1 ⇔ ORL_tupled (x,x1)

optry

|- (∀p q. optry (SOME p) q = SOME p) ∧ ∀q. optry NONE q = q

optry_list_tupled_primitive

|- optry_list_tupled =
   WFREC
     (@R. WF R ∧ (∀l f. R (f,l) (f,NONE::l)) ∧ ∀z l f. R (f,l) (f,SOME z::l))
     (λoptry_list_tupled a.
        case a of
          (f,[]) => I NONE
        | (f,NONE::l) => I (optry_list_tupled (f,l))
        | (f,SOME z::l) => I (optry (f z) (optry_list_tupled (f,l))))

optry_list_curried

|- ∀x x1. optry_list x x1 = optry_list_tupled (x,x1)

assocv_tupled_primitive

|- assocv_tupled =
   WFREC (@R. WF R ∧ ∀y l x a. a ≠ x ⇒ R (l,a) ((x,y)::l,a))
     (λassocv_tupled a'.
        case a' of
          ([],a) => I NONE
        | ((x,y)::l,a) => I (if a = x then SOME y else assocv_tupled (l,a)))

assocv_curried

|- ∀x x1. assocv x x1 = assocv_tupled (x,x1)

vcossa

|- ∀a l. vcossa a l = assocv l a

OPTION_UPDATE

|- ∀f g x. OPTION_UPDATE f g x = optry (f x) (g x)

merge_tupled_primitive

|- merge_tupled =
   WFREC
     (@R.
        WF R ∧
        (∀b2 b1 l2 l1 a2 a1 cmp.
           (apto cmp a1 a2 = EQUAL) ⇒
           R (cmp,l1,l2) (cmp,(a1,b1)::l1,(a2,b2)::l2)) ∧
        (∀b2 l2 l1 b1 a2 a1 cmp.
           (apto cmp a1 a2 = GREATER) ⇒
           R (cmp,(a1,b1)::l1,l2) (cmp,(a1,b1)::l1,(a2,b2)::l2)) ∧
        ∀b1 l2 b2 l1 a2 a1 cmp.
          (apto cmp a1 a2 = LESS) ⇒
          R (cmp,l1,(a2,b2)::l2) (cmp,(a1,b1)::l1,(a2,b2)::l2))
     (λmerge_tupled a.
        case a of
          (cmp,[],l) => I l
        | (cmp,v6::l1,[]) => I (v6::l1)
        | (cmp,(a1,b1)::l1,(a2,b2)::l2) =>
            I
              (case apto cmp a1 a2 of
                 LESS => (a1,b1)::merge_tupled (cmp,l1,(a2,b2)::l2)
               | EQUAL => (a1,b1)::merge_tupled (cmp,l1,l2)
               | GREATER => (a2,b2)::merge_tupled (cmp,(a1,b1)::l1,l2)))

merge_curried

|- ∀x x1 x2. merge x x1 x2 = merge_tupled (x,x1,x2)

incr_merge_tupled_primitive

|- incr_merge_tupled =
   WFREC
     (@R. WF R ∧ ∀lol m l cmp. R (cmp,merge cmp l m,lol) (cmp,l,SOME m::lol))
     (λincr_merge_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_merge_tupled (cmp,merge cmp l m,lol)))

incr_merge_curried

|- ∀x x1 x2. incr_merge x x1 x2 = incr_merge_tupled (x,x1,x2)

ORL_sublists_tupled_primitive

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

ORL_sublists_curried

|- ∀x x1. ORL_sublists x x1 ⇔ ORL_sublists_tupled (x,x1)

incr_build

|- (∀cmp. incr_build cmp [] = []) ∧
   ∀cmp ab l. incr_build cmp (ab::l) = incr_merge cmp [ab] (incr_build cmp l)

merge_out_tupled_primitive

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

merge_out_curried

|- ∀x x1 x2. merge_out x x1 x2 = merge_out_tupled (x,x1,x2)

incr_flat

|- ∀cmp lol. incr_flat cmp lol = merge_out cmp [] lol

incr_sort

|- ∀cmp l. incr_sort cmp l = merge_out cmp [] (incr_build cmp l)

OPTION_FLAT_primitive

|- OPTION_FLAT =
   WFREC (@R. WF R ∧ (∀l. R l (NONE::l)) ∧ ∀a l. R l (SOME a::l))
     (λOPTION_FLAT a'.
        case a' of
          [] => I []
        | NONE::l => I (OPTION_FLAT l)
        | SOME a::l => I (a ++ OPTION_FLAT l))

unlookup

|- ∀f. unlookup f = FUN_FMAP (THE o f) (IS_SOME o f)

bt_to_fmap_tupled_primitive

|- bt_to_fmap_tupled =
   WFREC
     (@R.
        WF R ∧ (∀r v x l cmp. R (cmp,l) (cmp,node l (x,v) r)) ∧
        ∀v x l r cmp. R (cmp,r) (cmp,node l (x,v) r))
     (λbt_to_fmap_tupled a.
        case a of
          (cmp,nt) => I FEMPTY
        | (cmp,node l (x,v) r) =>
            I
              (DRESTRICT (bt_to_fmap_tupled (cmp,l))
                 {y | apto cmp y x = LESS} ⊌ FEMPTY |+ (x,v) ⊌
               DRESTRICT (bt_to_fmap_tupled (cmp,r))
                 {z | apto cmp x z = LESS}))

bt_to_fmap_curried

|- ∀x x1. FMAPAL x x1 = bt_to_fmap_tupled (x,x1)

bt_to_fmap_lb

|- ∀cmp lb t.
     bt_to_fmap_lb cmp lb t =
     DRESTRICT (FMAPAL cmp t) {x | apto cmp lb x = LESS}

bt_to_fmap_ub

|- ∀cmp t ub.
     bt_to_fmap_ub cmp t ub =
     DRESTRICT (FMAPAL cmp t) {x | apto cmp x ub = LESS}

bt_to_fmap_lb_ub

|- ∀cmp lb t ub.
     bt_to_fmap_lb_ub cmp lb t ub =
     DRESTRICT (FMAPAL cmp t)
       {x | (apto cmp lb x = LESS) ∧ (apto cmp x ub = LESS)}

bt_map

|- (∀f. bt_map f nt = nt) ∧
   ∀f l x r. bt_map f (node l x r) = node (bt_map f l) (f x) (bt_map f r)

bt_to_orl_lb_ub_tupled_primitive

|- bt_to_orl_lb_ub_tupled =
   WFREC
     (@R.
        WF R ∧
        (∀y l ub r x lb cmp.
           apto cmp lb x ≠ LESS ⇒
           R (cmp,lb,r,ub) (cmp,lb,node l (x,y) r,ub)) ∧
        (∀r y l ub x lb cmp.
           (apto cmp lb x = LESS) ∧ apto cmp x ub ≠ LESS ⇒
           R (cmp,lb,l,ub) (cmp,lb,node l (x,y) r,ub)) ∧
        (∀r y l ub x lb cmp.
           (apto cmp lb x = LESS) ∧ (apto cmp x ub = LESS) ⇒
           R (cmp,lb,l,x) (cmp,lb,node l (x,y) r,ub)) ∧
        ∀y l r ub x lb cmp.
          (apto cmp lb x = LESS) ∧ (apto cmp x ub = LESS) ⇒
          R (cmp,x,r,ub) (cmp,lb,node l (x,y) r,ub))
     (λbt_to_orl_lb_ub_tupled a.
        case a of
          (cmp,lb,nt,ub) => I []
        | (cmp,lb,node l (x,y) r,ub) =>
            I
              (if apto cmp lb x = LESS then
                 if apto cmp x ub = LESS then
                   bt_to_orl_lb_ub_tupled (cmp,lb,l,x) ++ [(x,y)] ++
                   bt_to_orl_lb_ub_tupled (cmp,x,r,ub)
                 else bt_to_orl_lb_ub_tupled (cmp,lb,l,ub)
               else bt_to_orl_lb_ub_tupled (cmp,lb,r,ub)))

bt_to_orl_lb_ub_curried

|- ∀x x1 x2 x3.
     bt_to_orl_lb_ub x x1 x2 x3 = bt_to_orl_lb_ub_tupled (x,x1,x2,x3)

bt_to_orl_lb_tupled_primitive

|- bt_to_orl_lb_tupled =
   WFREC
     (@R.
        WF R ∧
        (∀y l r x lb cmp.
           apto cmp lb x ≠ LESS ⇒ R (cmp,lb,r) (cmp,lb,node l (x,y) r)) ∧
        ∀y l r x lb cmp.
          (apto cmp lb x = LESS) ⇒ R (cmp,x,r) (cmp,lb,node l (x,y) r))
     (λbt_to_orl_lb_tupled a.
        case a of
          (cmp,lb,nt) => I []
        | (cmp,lb,node l (x,y) r) =>
            I
              (if apto cmp lb x = LESS then
                 bt_to_orl_lb_ub cmp lb l x ++ [(x,y)] ++
                 bt_to_orl_lb_tupled (cmp,x,r)
               else bt_to_orl_lb_tupled (cmp,lb,r)))

bt_to_orl_lb_curried

|- ∀x x1 x2. bt_to_orl_lb x x1 x2 = bt_to_orl_lb_tupled (x,x1,x2)

bt_to_orl_ub_tupled_primitive

|- bt_to_orl_ub_tupled =
   WFREC
     (@R.
        WF R ∧
        (∀r y l ub x cmp.
           apto cmp x ub ≠ LESS ⇒ R (cmp,l,ub) (cmp,node l (x,y) r,ub)) ∧
        ∀r y l ub x cmp.
          (apto cmp x ub = LESS) ⇒ R (cmp,l,x) (cmp,node l (x,y) r,ub))
     (λbt_to_orl_ub_tupled a.
        case a of
          (cmp,nt,ub) => I []
        | (cmp,node l (x,y) r,ub) =>
            I
              (if apto cmp x ub = LESS then
                 bt_to_orl_ub_tupled (cmp,l,x) ++ [(x,y)] ++
                 bt_to_orl_lb_ub cmp x r ub
               else bt_to_orl_ub_tupled (cmp,l,ub)))

bt_to_orl_ub_curried

|- ∀x x1 x2. bt_to_orl_ub x x1 x2 = bt_to_orl_ub_tupled (x,x1,x2)

bt_to_orl_tupled_primitive

|- bt_to_orl_tupled =
   WFREC (@R. WF R)
     (λbt_to_orl_tupled a.
        case a of
          (cmp,nt) => I []
        | (cmp,node l (x,y) r) =>
            I (bt_to_orl_ub cmp l x ++ [(x,y)] ++ bt_to_orl_lb cmp x r))

bt_to_orl_curried

|- ∀x x1. bt_to_orl x x1 = bt_to_orl_tupled (x,x1)

fmap

|- ∀l. fmap l = FEMPTY |++ REVERSE l

bt_to_orl_lb_ub_ac_tupled_AUX

|- ∀R.
     bt_to_orl_lb_ub_ac_tupled_aux R =
     WFREC R
       (λbt_to_orl_lb_ub_ac_tupled a.
          case a of
            (cmp,lb,nt,ub,m) => I m
          | (cmp,lb,node l (x,y) r,ub,m) =>
              I
                (if apto cmp lb x = LESS then
                   if apto cmp x ub = LESS then
                     bt_to_orl_lb_ub_ac_tupled
                       (cmp,lb,l,x,
                        (x,y)::bt_to_orl_lb_ub_ac_tupled (cmp,x,r,ub,m))
                   else bt_to_orl_lb_ub_ac_tupled (cmp,lb,l,ub,m)
                 else bt_to_orl_lb_ub_ac_tupled (cmp,lb,r,ub,m)))

bt_to_orl_lb_ub_ac_tupled_primitive

|- bt_to_orl_lb_ub_ac_tupled =
   bt_to_orl_lb_ub_ac_tupled_aux
     (@R.
        WF R ∧
        (∀y l m ub r x lb cmp.
           apto cmp lb x ≠ LESS ⇒
           R (cmp,lb,r,ub,m) (cmp,lb,node l (x,y) r,ub,m)) ∧
        (∀r y m l ub x lb cmp.
           (apto cmp lb x = LESS) ∧ apto cmp x ub ≠ LESS ⇒
           R (cmp,lb,l,ub,m) (cmp,lb,node l (x,y) r,ub,m)) ∧
        (∀m r y l ub x lb cmp.
           (apto cmp lb x = LESS) ∧ (apto cmp x ub = LESS) ⇒
           R
             (cmp,lb,l,x,
              (x,y)::bt_to_orl_lb_ub_ac_tupled_aux R (cmp,x,r,ub,m))
             (cmp,lb,node l (x,y) r,ub,m)) ∧
        ∀y l m r ub x lb cmp.
          (apto cmp lb x = LESS) ∧ (apto cmp x ub = LESS) ⇒
          R (cmp,x,r,ub,m) (cmp,lb,node l (x,y) r,ub,m))

bt_to_orl_lb_ub_ac_curried

|- ∀x x1 x2 x3 x4.
     bt_to_orl_lb_ub_ac x x1 x2 x3 x4 =
     bt_to_orl_lb_ub_ac_tupled (x,x1,x2,x3,x4)

bt_to_orl_lb_ac_tupled_primitive

|- bt_to_orl_lb_ac_tupled =
   WFREC
     (@R.
        WF R ∧
        (∀y l m r x lb cmp.
           apto cmp lb x ≠ LESS ⇒ R (cmp,lb,r,m) (cmp,lb,node l (x,y) r,m)) ∧
        ∀y l m r x lb cmp.
          (apto cmp lb x = LESS) ⇒ R (cmp,x,r,m) (cmp,lb,node l (x,y) r,m))
     (λbt_to_orl_lb_ac_tupled a.
        case a of
          (cmp,lb,nt,m) => I m
        | (cmp,lb,node l (x,y) r,m) =>
            I
              (if apto cmp lb x = LESS then
                 bt_to_orl_lb_ub_ac cmp lb l x
                   ((x,y)::bt_to_orl_lb_ac_tupled (cmp,x,r,m))
               else bt_to_orl_lb_ac_tupled (cmp,lb,r,m)))

bt_to_orl_lb_ac_curried

|- ∀x x1 x2 x3.
     bt_to_orl_lb_ac x x1 x2 x3 = bt_to_orl_lb_ac_tupled (x,x1,x2,x3)

bt_to_orl_ub_ac_tupled_primitive

|- bt_to_orl_ub_ac_tupled =
   WFREC
     (@R.
        WF R ∧
        (∀r y m l ub x cmp.
           apto cmp x ub ≠ LESS ⇒ R (cmp,l,ub,m) (cmp,node l (x,y) r,ub,m)) ∧
        ∀m r y l ub x cmp.
          (apto cmp x ub = LESS) ⇒
          R (cmp,l,x,(x,y)::bt_to_orl_lb_ub_ac cmp x r ub m)
            (cmp,node l (x,y) r,ub,m))
     (λbt_to_orl_ub_ac_tupled a.
        case a of
          (cmp,nt,ub,m) => I m
        | (cmp,node l (x,y) r,ub,m) =>
            I
              (if apto cmp x ub = LESS then
                 bt_to_orl_ub_ac_tupled
                   (cmp,l,x,(x,y)::bt_to_orl_lb_ub_ac cmp x r ub m)
               else bt_to_orl_ub_ac_tupled (cmp,l,ub,m)))

bt_to_orl_ub_ac_curried

|- ∀x x1 x2 x3.
     bt_to_orl_ub_ac x x1 x2 x3 = bt_to_orl_ub_ac_tupled (x,x1,x2,x3)

bt_to_orl_ac_tupled_primitive

|- bt_to_orl_ac_tupled =
   WFREC (@R. WF R)
     (λbt_to_orl_ac_tupled a.
        case a of
          (cmp,nt,m) => I m
        | (cmp,node l (x,y) r,m) =>
            I (bt_to_orl_ub_ac cmp l x ((x,y)::bt_to_orl_lb_ac cmp x r m)))

bt_to_orl_ac_curried

|- ∀x x1 x2. bt_to_orl_ac x x1 x2 = bt_to_orl_ac_tupled (x,x1,x2)

ORWL

|- ∀cmp f l. ORWL cmp f l ⇔ (f = fmap l) ∧ ORL cmp l

OFU

|- ∀cmp f g. OFU cmp f g = DRESTRICT f {x | LESS_ALL cmp x (FDOM g)} ⊌ g

UFO

|- ∀cmp f g.
     UFO cmp f g =
     f ⊌ DRESTRICT g {y | ∀z. z ∈ FDOM f ⇒ (apto cmp z y = LESS)}

bl_to_fmap_tupled_primitive

|- bl_to_fmap_tupled =
   WFREC
     (@R.
        WF R ∧ (∀b cmp. R (cmp,b) (cmp,zerbl b)) ∧
        ∀t y x b cmp. R (cmp,b) (cmp,onebl (x,y) t b))
     (λbl_to_fmap_tupled a.
        case a of
          (cmp,nbl) => I FEMPTY
        | (cmp,zerbl b) => I (bl_to_fmap_tupled (cmp,b))
        | (cmp,onebl (x,y) t b') =>
            I
              (OFU cmp
                 (FEMPTY |+ (x,y) ⊌
                  DRESTRICT (FMAPAL cmp t) {z | apto cmp x z = LESS})
                 (bl_to_fmap_tupled (cmp,b'))))

bl_to_fmap_curried

|- ∀x x1. bl_to_fmap x x1 = bl_to_fmap_tupled (x,x1)

inter_merge_tupled_primitive

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

inter_merge_curried

|- ∀x x1 x2. inter_merge x x1 x2 = inter_merge_tupled (x,x1,x2)

diff_merge_tupled_primitive

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

diff_merge_curried

|- ∀x x1 x2. diff_merge x x1 x2 = diff_merge_tupled (x,x1,x2)

AP_SND

|- ∀f a b. AP_SND f (a,b) = (a,f b)

ORL_bt_lb_ub_tupled_primitive

|- ORL_bt_lb_ub_tupled =
   WFREC
     (@R.
        WF R ∧
        (∀ub r y x l lb cmp. R (cmp,lb,l,x) (cmp,lb,node l (x,y) r,ub)) ∧
        ∀y l lb ub r x cmp. R (cmp,x,r,ub) (cmp,lb,node l (x,y) r,ub))
     (λORL_bt_lb_ub_tupled a.
        case a of
          (cmp,lb,nt,ub) => I (apto cmp lb ub = LESS)
        | (cmp,lb,node l (x,y) r,ub) =>
            I
              (ORL_bt_lb_ub_tupled (cmp,lb,l,x) ∧
               ORL_bt_lb_ub_tupled (cmp,x,r,ub)))

ORL_bt_lb_ub_curried

|- ∀x x1 x2 x3. ORL_bt_lb_ub x x1 x2 x3 ⇔ ORL_bt_lb_ub_tupled (x,x1,x2,x3)

ORL_bt_lb_tupled_primitive

|- ORL_bt_lb_tupled =
   WFREC (@R. WF R ∧ ∀y l lb r x cmp. R (cmp,x,r) (cmp,lb,node l (x,y) r))
     (λORL_bt_lb_tupled a.
        case a of
          (cmp,lb,nt) => I T
        | (cmp,lb,node l (x,y) r) =>
            I (ORL_bt_lb_ub cmp lb l x ∧ ORL_bt_lb_tupled (cmp,x,r)))

ORL_bt_lb_curried

|- ∀x x1 x2. ORL_bt_lb x x1 x2 ⇔ ORL_bt_lb_tupled (x,x1,x2)

ORL_bt_ub_tupled_primitive

|- ORL_bt_ub_tupled =
   WFREC (@R. WF R ∧ ∀ub r y x l cmp. R (cmp,l,x) (cmp,node l (x,y) r,ub))
     (λORL_bt_ub_tupled a.
        case a of
          (cmp,nt,ub) => I T
        | (cmp,node l (x,y) r,ub) =>
            I (ORL_bt_ub_tupled (cmp,l,x) ∧ ORL_bt_lb_ub cmp x r ub))

ORL_bt_ub_curried

|- ∀x x1 x2. ORL_bt_ub x x1 x2 ⇔ ORL_bt_ub_tupled (x,x1,x2)

ORL_bt_tupled_primitive

|- ORL_bt_tupled =
   WFREC (@R. WF R)
     (λORL_bt_tupled a.
        case a of
          (cmp,nt) => I T
        | (cmp,node l (x,y) r) => I (ORL_bt_ub cmp l x ∧ ORL_bt_lb cmp x r))

ORL_bt_curried

|- ∀x x1. ORL_bt x x1 ⇔ ORL_bt_tupled (x,x1)

list_rplacv_cn_tupled_primitive

|- list_rplacv_cn_tupled =
   WFREC
     (@R.
        WF R ∧
        ∀z cn l y w x.
          x ≠ w ⇒ R ((x,y),l,(λm. cn ((w,z)::m))) ((x,y),(w,z)::l,cn))
     (λlist_rplacv_cn_tupled a.
        case a of
          ((x,y),[],cn) => I []
        | ((x,y),(w,z)::l,cn) =>
            I
              (if x = w then cn ((x,y)::l)
               else list_rplacv_cn_tupled ((x,y),l,(λm. cn ((w,z)::m)))))

list_rplacv_cn_curried

|- ∀x x1 x2. list_rplacv_cn x x1 x2 = list_rplacv_cn_tupled (x,x1,x2)

bt_rplacv_cn_tupled_primitive

|- bt_rplacv_cn_tupled =
   WFREC
     (@R.
        WF R ∧
        (∀z l cn r y w x cmp.
           (apto cmp x w = GREATER) ⇒
           R (cmp,(x,y),r,(λm. cn (node l (w,z) m)))
             (cmp,(x,y),node l (w,z) r,cn)) ∧
        ∀r z cn l y w x cmp.
          (apto cmp x w = LESS) ⇒
          R (cmp,(x,y),l,(λm. cn (node m (w,z) r)))
            (cmp,(x,y),node l (w,z) r,cn))
     (λbt_rplacv_cn_tupled a.
        case a of
          (cmp,(x,y),nt,cn) => I nt
        | (cmp,(x,y),node l (w,z) r,cn) =>
            I
              (case apto cmp x w of
                 LESS =>
                   bt_rplacv_cn_tupled (cmp,(x,y),l,(λm. cn (node m (w,z) r)))
               | EQUAL => cn (node l (x,y) r)
               | GREATER =>
                   bt_rplacv_cn_tupled
                     (cmp,(x,y),r,(λm. cn (node l (w,z) m)))))

bt_rplacv_cn_curried

|- ∀x x1 x2 x3. bt_rplacv_cn x x1 x2 x3 = bt_rplacv_cn_tupled (x,x1,x2,x3)

Theorems

ORL_ind

|- ∀P.
     (∀cmp. P cmp []) ∧ (∀cmp a b l. P cmp l ⇒ P cmp ((a,b)::l)) ⇒
     ∀v v1. P v v1

ORL

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

optry_list_ind

|- ∀P.
     (∀f. P f []) ∧ (∀f l. P f l ⇒ P f (NONE::l)) ∧
     (∀f z l. P f l ⇒ P f (SOME z::l)) ⇒
     ∀v v1. P v v1

optry_list

|- (∀f. optry_list f [] = NONE) ∧
   (∀l f. optry_list f (NONE::l) = optry_list f l) ∧
   ∀z l f. optry_list f (SOME z::l) = optry (f z) (optry_list f l)

assocv_ind

|- ∀P.
     (∀a. P [] a) ∧ (∀x y l a. (a ≠ x ⇒ P l a) ⇒ P ((x,y)::l) a) ⇒
     ∀v v1. P v v1

assocv

|- (∀a. assocv [] a = NONE) ∧
   ∀y x l a. assocv ((x,y)::l) a = if a = x then SOME y else assocv l a

merge_ind

|- ∀P.
     (∀cmp l. P cmp [] l) ∧ (∀cmp v4 v5. P cmp (v4::v5) []) ∧
     (∀cmp a1 b1 l1 a2 b2 l2.
        ((apto cmp a1 a2 = EQUAL) ⇒ P cmp l1 l2) ∧
        ((apto cmp a1 a2 = GREATER) ⇒ P cmp ((a1,b1)::l1) l2) ∧
        ((apto cmp a1 a2 = LESS) ⇒ P cmp l1 ((a2,b2)::l2)) ⇒
        P cmp ((a1,b1)::l1) ((a2,b2)::l2)) ⇒
     ∀v v1 v2. P v v1 v2

merge

|- (∀l cmp. merge cmp [] l = l) ∧
   (∀v5 v4 cmp. merge cmp (v4::v5) [] = v4::v5) ∧
   ∀l2 l1 cmp b2 b1 a2 a1.
     merge cmp ((a1,b1)::l1) ((a2,b2)::l2) =
     case apto cmp a1 a2 of
       LESS => (a1,b1)::merge cmp l1 ((a2,b2)::l2)
     | EQUAL => (a1,b1)::merge cmp l1 l2
     | GREATER => (a2,b2)::merge cmp ((a1,b1)::l1) l2

incr_merge_ind

|- ∀P.
     (∀cmp l. P cmp l []) ∧ (∀cmp l lol. P cmp l (NONE::lol)) ∧
     (∀cmp l m lol. P cmp (merge cmp l m) lol ⇒ P cmp l (SOME m::lol)) ⇒
     ∀v v1 v2. P v v1 v2

incr_merge

|- (∀l cmp. incr_merge cmp l [] = [SOME l]) ∧
   (∀lol l cmp. incr_merge cmp l (NONE::lol) = SOME l::lol) ∧
   ∀m lol l cmp.
     incr_merge cmp l (SOME m::lol) = NONE::incr_merge cmp (merge cmp l m) lol

ORL_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

ORL_sublists

|- (∀cmp. ORL_sublists cmp [] ⇔ T) ∧
   (∀lol cmp. ORL_sublists cmp (NONE::lol) ⇔ ORL_sublists cmp lol) ∧
   ∀m lol cmp.
     ORL_sublists cmp (SOME m::lol) ⇔ ORL cmp m ∧ ORL_sublists cmp lol

merge_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 (merge cmp l m) lol ⇒ P cmp l (SOME m::lol)) ⇒
     ∀v v1 v2. P v v1 v2

merge_out

|- (∀l cmp. merge_out cmp l [] = l) ∧
   (∀lol l cmp. merge_out cmp l (NONE::lol) = merge_out cmp l lol) ∧
   ∀m lol l cmp.
     merge_out cmp l (SOME m::lol) = merge_out cmp (merge cmp l m) lol

OPTION_FLAT_ind

|- ∀P. P [] ∧ (∀l. P l ⇒ P (NONE::l)) ∧ (∀a l. P l ⇒ P (SOME a::l)) ⇒ ∀v. P v

OPTION_FLAT

|- (OPTION_FLAT [] = []) ∧ (∀l. OPTION_FLAT (NONE::l) = OPTION_FLAT l) ∧
   ∀l a. OPTION_FLAT (SOME a::l) = a ++ OPTION_FLAT l

bt_to_fmap_ind

|- ∀P.
     (∀cmp. P cmp nt) ∧
     (∀cmp l x v r. P cmp l ∧ P cmp r ⇒ P cmp (node l (x,v) r)) ⇒
     ∀v v1. P v v1

bt_to_fmap

|- (∀cmp. FMAPAL cmp nt = FEMPTY) ∧
   ∀x v r l cmp.
     FMAPAL cmp (node l (x,v) r) =
     DRESTRICT (FMAPAL cmp l) {y | apto cmp y x = LESS} ⊌ FEMPTY |+ (x,v) ⊌
     DRESTRICT (FMAPAL cmp r) {z | apto cmp x z = LESS}

FAPPLY_nt

|- ∀cmp x. FMAPAL cmp nt ' x = FEMPTY ' x

FAPPLY_node

|- ∀cmp x l a b r.
     FMAPAL cmp (node l (a,b) r) ' x =
     case apto cmp x a of
       LESS => FMAPAL cmp l ' x
     | EQUAL => b
     | GREATER => FMAPAL cmp r ' x

bt_FST_FDOM

|- ∀cmp t. FDOM (FMAPAL cmp t) = ENUMERAL cmp (bt_map FST t)

bt_to_orl_lb_ub_ind

|- ∀P.
     (∀cmp lb ub. P cmp lb nt ub) ∧
     (∀cmp lb l x y r ub.
        (apto cmp lb x ≠ LESS ⇒ P cmp lb r ub) ∧
        ((apto cmp lb x = LESS) ∧ apto cmp x ub ≠ LESS ⇒ P cmp lb l ub) ∧
        ((apto cmp lb x = LESS) ∧ (apto cmp x ub = LESS) ⇒ P cmp lb l x) ∧
        ((apto cmp lb x = LESS) ∧ (apto cmp x ub = LESS) ⇒ P cmp x r ub) ⇒
        P cmp lb (node l (x,y) r) ub) ⇒
     ∀v v1 v2 v3. P v v1 v2 v3

bt_to_orl_lb_ub

|- (∀ub lb cmp. bt_to_orl_lb_ub cmp lb nt ub = []) ∧
   ∀y x ub r lb l cmp.
     bt_to_orl_lb_ub cmp lb (node l (x,y) r) ub =
     if apto cmp lb x = LESS then
       if apto cmp x ub = LESS then
         bt_to_orl_lb_ub cmp lb l x ++ [(x,y)] ++ bt_to_orl_lb_ub cmp x r ub
       else bt_to_orl_lb_ub cmp lb l ub
     else bt_to_orl_lb_ub cmp lb r ub

bt_to_orl_lb_ind

|- ∀P.
     (∀cmp lb. P cmp lb nt) ∧
     (∀cmp lb l x y r.
        (apto cmp lb x ≠ LESS ⇒ P cmp lb r) ∧
        ((apto cmp lb x = LESS) ⇒ P cmp x r) ⇒
        P cmp lb (node l (x,y) r)) ⇒
     ∀v v1 v2. P v v1 v2

bt_to_orl_lb

|- (∀lb cmp. bt_to_orl_lb cmp lb nt = []) ∧
   ∀y x r lb l cmp.
     bt_to_orl_lb cmp lb (node l (x,y) r) =
     if apto cmp lb x = LESS then
       bt_to_orl_lb_ub cmp lb l x ++ [(x,y)] ++ bt_to_orl_lb cmp x r
     else bt_to_orl_lb cmp lb r

bt_to_orl_ub_ind

|- ∀P.
     (∀cmp ub. P cmp nt ub) ∧
     (∀cmp l x y r ub.
        (apto cmp x ub ≠ LESS ⇒ P cmp l ub) ∧
        ((apto cmp x ub = LESS) ⇒ P cmp l x) ⇒
        P cmp (node l (x,y) r) ub) ⇒
     ∀v v1 v2. P v v1 v2

bt_to_orl_ub

|- (∀ub cmp. bt_to_orl_ub cmp nt ub = []) ∧
   ∀y x ub r l cmp.
     bt_to_orl_ub cmp (node l (x,y) r) ub =
     if apto cmp x ub = LESS then
       bt_to_orl_ub cmp l x ++ [(x,y)] ++ bt_to_orl_lb_ub cmp x r ub
     else bt_to_orl_ub cmp l ub

bt_to_orl_ind

|- ∀P.
     (∀cmp. P cmp nt) ∧ (∀cmp l x y r. P cmp (node l (x,y) r)) ⇒ ∀v v1. P v v1

bt_to_orl

|- (bt_to_orl cmp nt = []) ∧
   (bt_to_orl cmp (node l (x,y) r) =
    bt_to_orl_ub cmp l x ++ [(x,y)] ++ bt_to_orl_lb cmp x r)

bt_to_orl_lb_ub_ac_ind

|- ∀P.
     (∀cmp lb ub m. P cmp lb nt ub m) ∧
     (∀cmp lb l x y r ub m.
        (apto cmp lb x ≠ LESS ⇒ P cmp lb r ub m) ∧
        ((apto cmp lb x = LESS) ∧ apto cmp x ub ≠ LESS ⇒ P cmp lb l ub m) ∧
        ((apto cmp lb x = LESS) ∧ (apto cmp x ub = LESS) ⇒
         P cmp lb l x ((x,y)::bt_to_orl_lb_ub_ac cmp x r ub m)) ∧
        ((apto cmp lb x = LESS) ∧ (apto cmp x ub = LESS) ⇒ P cmp x r ub m) ⇒
        P cmp lb (node l (x,y) r) ub m) ⇒
     ∀v v1 v2 v3 v4. P v v1 v2 v3 v4

bt_to_orl_lb_ub_ac

|- (∀ub m lb cmp. bt_to_orl_lb_ub_ac cmp lb nt ub m = m) ∧
   ∀y x ub r m lb l cmp.
     bt_to_orl_lb_ub_ac cmp lb (node l (x,y) r) ub m =
     if apto cmp lb x = LESS then
       if apto cmp x ub = LESS then
         bt_to_orl_lb_ub_ac cmp lb l x
           ((x,y)::bt_to_orl_lb_ub_ac cmp x r ub m)
       else bt_to_orl_lb_ub_ac cmp lb l ub m
     else bt_to_orl_lb_ub_ac cmp lb r ub m

bt_to_orl_lb_ac_ind

|- ∀P.
     (∀cmp lb m. P cmp lb nt m) ∧
     (∀cmp lb l x y r m.
        (apto cmp lb x ≠ LESS ⇒ P cmp lb r m) ∧
        ((apto cmp lb x = LESS) ⇒ P cmp x r m) ⇒
        P cmp lb (node l (x,y) r) m) ⇒
     ∀v v1 v2 v3. P v v1 v2 v3

bt_to_orl_lb_ac

|- (∀m lb cmp. bt_to_orl_lb_ac cmp lb nt m = m) ∧
   ∀y x r m lb l cmp.
     bt_to_orl_lb_ac cmp lb (node l (x,y) r) m =
     if apto cmp lb x = LESS then
       bt_to_orl_lb_ub_ac cmp lb l x ((x,y)::bt_to_orl_lb_ac cmp x r m)
     else bt_to_orl_lb_ac cmp lb r m

bt_to_orl_ub_ac_ind

|- ∀P.
     (∀cmp ub m. P cmp nt ub m) ∧
     (∀cmp l x y r ub m.
        (apto cmp x ub ≠ LESS ⇒ P cmp l ub m) ∧
        ((apto cmp x ub = LESS) ⇒
         P cmp l x ((x,y)::bt_to_orl_lb_ub_ac cmp x r ub m)) ⇒
        P cmp (node l (x,y) r) ub m) ⇒
     ∀v v1 v2 v3. P v v1 v2 v3

bt_to_orl_ub_ac

|- (∀ub m cmp. bt_to_orl_ub_ac cmp nt ub m = m) ∧
   ∀y x ub r m l cmp.
     bt_to_orl_ub_ac cmp (node l (x,y) r) ub m =
     if apto cmp x ub = LESS then
       bt_to_orl_ub_ac cmp l x ((x,y)::bt_to_orl_lb_ub_ac cmp x r ub m)
     else bt_to_orl_ub_ac cmp l ub m

bt_to_orl_ac_ind

|- ∀P.
     (∀cmp m. P cmp nt m) ∧ (∀cmp l x y r m. P cmp (node l (x,y) r) m) ⇒
     ∀v v1 v2. P v v1 v2

bt_to_orl_ac

|- (bt_to_orl_ac cmp nt m = m) ∧
   (bt_to_orl_ac cmp (node l (x,y) r) m =
    bt_to_orl_ub_ac cmp l x ((x,y)::bt_to_orl_lb_ac cmp x r m))

ORWL_bt_to_orl

|- ∀cmp t. ORWL cmp (FMAPAL cmp t) (bt_to_orl cmp t)

bl_to_fmap_ind

|- ∀P.
     (∀cmp. P cmp nbl) ∧ (∀cmp b. P cmp b ⇒ P cmp (zerbl b)) ∧
     (∀cmp x y t b. P cmp b ⇒ P cmp (onebl (x,y) t b)) ⇒
     ∀v v1. P v v1

bl_to_fmap

|- (∀cmp. bl_to_fmap cmp nbl = FEMPTY) ∧
   (∀cmp b. bl_to_fmap cmp (zerbl b) = bl_to_fmap cmp b) ∧
   ∀y x t cmp b.
     bl_to_fmap cmp (onebl (x,y) t b) =
     OFU cmp
       (FEMPTY |+ (x,y) ⊌ DRESTRICT (FMAPAL cmp t) {z | apto cmp x z = LESS})
       (bl_to_fmap cmp b)

bt_to_orl_ID_IMP

|- ∀cmp l. ORL cmp l ⇒ (bt_to_orl cmp (list_to_bt l) = l)

fmap_FDOM

|- ∀l. FDOM (fmap l) = LIST_TO_SET (MAP FST l)

ORL_FUNION_IMP

|- ∀cmp l.
     ORL cmp l ⇒
     ∀m.
       ORL cmp m ⇒
       ORL cmp (merge cmp l m) ∧ (fmap (merge cmp l m) = fmap l ⊌ fmap m)

FMAPAL_FDOM_THM

|- (∀cmp x. x ∈ FDOM (FMAPAL cmp nt) ⇔ F) ∧
   ∀cmp x a b l r.
     x ∈ FDOM (FMAPAL cmp (node l (a,b) r)) ⇔
     case apto cmp x a of
       LESS => x ∈ FDOM (FMAPAL cmp l)
     | EQUAL => T
     | GREATER => x ∈ FDOM (FMAPAL cmp r)

inter_merge_ind

|- ∀P.
     (∀cmp. P cmp [] []) ∧ (∀cmp a b l. P cmp ((a,b)::l) []) ∧
     (∀cmp y m. P cmp [] (y::m)) ∧
     (∀cmp a b l y m.
        ((apto cmp a y = EQUAL) ⇒ P cmp l m) ∧
        ((apto cmp a y = GREATER) ⇒ P cmp ((a,b)::l) m) ∧
        ((apto cmp a y = LESS) ⇒ P cmp l (y::m)) ⇒
        P cmp ((a,b)::l) (y::m)) ⇒
     ∀v v1 v2. P v v1 v2

inter_merge

|- (∀cmp. inter_merge cmp [] [] = []) ∧
   (∀l cmp b a. inter_merge cmp ((a,b)::l) [] = []) ∧
   (∀y m cmp. inter_merge cmp [] (y::m) = []) ∧
   ∀y m l cmp b a.
     inter_merge cmp ((a,b)::l) (y::m) =
     case apto cmp a y of
       LESS => inter_merge cmp l (y::m)
     | EQUAL => (a,b)::inter_merge cmp l m
     | GREATER => inter_merge cmp ((a,b)::l) m

ORL_DRESTRICT_IMP

|- ∀cmp l.
     ORL cmp l ⇒
     ∀m.
       OL cmp m ⇒
       ORL cmp (inter_merge cmp l m) ∧
       (fmap (inter_merge cmp l m) = DRESTRICT (fmap l) (LIST_TO_SET m))

diff_merge_ind

|- ∀P.
     (∀cmp. P cmp [] []) ∧ (∀cmp a b l. P cmp ((a,b)::l) []) ∧
     (∀cmp y m. P cmp [] (y::m)) ∧
     (∀cmp a b l y m.
        ((apto cmp a y = EQUAL) ⇒ P cmp l m) ∧
        ((apto cmp a y = GREATER) ⇒ P cmp ((a,b)::l) m) ∧
        ((apto cmp a y = LESS) ⇒ P cmp l (y::m)) ⇒
        P cmp ((a,b)::l) (y::m)) ⇒
     ∀v v1 v2. P v v1 v2

diff_merge

|- (∀cmp. diff_merge cmp [] [] = []) ∧
   (∀l cmp b a. diff_merge cmp ((a,b)::l) [] = (a,b)::l) ∧
   (∀y m cmp. diff_merge cmp [] (y::m) = []) ∧
   ∀y m l cmp b a.
     diff_merge cmp ((a,b)::l) (y::m) =
     case apto cmp a y of
       LESS => (a,b)::diff_merge cmp l (y::m)
     | EQUAL => diff_merge cmp l m
     | GREATER => diff_merge cmp ((a,b)::l) m

ORL_DRESTRICT_COMPL_IMP

|- ∀cmp l.
     ORL cmp l ⇒
     ∀m.
       OL cmp m ⇒
       ORL cmp (diff_merge cmp l m) ∧
       (fmap (diff_merge cmp l m) =
        DRESTRICT (fmap l) (COMPL (LIST_TO_SET m)))

FMAPAL_fmap

|- ∀cmp l. fmap l = FMAPAL cmp (list_to_bt (incr_sort cmp l))

ORL_FMAPAL

|- ∀cmp l. ORL cmp l ⇒ (fmap l = FMAPAL cmp (list_to_bt l))

ORWL_FUNION_THM

|- ∀cmp s l t m.
     ORWL cmp s l ∧ ORWL cmp t m ⇒ ORWL cmp (s ⊌ t) (merge cmp l m)

ORWL_DRESTRICT_THM

|- ∀cmp s l t m.
     ORWL cmp s l ∧ OWL cmp t m ⇒
     ORWL cmp (DRESTRICT s t) (inter_merge cmp l m)

ORWL_DRESTRICT_COMPL_THM

|- ∀cmp s l t m.
     ORWL cmp s l ∧ OWL cmp t m ⇒
     ORWL cmp (DRESTRICT s (COMPL t)) (diff_merge cmp l m)

o_f_bt_map

|- ∀cmp f t. f o_f FMAPAL cmp t = FMAPAL cmp (bt_map (AP_SND f) t)

FAPPLY_fmap_NIL

|- ∀x. fmap [] ' x = FEMPTY ' x

FAPPLY_fmap_CONS

|- ∀x y z l. fmap ((y,z)::l) ' x = if x = y then z else fmap l ' x

o_f_fmap

|- ∀f l. f o_f fmap l = fmap (MAP (AP_SND f) l)

ORL_bt_lb_ub_ind

|- ∀P.
     (∀cmp lb ub. P cmp lb nt ub) ∧
     (∀cmp lb l x y r ub.
        P cmp lb l x ∧ P cmp x r ub ⇒ P cmp lb (node l (x,y) r) ub) ⇒
     ∀v v1 v2 v3. P v v1 v2 v3

ORL_bt_lb_ub

|- (∀ub lb cmp. ORL_bt_lb_ub cmp lb nt ub ⇔ (apto cmp lb ub = LESS)) ∧
   ∀y x ub r lb l cmp.
     ORL_bt_lb_ub cmp lb (node l (x,y) r) ub ⇔
     ORL_bt_lb_ub cmp lb l x ∧ ORL_bt_lb_ub cmp x r ub

ORL_bt_lb_ind

|- ∀P.
     (∀cmp lb. P cmp lb nt) ∧
     (∀cmp lb l x y r. P cmp x r ⇒ P cmp lb (node l (x,y) r)) ⇒
     ∀v v1 v2. P v v1 v2

ORL_bt_lb

|- (∀lb cmp. ORL_bt_lb cmp lb nt ⇔ T) ∧
   ∀y x r lb l cmp.
     ORL_bt_lb cmp lb (node l (x,y) r) ⇔
     ORL_bt_lb_ub cmp lb l x ∧ ORL_bt_lb cmp x r

ORL_bt_ub_ind

|- ∀P.
     (∀cmp ub. P cmp nt ub) ∧
     (∀cmp l x y r ub. P cmp l x ⇒ P cmp (node l (x,y) r) ub) ⇒
     ∀v v1 v2. P v v1 v2

ORL_bt_ub

|- (∀ub cmp. ORL_bt_ub cmp nt ub ⇔ T) ∧
   ∀y x ub r l cmp.
     ORL_bt_ub cmp (node l (x,y) r) ub ⇔
     ORL_bt_ub cmp l x ∧ ORL_bt_lb_ub cmp x r ub

ORL_bt_ind

|- ∀P.
     (∀cmp. P cmp nt) ∧ (∀cmp l x y r. P cmp (node l (x,y) r)) ⇒ ∀v v1. P v v1

ORL_bt

|- (ORL_bt cmp nt ⇔ T) ∧
   (ORL_bt cmp (node l (x,y) r) ⇔ ORL_bt_ub cmp l x ∧ ORL_bt_lb cmp x r)

better_bt_to_orl

|- ∀cmp t.
     bt_to_orl cmp t =
     if ORL_bt cmp t then bt_to_list_ac t [] else bt_to_orl_ac cmp t []

list_rplacv_cn_ind

|- ∀P.
     (∀x y cn. P (x,y) [] cn) ∧
     (∀x y w z l cn.
        (x ≠ w ⇒ P (x,y) l (λm. cn ((w,z)::m))) ⇒ P (x,y) ((w,z)::l) cn) ⇒
     ∀v v1 v2 v3. P (v,v1) v2 v3

list_rplacv_cn

|- (∀y x cn. list_rplacv_cn (x,y) [] cn = []) ∧
   ∀z y x w l cn.
     list_rplacv_cn (x,y) ((w,z)::l) cn =
     if x = w then cn ((x,y)::l)
     else list_rplacv_cn (x,y) l (λm. cn ((w,z)::m))

fmap_FDOM_rec

|- (∀x. x ∈ FDOM (fmap []) ⇔ F) ∧
   ∀x w z l. x ∈ FDOM (fmap ((w,z)::l)) ⇔ (x = w) ∨ x ∈ FDOM (fmap l)

list_rplacv_thm

|- ∀x y l.
     (let ans = list_rplacv_cn (x,y) l (λm. m)
      in
        if ans = [] then x ∉ FDOM (fmap l)
        else x ∈ FDOM (fmap l) ∧ (fmap l |+ (x,y) = fmap ans))

bt_rplacv_cn_ind

|- ∀P.
     (∀cmp x y cn. P cmp (x,y) nt cn) ∧
     (∀cmp x y l w z r cn.
        ((apto cmp x w = GREATER) ⇒ P cmp (x,y) r (λm. cn (node l (w,z) m))) ∧
        ((apto cmp x w = LESS) ⇒ P cmp (x,y) l (λm. cn (node m (w,z) r))) ⇒
        P cmp (x,y) (node l (w,z) r) cn) ⇒
     ∀v v1 v2 v3 v4. P v (v1,v2) v3 v4

bt_rplacv_cn

|- (∀y x cn cmp. bt_rplacv_cn cmp (x,y) nt cn = nt) ∧
   ∀z y x w r l cn cmp.
     bt_rplacv_cn cmp (x,y) (node l (w,z) r) cn =
     case apto cmp x w of
       LESS => bt_rplacv_cn cmp (x,y) l (λm. cn (node m (w,z) r))
     | EQUAL => cn (node l (x,y) r)
     | GREATER => bt_rplacv_cn cmp (x,y) r (λm. cn (node l (w,z) m))

bt_rplacv_thm

|- ∀cmp x y t.
     (let ans = bt_rplacv_cn cmp (x,y) t (λm. m)
      in
        if ans = nt then x ∉ FDOM (FMAPAL cmp t)
        else
          x ∈ FDOM (FMAPAL cmp t) ∧ (FMAPAL cmp t |+ (x,y) = FMAPAL cmp ans))

FUN_fmap_thm

|- ∀f l. fmap (MAP (λx. (x,f x)) l) = FUN_FMAP f (LIST_TO_SET l)

fmap_ORWL_thm

|- ∀cmp l. ORWL cmp (fmap l) (incr_sort cmp l)