Theory "fmapal"

Signature

Definitions

optry

⊢ (∀p q. optry (SOME p) q = SOME p) ∧ ∀q. optry NONE q = q

vcossa

⊢ ∀a l. vcossa a l = assocv l a

OPTION_UPDATE

⊢ ∀f g x. OPTION_UPDATE f g x = optry (f x) (g x)

incr_build

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

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 ∘ f) (IS_SOME ∘ f)

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)

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

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)} FUNION g

UFO

⊢ ∀cmp f g.
      UFO cmp f g =
      f FUNION DRESTRICT g {y | ∀z. z ∈ FDOM f ⇒ apto cmp z y = Less}

AP_SND

⊢ ∀f a b. AP_SND f (a,b) = (a,f b)

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} FUNION
      FEMPTY |+ (x,v) FUNION
      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) FUNION
         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 FUNION 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 FUNION 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)