Theory sptree

⊢ (∀k. isEmpty (delete k LN)) ∧
  (∀k a. delete k ⦕ 0 ↦ a ⦖ = if k = 0 then LN else ⦕ 0 ↦ a ⦖) ∧
  (∀k t1 t2.
     delete k (BN t1 t2) =
     if k = 0 then BN t1 t2
     else if EVEN k then mk_BN (delete ((k − 1) DIV 2) t1) t2
     else mk_BN t1 (delete ((k − 1) DIV 2) t2)) ∧
  ∀k t1 a t2.
    delete k (BS t1 a t2) =
    if k = 0 then BN t1 t2
    else if EVEN k then mk_BS (delete ((k − 1) DIV 2) t1) a t2
    else mk_BS t1 a (delete ((k − 1) DIV 2) t2)

⊢ (∀t. isEmpty (difference LN t)) ∧
  (∀a t.
     difference ⦕ 0 ↦ a ⦖ t =
     case t of
       LN => ⦕ 0 ↦ a ⦖
     | ⦕ 0 ↦ b ⦖ => LN
     | BN t1 t2 => ⦕ 0 ↦ a ⦖
     | BS t1' b' t2' => LN) ∧
  (∀t1 t2 t.
     difference (BN t1 t2) t =
     case t of
       LN => BN t1 t2
     | ⦕ 0 ↦ a ⦖ => BN t1 t2
     | BN t1' t2' => mk_BN (difference t1 t1') (difference t2 t2')
     | BS t1'' a'' t2'' => mk_BN (difference t1 t1'') (difference t2 t2'')) ∧
  ∀t1 a t2 t.
    difference (BS t1 a t2) t =
    case t of
      LN => BS t1 a t2
    | ⦕ 0 ↦ a' ⦖ => BN t1 t2
    | BN t1' t2' => mk_BS (difference t1 t1') a (difference t2 t2')
    | BS t1'' a'³' t2'' => mk_BN (difference t1 t1'') (difference t2 t2'')

⊢ domain LN = ∅ ∧ (∀v0. domain ⦕ 0 ↦ v0 ⦖ = {0}) ∧
  (∀t1 t2.
     domain (BN t1 t2) =
     IMAGE (λn. 2 * n + 2) (domain t1) ∪ IMAGE (λn. 2 * n + 1) (domain t2)) ∧
  ∀t1 v1 t2.
    domain (BS t1 v1 t2) =
    {0} ∪ IMAGE (λn. 2 * n + 2) (domain t1) ∪
    IMAGE (λn. 2 * n + 1) (domain t2)

⊢ (∀f. isEmpty (filter_v f LN)) ∧
  (∀f x. filter_v f ⦕ 0 ↦ x ⦖ = if f x then ⦕ 0 ↦ x ⦖ else LN) ∧
  (∀f l r. filter_v f (BN l r) = mk_BN (filter_v f l) (filter_v f r)) ∧
  ∀f l x r.
    filter_v f (BS l x r) =
    if f x then mk_BS (filter_v f l) x (filter_v f r)
    else mk_BN (filter_v f l) (filter_v f r)

⊢ (∀f i acc. foldi f i acc LN = acc) ∧
  (∀f i acc a. foldi f i acc ⦕ 0 ↦ a ⦖ = f i a acc) ∧
  (∀f i acc t1 t2.
     foldi f i acc (BN t1 t2) =
     (let
        inc = sptree$lrnext i
      in
        foldi f (i + inc) (foldi f (i + 2 * inc) acc t1) t2)) ∧
  ∀f i acc t1 a t2.
    foldi f i acc (BS t1 a t2) =
    (let
       inc = sptree$lrnext i
     in
       foldi f (i + inc) (f i a (foldi f (i + 2 * inc) acc t1)) t2)

⊢ fromAList =
  WFREC (@R. WF R ∧ ∀y x xs. R xs ((x,y)::xs))
    (λfromAList a.
         case a of [] => I LN | (x,y)::xs => I (insert x y (fromAList xs)))

⊢ ∀l. fromList l = SND (FOLDL (λ(i,t) a. (i + 1,insert i a t)) (0,LN) l)

⊢ gather_inclist_offsets =
  WFREC (@R. WF R ∧ ∀x inc xs. R xs ((inc,x)::xs))
    (λgather_inclist_offsets a.
         case a of
           [] => I []
         | (inc,x)::xs =>
           I ((0,x)::MAP ($+ inc ## I) (gather_inclist_offsets xs)))

⊢ (∀t. isEmpty (inter LN t)) ∧
  (∀a t.
     inter ⦕ 0 ↦ a ⦖ t =
     case t of
       LN => LN
     | ⦕ 0 ↦ b ⦖ => ⦕ 0 ↦ a ⦖
     | BN t1 t2 => LN
     | BS t1' v4 t2' => ⦕ 0 ↦ a ⦖) ∧
  (∀t1 t2 t.
     inter (BN t1 t2) t =
     case t of
       LN => LN
     | ⦕ 0 ↦ a ⦖ => LN
     | BN t1' t2' => mk_BN (inter t1 t1') (inter t2 t2')
     | BS t1'' a'' t2'' => mk_BN (inter t1 t1'') (inter t2 t2'')) ∧
  ∀t1 a t2 t.
    inter (BS t1 a t2) t =
    case t of
      LN => LN
    | ⦕ 0 ↦ a' ⦖ => ⦕ 0 ↦ a ⦖
    | BN t1' t2' => mk_BN (inter t1 t1') (inter t2 t2')
    | BS t1'' a'³' t2'' => mk_BS (inter t1 t1'') a (inter t2 t2'')

⊢ (∀t. isEmpty (inter_eq LN t)) ∧
  (∀a t.
     inter_eq ⦕ 0 ↦ a ⦖ t =
     case t of
       LN => LN
     | ⦕ 0 ↦ b ⦖ => if a = b then ⦕ 0 ↦ a ⦖ else LN
     | BN t1 t2 => LN
     | BS t1' b' t2' => if a = b' then ⦕ 0 ↦ a ⦖ else LN) ∧
  (∀t1 t2 t.
     inter_eq (BN t1 t2) t =
     case t of
       LN => LN
     | ⦕ 0 ↦ a ⦖ => LN
     | BN t1' t2' => mk_BN (inter_eq t1 t1') (inter_eq t2 t2')
     | BS t1'' a'' t2'' => mk_BN (inter_eq t1 t1'') (inter_eq t2 t2'')) ∧
  ∀t1 a t2 t.
    inter_eq (BS t1 a t2) t =
    case t of
      LN => LN
    | ⦕ 0 ↦ a' ⦖ => if a' = a then ⦕ 0 ↦ a ⦖ else LN
    | BN t1' t2' => mk_BN (inter_eq t1 t1') (inter_eq t2 t2')
    | BS t1'' a'³' t2'' =>
      if a'³' = a then mk_BS (inter_eq t1 t1'') a (inter_eq t2 t2'')
      else mk_BN (inter_eq t1 t1'') (inter_eq t2 t2'')

⊢ (∀t. list_insert [] t = t) ∧
  ∀n ns t. list_insert (n::ns) t = list_insert ns (insert n () t)

⊢ isEmpty (list_to_num_set []) ∧
  ∀n ns. list_to_num_set (n::ns) = insert n () (list_to_num_set ns)

⊢ sptree$lrnext =
  WFREC (@R. WF R ∧ ∀n. n ≠ 0 ⇒ R ((n − 1) DIV 2) n)
    (λlrnext a. I (if a = 0 then 1 else 2 * lrnext ((a − 1) DIV 2)))

⊢ (∀f. isEmpty (map f LN)) ∧ (∀f a. map f ⦕ 0 ↦ a ⦖ = ⦕ 0 ↦ f a ⦖) ∧
  (∀f t1 t2. map f (BN t1 t2) = BN (map f t1) (map f t2)) ∧
  ∀f t1 a t2. map f (BS t1 a t2) = BS (map f t1) (f a) (map f t2)

⊢ (∀f i. isEmpty (mapi0 f i LN)) ∧
  (∀f i a. mapi0 f i ⦕ 0 ↦ a ⦖ = ⦕ 0 ↦ f i a ⦖) ∧
  (∀f i t1 t2.
     mapi0 f i (BN t1 t2) =
     (let
        inc = sptree$lrnext i
      in
        mk_BN (mapi0 f (i + 2 * inc) t1) (mapi0 f (i + inc) t2))) ∧
  ∀f i t1 a t2.
    mapi0 f i (BS t1 a t2) =
    (let
       inc = sptree$lrnext i
     in
       mk_BS (mapi0 f (i + 2 * inc) t1) (f i a) (mapi0 f (i + inc) t2))

⊢ ∀f pt. mapi f pt = mapi0 f 0 pt

⊢ isEmpty (mk_wf LN) ∧ (∀x. mk_wf ⦕ 0 ↦ x ⦖ = ⦕ 0 ↦ x ⦖) ∧
  (∀t1 t2. mk_wf (BN t1 t2) = mk_BN (mk_wf t1) (mk_wf t2)) ∧
  ∀t1 x t2. mk_wf (BS t1 x t2) = mk_BS (mk_wf t1) x (mk_wf t2)

⊢ size LN = 0 ∧ (∀a. size ⦕ 0 ↦ a ⦖ = 1) ∧
  (∀t1 t2. size (BN t1 t2) = size t1 + size t2) ∧
  ∀t1 a t2. size (BS t1 a t2) = size t1 + size t2 + 1

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

⊢ (∀v f f1 f2. spt_CASE LN v f f1 f2 = v) ∧
  (∀a v f f1 f2. spt_CASE ⦕ 0 ↦ a ⦖ v f f1 f2 = f a) ∧
  (∀a0 a1 v f f1 f2. spt_CASE (BN a0 a1) v f f1 f2 = f1 a0 a1) ∧
  ∀a0 a1 a2 v f f1 f2. spt_CASE (BS a0 a1 a2) v f f1 f2 = f2 a0 a1 a2

⊢ spt_center =
  WFREC (@R. WF R)
    (λspt_center a.
         case a of
           LN => I NONE
         | ⦕ 0 ↦ x ⦖ => I (SOME x)
         | BN v7 v8 => I NONE
         | BS t1 x' t2 => I (SOME x'))

⊢ (∀f acc. spt_fold f acc LN = acc) ∧
  (∀f acc a. spt_fold f acc ⦕ 0 ↦ a ⦖ = f a acc) ∧
  (∀f acc t1 t2.
     spt_fold f acc (BN t1 t2) = spt_fold f (spt_fold f acc t1) t2) ∧
  ∀f acc t1 a t2.
    spt_fold f acc (BS t1 a t2) = spt_fold f (f a (spt_fold f acc t1)) t2

⊢ isEmpty (spt_left LN) ∧ (∀x. isEmpty (spt_left ⦕ 0 ↦ x ⦖)) ∧
  (∀t1 t2. spt_left (BN t1 t2) = t1) ∧ ∀t1 x t2. spt_left (BS t1 x t2) = t1

⊢ isEmpty (spt_right LN) ∧ (∀x. isEmpty (spt_right ⦕ 0 ↦ x ⦖)) ∧
  (∀t1 t2. spt_right (BN t1 t2) = t2) ∧
  ∀t1 x t2. spt_right (BS t1 x t2) = t2

⊢ (∀f. spt_size f LN = 0) ∧ (∀f a. spt_size f ⦕ 0 ↦ a ⦖ = 1 + f a) ∧
  (∀f a0 a1. spt_size f (BN a0 a1) = 1 + (spt_size f a0 + spt_size f a1)) ∧
  ∀f a0 a1 a2.
    spt_size f (BS a0 a1 a2) = 1 + (spt_size f a0 + (f a1 + spt_size f a2))

⊢ ∀j q.
    add_pause j q = case q of [] => [(j,LN)] | (i,spt)::q => (i + j,spt)::q

⊢ (∀t. subspt LN t ⇔ T) ∧
  (∀x t. subspt ⦕ 0 ↦ x ⦖ t ⇔ spt_center t = SOME x) ∧
  (∀t1 t2 t.
     subspt (BN t1 t2) t ⇔ subspt t1 (spt_left t) ∧ subspt t2 (spt_right t)) ∧
  ∀t1 x t2 t.
    subspt (BS t1 x t2) t ⇔
    spt_center t = SOME x ∧ subspt t1 (spt_left t) ∧
    subspt t2 (spt_right t)

⊢ toAList = foldi (λk v a. (k,v)::a) 0 []

⊢ (∀acc. toListA acc LN = acc) ∧ (∀acc a. toListA acc ⦕ 0 ↦ a ⦖ = a::acc) ∧
  (∀acc t1 t2. toListA acc (BN t1 t2) = toListA (toListA acc t2) t1) ∧
  ∀acc t1 a t2. toListA acc (BS t1 a t2) = toListA (a::toListA acc t2) t1

⊢ ∀m. toList m = toListA [] m

⊢ ∀spt. toSortedAList spt = spts_to_alist 0 [(1,spt)] []

⊢ (∀t. union LN t = t) ∧
  (∀a t.
     union ⦕ 0 ↦ a ⦖ t =
     case t of
       LN => ⦕ 0 ↦ a ⦖
     | ⦕ 0 ↦ b ⦖ => ⦕ 0 ↦ a ⦖
     | BN t1 t2 => BS t1 a t2
     | BS t1' v4 t2' => BS t1' a t2') ∧
  (∀t1 t2 t.
     union (BN t1 t2) t =
     case t of
       LN => BN t1 t2
     | ⦕ 0 ↦ a ⦖ => BS t1 a t2
     | BN t1' t2' => BN (union t1 t1') (union t2 t2')
     | BS t1'' a'' t2'' => BS (union t1 t1'') a'' (union t2 t2'')) ∧
  ∀t1 a t2 t.
    union (BS t1 a t2) t =
    case t of
      LN => BS t1 a t2
    | ⦕ 0 ↦ a' ⦖ => BS t1 a t2
    | BN t1' t2' => BS (union t1 t1') a (union t2 t2')
    | BS t1'' a'³' t2'' => BS (union t1 t1'') a (union t2 t2'')

⊢ (wf LN ⇔ T) ∧ (∀a. wf ⦕ 0 ↦ a ⦖ ⇔ T) ∧
  (∀t1 t2. wf (BN t1 t2) ⇔ wf t1 ∧ wf t2 ∧ ¬(isEmpty t1 ∧ isEmpty t2)) ∧
  ∀t1 a t2. wf (BS t1 a t2) ⇔ wf t1 ∧ wf t2 ∧ ¬(isEmpty t1 ∧ isEmpty t2)

⊢ ∀t. ALL_DISTINCT (MAP FST (toAList t))

⊢ ALL_DISTINCT (MAP FST (toSortedAList t))

⊢ ∀t x. ALOOKUP (toAList t) x = lookup x t

⊢ ALOOKUP (toSortedAList spt) i = lookup i spt

⊢ FINITE (domain t)

⊢ ∀x y. subspt x y ∧ domain x ≠ domain y ⇒ size x < size y

⊢ ∀n x t1 t2.
    (n ∈ domain LN ⇔ F) ∧ (n ∈ domain ⦕ 0 ↦ x ⦖ ⇔ n = 0) ∧
    (n ∈ domain (BN t1 t2) ⇔
     n ≠ 0 ∧
     if EVEN n then (n − 1) DIV 2 ∈ domain t1
     else (n − 1) DIV 2 ∈ domain t2) ∧
    (n ∈ domain (BS t1 x t2) ⇔
     n = 0 ∨
     if EVEN n then (n − 1) DIV 2 ∈ domain t1
     else (n − 1) DIV 2 ∈ domain t2)

⊢ LENGTH (toAList t) = size t

⊢ LENGTH (toSortedAList t) = size t

⊢ MAP SND (gather_inclist_offsets xs) = MAP SND xs

⊢ ∀n acc.
    MAP f (foldi (λk v a. (k,v)::a) n acc pt) =
    foldi (λk v a. f (k,v)::a) n (MAP f acc) pt

⊢ ∀t k v. MEM (k,v) (toAList t) ⇔ lookup k t = SOME v

⊢ ∀x t. MEM x (toList t) ⇔ ∃k. lookup k t = SOME x

⊢ MEM (i,x) (toSortedAList spt) ⇔ lookup i spt = SOME x

⊢ PERM (toAList t) (toSortedAList t)

⊢ SORTED $< (MAP FST (toSortedAList spt))

⊢ EVERY (λx. f x ≤ g x) xs ⇒ SUM (MAP f xs) ≤ SUM (MAP g xs)

⊢ EVERY (λx. f x ≤ g x) xs ∧ EXISTS (λx. f x < g x) xs ⇒
  SUM (MAP f xs) < SUM (MAP g xs)

⊢ ∀xs ys s.
    ALL_DISTINCT xs ∧ LENGTH xs = LENGTH ys ⇒
    alist_insert (REVERSE xs) (REVERSE ys) s = alist_insert xs ys s

⊢ ∀a1 a2 s b1 b2.
    LENGTH a1 = LENGTH a2 ⇒
    alist_insert (a1 ⧺ b1) (a2 ⧺ b2) s =
    alist_insert a1 a2 (alist_insert b1 b2 s)

⊢ (∀xs t. alist_insert [] xs t = t) ∧
  (∀v6 v5 t. alist_insert (v5::v6) [] t = t) ∧
  ∀xs x vs v t.
    alist_insert (v::vs) (x::xs) t = insert v x (alist_insert vs xs t)

⊢ ∀P. (∀xs t. P [] xs t) ∧ (∀v5 v6 t. P (v5::v6) [] t) ∧
      (∀v vs x xs t. P vs xs t ⇒ P (v::vs) (x::xs) t) ⇒
      ∀v v1 v2. P v v1 v2

⊢ ∀xs ys z.
    ¬MEM x xs ⇒
    alist_insert xs ys (insert x y z) = insert x y (alist_insert xs ys z)

⊢ DATATYPE (spt LN LS BN BS)

⊢ delete (NUMERAL n) t = delete n t ∧ isEmpty (delete 0 LN) ∧
  isEmpty (delete 0 ⦕ 0 ↦ a ⦖) ∧ delete 0 (BN t1 t2) = BN t1 t2 ∧
  delete 0 (BS t1 a t2) = BN t1 t2 ∧ isEmpty (delete ZERO LN) ∧
  isEmpty (delete ZERO ⦕ 0 ↦ a ⦖) ∧ delete ZERO (BN t1 t2) = BN t1 t2 ∧
  delete ZERO (BS t1 a t2) = BN t1 t2 ∧ isEmpty (delete (BIT1 n) LN) ∧
  delete (BIT1 n) ⦕ 0 ↦ a ⦖ = ⦕ 0 ↦ a ⦖ ∧
  delete (BIT1 n) (BN t1 t2) = mk_BN t1 (delete n t2) ∧
  delete (BIT1 n) (BS t1 a t2) = mk_BS t1 a (delete n t2) ∧
  isEmpty (delete (BIT2 n) LN) ∧ delete (BIT2 n) ⦕ 0 ↦ a ⦖ = ⦕ 0 ↦ a ⦖ ∧
  delete (BIT2 n) (BN t1 t2) = mk_BN (delete n t1) t2 ∧
  delete (BIT2 n) (BS t1 a t2) = mk_BS (delete n t1) a t2

⊢ ∀f n k.
    delete n (delete k f) =
    if n = k then delete n f else delete k (delete n f)

⊢ ∀n t. wf t ⇒ (n ∉ domain t ⇔ delete n t = t)

⊢ ∀x t. delete x (mk_wf t) = mk_wf (delete x t)

⊢ isEmpty (difference a b) ⇒ domain a ⊆ domain b

⊢ ∀ls live. domain (FOLDR delete live ls) = domain live DIFF set ls

⊢ ∀a b locs.
    LENGTH a = LENGTH b ⇒
    domain (alist_insert a b locs) = domain locs ∪ set a

⊢ domain (delete k t) = domain t DELETE k

⊢ ∀t1 t2. domain (difference t1 t2) = domain t1 DIFF domain t2

⊢ ∀t. wf t ⇒ (isEmpty t ⇔ domain t = ∅)

⊢ ∀t1 t2.
    domain t1 = domain t2 ⇔ ∀k. lookup k t1 = NONE ⇔ lookup k t2 = NONE

⊢ domain t = foldi (λk v a. k INSERT a) 0 ∅ t

⊢ ∀ls. domain (fromAList ls) = set (MAP FST ls)

⊢ domain (fromList l) = count (LENGTH l)

⊢ domain (insert k v t) = k INSERT domain t

⊢ domain (inter t1 t2) = domain t1 ∩ domain t2

⊢ ∀xs x t. x ∈ domain (list_insert xs t) ⇔ MEM x xs ∨ x ∈ domain t

⊢ ∀xs. x ∈ domain (list_to_num_set xs) ⇔ MEM x xs

⊢ ∀t k. k ∈ domain t ⇔ ∃v. lookup k t = SOME v

⊢ ∀s. domain (map f s) = domain s

⊢ domain (mapi f x) = domain x

⊢ ∀t. domain (mk_wf t) = domain t

⊢ domain (insert k v LN) = {k}

⊢ domain (union t1 t2) = domain t1 ∪ domain t2

⊢ ∀f a t. foldi f 0 a t = FOLDR (UNCURRY f) a (toAList t)

⊢ ∀l1 l2. fromAList (l1 ⧺ l2) = union (fromAList l1) (fromAList l2)

⊢ isEmpty (fromAList []) ∧
  ∀y xs x. fromAList ((x,y)::xs) = insert x y (fromAList xs)

⊢ ∀P. P [] ∧ (∀x y xs. P xs ⇒ P ((x,y)::xs)) ⇒ ∀v. P v

⊢ ∀t. wf t ⇒ fromAList (toAList t) = t

⊢ ∀l. fromList l = fromAList (ZIP (COUNT_LIST (LENGTH l),l))

⊢ gather_inclist_offsets (xs ⧺ ys) =
  gather_inclist_offsets xs ⧺
  MAP ($+ (SUM (MAP FST xs)) ## I) (gather_inclist_offsets ys)

⊢ gather_inclist_offsets [] = [] ∧
  ∀xs x inc.
    gather_inclist_offsets ((inc,x)::xs) =
    (0,x)::MAP ($+ inc ## I) (gather_inclist_offsets xs)

⊢ ∀P. P [] ∧ (∀inc x xs. P xs ⇒ P ((inc,x)::xs)) ⇒ ∀v. P v

⊢ insert (NUMERAL n) a t = insert n a t ∧ insert 0 a LN = ⦕ 0 ↦ a ⦖ ∧
  insert 0 a ⦕ 0 ↦ a' ⦖ = ⦕ 0 ↦ a ⦖ ∧ insert 0 a (BN t1 t2) = BS t1 a t2 ∧
  insert 0 a (BS t1 a' t2) = BS t1 a t2 ∧ insert ZERO a LN = ⦕ 0 ↦ a ⦖ ∧
  insert ZERO a ⦕ 0 ↦ a' ⦖ = ⦕ 0 ↦ a ⦖ ∧
  insert ZERO a (BN t1 t2) = BS t1 a t2 ∧
  insert ZERO a (BS t1 a' t2) = BS t1 a t2 ∧
  insert (BIT1 n) a LN = BN LN (insert n a LN) ∧
  insert (BIT1 n) a ⦕ 0 ↦ a' ⦖ = BS LN a' (insert n a LN) ∧
  insert (BIT1 n) a (BN t1 t2) = BN t1 (insert n a t2) ∧
  insert (BIT1 n) a (BS t1 a' t2) = BS t1 a' (insert n a t2) ∧
  insert (BIT2 n) a LN = BN (insert n a LN) LN ∧
  insert (BIT2 n) a ⦕ 0 ↦ a' ⦖ = BS (insert n a LN) a' LN ∧
  insert (BIT2 n) a (BN t1 t2) = BN (insert n a t1) t2 ∧
  insert (BIT2 n) a (BS t1 a' t2) = BS (insert n a t1) a' t2

⊢ (∀k a.
     insert k a LN =
     if k = 0 then ⦕ 0 ↦ a ⦖
     else if EVEN k then BN (insert ((k − 1) DIV 2) a LN) LN
     else BN LN (insert ((k − 1) DIV 2) a LN)) ∧
  (∀k a' a.
     insert k a ⦕ 0 ↦ a' ⦖ =
     if k = 0 then ⦕ 0 ↦ a ⦖
     else if EVEN k then BS (insert ((k − 1) DIV 2) a LN) a' LN
     else BS LN a' (insert ((k − 1) DIV 2) a LN)) ∧
  (∀t2 t1 k a.
     insert k a (BN t1 t2) =
     if k = 0 then BS t1 a t2
     else if EVEN k then BN (insert ((k − 1) DIV 2) a t1) t2
     else BN t1 (insert ((k − 1) DIV 2) a t2)) ∧
  ∀t2 t1 k a' a.
    insert k a (BS t1 a' t2) =
    if k = 0 then BS t1 a t2
    else if EVEN k then BS (insert ((k − 1) DIV 2) a t1) a' t2
    else BS t1 a' (insert ((k − 1) DIV 2) a t2)

⊢ ∀ls k v.
    k < LENGTH ls ⇒
    insert k v (fromList ls) = fromList (TAKE k ls ⧺ [v] ⧺ DROP (SUC k) ls)

⊢ ∀P. (∀k a.
         (k ≠ 0 ∧ EVEN k ⇒ P ((k − 1) DIV 2) a LN) ∧
         (k ≠ 0 ∧ ¬EVEN k ⇒ P ((k − 1) DIV 2) a LN) ⇒
         P k a LN) ∧
      (∀k a a'.
         (k ≠ 0 ∧ EVEN k ⇒ P ((k − 1) DIV 2) a LN) ∧
         (k ≠ 0 ∧ ¬EVEN k ⇒ P ((k − 1) DIV 2) a LN) ⇒
         P k a ⦕ 0 ↦ a' ⦖) ∧
      (∀k a t1 t2.
         (k ≠ 0 ∧ EVEN k ⇒ P ((k − 1) DIV 2) a t1) ∧
         (k ≠ 0 ∧ ¬EVEN k ⇒ P ((k − 1) DIV 2) a t2) ⇒
         P k a (BN t1 t2)) ∧
      (∀k a t1 a' t2.
         (k ≠ 0 ∧ EVEN k ⇒ P ((k − 1) DIV 2) a t1) ∧
         (k ≠ 0 ∧ ¬EVEN k ⇒ P ((k − 1) DIV 2) a t2) ⇒
         P k a (BS t1 a' t2)) ⇒
      ∀v v1 v2. P v v1 v2

⊢ ∀x1 x2 v1 v2 t.
    insert x1 v1 (insert x2 v2 t) =
    if x1 = x2 then insert x1 v1 t else insert x2 v2 (insert x1 v1 t)

⊢ ∀x v t. insert x v (mk_wf t) = mk_wf (insert x v t)

⊢ insert k a t ≠ LN

⊢ ∀t a b c. insert a b (insert a c t) = insert a b t

⊢ ∀t a b c d. a ≠ c ⇒ insert a b (insert c d t) = insert c d (insert a b t)

⊢ ∀t x. lookup x t = SOME y ⇒ insert x y t = t

⊢ ∀k v s. insert k v s = union (insert k v LN) s

⊢ ∀t. isEmpty (inter t LN) ∧ isEmpty (inter LN t)

⊢ ∀t1 t2 t3. inter t1 (inter t2 t3) = inter (inter t1 t2) t3

⊢ ∀t1 t2 t3 t4.
    inter t1 t2 = inter t3 t4 ⇔
    ∀x. lookup x (inter t1 t2) = lookup x (inter t3 t4)

⊢ ∀x y. isEmpty (inter x y) ⇔ DISJOINT (domain x) (domain y)

⊢ ∀t1 t2. inter (mk_wf t1) (mk_wf t2) = mk_wf (inter t1 t2)

⊢ ∀t. wf t ⇒ (isEmpty t ⇔ toList t = [])

⊢ ∀t acc. wf t ⇒ (isEmpty t ⇔ toListA acc t = acc)

⊢ isEmpty (union m1 m2) ⇔ isEmpty m1 ∧ isEmpty m2

⊢ list_size f (xs ⧺ ys) = list_size f xs + list_size f ys

⊢ ∀l1 l2.
    list_to_num_set (l1 ⧺ l2) =
    union (list_to_num_set l1) (list_to_num_set l2)

⊢ ∀spt. lookup 0 spt = spt_center spt

⊢ lookup k (FOLDL union t ls) =
  FOLDL OPTION_CHOICE (lookup k t) (MAP (lookup k) ls)

⊢ lookup k t = NONE ⇔ k ∉ domain t

⊢ ∀x y t z.
    LENGTH x = LENGTH y ⇒
    lookup z (alist_insert x y t) =
    case ALOOKUP (ZIP (x,y)) z of NONE => lookup z t | SOME a => SOME a

⊢ lookup (NUMERAL n) t = lookup n t ∧ lookup 0 LN = NONE ∧
  lookup 0 ⦕ 0 ↦ a ⦖ = SOME a ∧ lookup 0 (BN t1 t2) = NONE ∧
  lookup 0 (BS t1 a t2) = SOME a ∧ lookup ZERO LN = NONE ∧
  lookup ZERO ⦕ 0 ↦ a ⦖ = SOME a ∧ lookup ZERO (BN t1 t2) = NONE ∧
  lookup ZERO (BS t1 a t2) = SOME a ∧ lookup (BIT1 n) LN = NONE ∧
  lookup (BIT1 n) ⦕ 0 ↦ a ⦖ = NONE ∧
  lookup (BIT1 n) (BN t1 t2) = lookup n t2 ∧
  lookup (BIT1 n) (BS t1 a t2) = lookup n t2 ∧ lookup (BIT2 n) LN = NONE ∧
  lookup (BIT2 n) ⦕ 0 ↦ a ⦖ = NONE ∧
  lookup (BIT2 n) (BN t1 t2) = lookup n t1 ∧
  lookup (BIT2 n) (BS t1 a t2) = lookup n t1

⊢ (∀k. lookup k LN = NONE) ∧
  (∀k a. lookup k ⦕ 0 ↦ a ⦖ = if k = 0 then SOME a else NONE) ∧
  (∀t2 t1 k.
     lookup k (BN t1 t2) =
     if k = 0 then NONE
     else lookup ((k − 1) DIV 2) (if EVEN k then t1 else t2)) ∧
  ∀t2 t1 k a.
    lookup k (BS t1 a t2) =
    if k = 0 then SOME a
    else lookup ((k − 1) DIV 2) (if EVEN k then t1 else t2)

⊢ ∀t k1 k2. lookup k1 (delete k2 t) = if k1 = k2 then NONE else lookup k1 t

⊢ ∀m1 m2 k.
    lookup k (difference m1 m2) =
    if lookup k m2 = NONE then lookup k m1 else NONE

⊢ ∀k t f.
    lookup k (filter_v f t) =
    case lookup k t of
      NONE => NONE
    | SOME v => if f v then SOME v else NONE

⊢ ∀ls x. lookup x (fromAList ls) = ALOOKUP ls x

⊢ ∀t x. lookup x (fromAList (toAList t)) = lookup x t

⊢ lookup n (fromList l) = if n < LENGTH l then SOME l❲n❳ else NONE

⊢ ∀k. LENGTH args ≤ k ⇒ lookup k (fromList args) = NONE

⊢ ∀P. (∀k. P k LN) ∧ (∀k a. P k ⦕ 0 ↦ a ⦖) ∧
      (∀k t1 t2.
         (k ≠ 0 ⇒ P ((k − 1) DIV 2) (if EVEN k then t1 else t2)) ⇒
         P k (BN t1 t2)) ∧
      (∀k t1 a t2.
         (k ≠ 0 ⇒ P ((k − 1) DIV 2) (if EVEN k then t1 else t2)) ⇒
         P k (BS t1 a t2)) ⇒
      ∀v v1. P v v1

⊢ ∀k2 v t k1.
    lookup k1 (insert k2 v t) = if k1 = k2 then SOME v else lookup k1 t

⊢ ∀k a t. lookup k (insert k a t) = SOME a

⊢ ∀m1 m2 k.
    lookup k (inter m1 m2) =
    case (lookup k m1,lookup k m2) of
      (NONE,v4) => NONE
    | (SOME v,NONE) => NONE
    | (SOME v,SOME w) => SOME v

⊢ (lookup x (inter t1 t2) = SOME y ⇔
   lookup x t1 = SOME y ∧ lookup x t2 ≠ NONE) ∧
  (lookup x (inter t1 t2) = NONE ⇔ lookup x t1 = NONE ∨ lookup x t2 = NONE)

⊢ lookup x (inter t1 t2) = if x ∈ domain t2 then lookup x t1 else NONE

⊢ lookup x (inter t1 (inter t2 t3)) = lookup x (inter (inter t1 t2) t3)

⊢ ∀m1 m2 k.
    lookup k (inter_eq m1 m2) =
    case lookup k m1 of
      NONE => NONE
    | SOME v => if lookup k m2 = SOME v then SOME v else NONE

⊢ ∀xs. lookup x (list_to_num_set xs) = if MEM x xs then SOME () else NONE

⊢ ∀s x. lookup x (map f s) = OPTION_MAP f (lookup x s)

⊢ ∀t n. lookup n (map (K x) t) = if n ∈ domain t then SOME x else NONE

⊢ lookup k (mapi f pt) = OPTION_MAP (f k) (lookup k pt)

⊢ ∀pt i k.
    lookup k (mapi0 f i pt) =
    case lookup k pt of NONE => NONE | SOME v => SOME (f (spt_acc i k) v)

⊢ lookup i (mk_BN t1 t2) =
  if i = 0 then NONE
  else lookup ((i − 1) DIV 2) (if EVEN i then t1 else t2)

⊢ ∀x t. lookup x (mk_wf t) = lookup x t

⊢ lookup k LN = NONE ∧ lookup 0 ⦕ 0 ↦ a ⦖ = SOME a ∧
  lookup 0 (BN t1 t2) = NONE ∧ lookup 0 (BS t1 a t2) = SOME a

⊢ lookup i (spt_left spt) = lookup (i * 2 + 2) spt

⊢ lookup i (spt_right spt) = lookup (i * 2 + 1) spt

⊢ ∀m1 m2 k.
    lookup k (union m1 m2) =
    case lookup k m1 of NONE => lookup k m2 | SOME v => SOME v

⊢ ∀n. sptree$lrnext n =
      if n = 0 then 1 else 2 * sptree$lrnext ((n − 1) DIV 2)

⊢ ∀n. sptree$lrnext n = 2 ** LOG2 (n + 1)

⊢ ∀P. (∀n. (n ≠ 0 ⇒ P ((n − 1) DIV 2)) ⇒ P n) ⇒ ∀v. P v

⊢ sptree$lrnext ZERO = 1 ∧
  (∀n. sptree$lrnext (BIT1 n) = 2 * sptree$lrnext n) ∧
  (∀n. sptree$lrnext (BIT2 n) = 2 * sptree$lrnext n) ∧
  (∀a. sptree$lrnext 0 = 1) ∧
  ∀n a. sptree$lrnext (NUMERAL n) = sptree$lrnext n

⊢ ∀t. isEmpty (map f t) ⇔ isEmpty t

⊢ map f (fromAList ls) = fromAList (MAP (λ(k,v). (k,f v)) ls)

⊢ ∀f x y z. map f (insert x y z) = insert x (f y) (map f z)

⊢ ∀t. map (K a) (map f t) = map (K a) t

⊢ ∀t f g. map f (map g t) = map (f ∘ g) t

⊢ ∀t1 t2. map f (union t1 t2) = union (map f t1) (map f t2)

⊢ mapi f pt =
  fromAList (MAP (λkv. (FST kv,f (FST kv) (SND kv))) (toAList pt))

⊢ mapi f (fromList ls) = fromList (MAPi f ls)

⊢ isEmpty (mk_BN LN LN) ∧ mk_BN LN ⦕ 0 ↦ v14 ⦖ = ⦕ 1 ↦ v14 ⦖ ∧
  mk_BN LN (BN v15 v16) = BN LN (BN v15 v16) ∧
  mk_BN LN (BS v17 v18 v19) = BN LN (BS v17 v18 v19) ∧
  mk_BN ⦕ 0 ↦ v2 ⦖ t2 = BN ⦕ 0 ↦ v2 ⦖ t2 ∧
  mk_BN (BN v3 v4) t2 = BN (BN v3 v4) t2 ∧
  mk_BN (BS v5 v6 v7) t2 = BN (BS v5 v6 v7) t2

⊢ ∀P. P LN LN ∧ (∀v14. P LN ⦕ 0 ↦ v14 ⦖) ∧ (∀v15 v16. P LN (BN v15 v16)) ∧
      (∀v17 v18 v19. P LN (BS v17 v18 v19)) ∧ (∀v2 t2. P ⦕ 0 ↦ v2 ⦖ t2) ∧
      (∀v3 v4 t2. P (BN v3 v4) t2) ∧ (∀v5 v6 v7 t2. P (BS v5 v6 v7) t2) ⇒
      ∀v v1. P v v1

⊢ mk_BS LN x LN = ⦕ 0 ↦ x ⦖ ∧ mk_BS ⦕ 0 ↦ v16 ⦖ x LN = ⦕ 0 ↦ x; 2 ↦ v16 ⦖ ∧
  mk_BS (BN v17 v18) x LN = BS (BN v17 v18) x LN ∧
  mk_BS (BS v19 v20 v21) x LN = BS (BS v19 v20 v21) x LN ∧
  mk_BS t1 x ⦕ 0 ↦ v4 ⦖ = BS t1 x ⦕ 0 ↦ v4 ⦖ ∧
  mk_BS t1 x (BN v5 v6) = BS t1 x (BN v5 v6) ∧
  mk_BS t1 x (BS v7 v8 v9) = BS t1 x (BS v7 v8 v9)

⊢ ∀P. (∀x. P LN x LN) ∧ (∀v16 x. P ⦕ 0 ↦ v16 ⦖ x LN) ∧
      (∀v17 v18 x. P (BN v17 v18) x LN) ∧
      (∀v19 v20 v21 x. P (BS v19 v20 v21) x LN) ∧
      (∀t1 x v4. P t1 x ⦕ 0 ↦ v4 ⦖) ∧ (∀t1 x v5 v6. P t1 x (BN v5 v6)) ∧
      (∀t1 x v7 v8 v9. P t1 x (BS v7 v8 v9)) ⇒
      ∀v v1 v2. P v v1 v2

⊢ ∀t1 t2. mk_wf t1 = mk_wf t2 ⇔ ∀x. lookup x t1 = lookup x t2

⊢ ∀t1 t2. wf t1 ∧ wf t2 ⇒ (domain t1 = domain t2 ⇔ t1 = t2)

⊢ set (MAP FST (toAList t)) = domain t

⊢ ∀t a i.
    foldi (λk v a. k INSERT a) i a t =
    a ∪ IMAGE (λn. i + sptree$lrnext i * n) (domain t)

⊢ ∀n t.
    size (delete n t) = if lookup n t = NONE then size t else size t − 1

⊢ ∀x y z t.
    domain z ⊆ domain y ∧ t ∈ domain y ∧ t ∉ domain z ∧ t ∈ domain x ⇒
    size (difference x y) < size (difference x z)

⊢ ∀t. size t = CARD (domain t)

⊢ size (fromList ls) = LENGTH ls

⊢ ∀k v m. size (insert k v m) = if k ∈ domain m then size m else size m + 1

⊢ size (list_to_num_set ls) = LENGTH (nub ls)

⊢ size (map f t) = size t

⊢ size (mapi f t) = size t

⊢ ∀x. size x = 0 ⇔ domain x = ∅

⊢ (∀a a'. ⦕ 0 ↦ a ⦖ = ⦕ 0 ↦ a' ⦖ ⇔ a = a') ∧
  (∀a0 a1 a0' a1'. BN a0 a1 = BN a0' a1' ⇔ a0 = a0' ∧ a1 = a1') ∧
  ∀a0 a1 a2 a0' a1' a2'.
    BS a0 a1 a2 = BS a0' a1' a2' ⇔ a0 = a0' ∧ a1 = a1' ∧ a2 = a2'

⊢ ∀f0 f1 f2 f3. ∃fn.
    fn LN = f0 ∧ (∀a. fn ⦕ 0 ↦ a ⦖ = f1 a) ∧
    (∀a0 a1. fn (BN a0 a1) = f2 a0 a1 (fn a0) (fn a1)) ∧
    ∀a0 a1 a2. fn (BS a0 a1 a2) = f3 a1 a0 a2 (fn a0) (fn a2)

⊢ ∀k. spt_acc 0 k = k

⊢ (∀i. spt_acc i 0 = i) ∧
  (∀k i.
     spt_acc i (NUMERAL (BIT1 k)) =
     spt_acc
       (i +
        if EVEN (NUMERAL (BIT1 k)) then 2 * sptree$lrnext i
        else sptree$lrnext i) ((NUMERAL (BIT1 k) − 1) DIV 2)) ∧
  ∀k i.
    spt_acc i (NUMERAL (BIT2 k)) =
    spt_acc
      (i +
       if EVEN (NUMERAL (BIT2 k)) then 2 * sptree$lrnext i
       else sptree$lrnext i) (NUMERAL (BIT1 k) DIV 2)

⊢ (∀i. spt_acc i 0 = i) ∧
  ∀k i.
    spt_acc i (SUC k) =
    spt_acc
      (i + if EVEN (SUC k) then 2 * sptree$lrnext i else sptree$lrnext i)
      (k DIV 2)

⊢ ∀k i. spt_acc i k = sptree$lrnext i * k + i

⊢ ∀P. (∀i. P i 0) ∧
      (∀i k.
         P
           (i +
            if EVEN (SUC k) then 2 * sptree$lrnext i else sptree$lrnext i)
           (k DIV 2) ⇒
         P i (SUC k)) ⇒
      ∀v v1. P v v1

⊢ spt_acc i k =
  if k = 0 then i
  else
    spt_acc (i + if EVEN k then 2 * sptree$lrnext i else sptree$lrnext i)
      ((k − 1) DIV 2)

⊢ ∀M M' v f f1 f2.
    M = M' ∧ (isEmpty M' ⇒ v = v') ∧ (∀a. M' = ⦕ 0 ↦ a ⦖ ⇒ f a = f' a) ∧
    (∀a0 a1. M' = BN a0 a1 ⇒ f1 a0 a1 = f1' a0 a1) ∧
    (∀a0 a1 a2. M' = BS a0 a1 a2 ⇒ f2 a0 a1 a2 = f2' a0 a1 a2) ⇒
    spt_CASE M v f f1 f2 = spt_CASE M' v' f' f1' f2'

⊢ spt_CASE x v f f1 f2 = v' ⇔
  isEmpty x ∧ v = v' ∨ (∃a. x = ⦕ 0 ↦ a ⦖ ∧ f a = v') ∨
  (∃s s0. x = BN s s0 ∧ f1 s s0 = v') ∨
  ∃s a s0. x = BS s a s0 ∧ f2 s a s0 = v'

⊢ spt_center ⦕ 0 ↦ x ⦖ = SOME x ∧ spt_center (BS t1 x t2) = SOME x ∧
  spt_center LN = NONE ∧ spt_center (BN v1 v2) = NONE

⊢ ∀P. (∀x. P ⦕ 0 ↦ x ⦖) ∧ (∀t1 x t2. P (BS t1 x t2)) ∧ P LN ∧
      (∀v1 v2. P (BN v1 v2)) ⇒
      ∀v. P v

⊢ (∀a. LN ≠ ⦕ 0 ↦ a ⦖) ∧ (∀a1 a0. LN ≠ BN a0 a1) ∧
  (∀a2 a1 a0. LN ≠ BS a0 a1 a2) ∧ (∀a1 a0 a. ⦕ 0 ↦ a ⦖ ≠ BN a0 a1) ∧
  (∀a2 a1 a0 a. ⦕ 0 ↦ a ⦖ ≠ BS a0 a1 a2) ∧
  ∀a2 a1' a1 a0' a0. BN a0 a1 ≠ BS a0' a1' a2

⊢ ∀t1 t2. wf t1 ∧ wf t2 ⇒ (t1 = t2 ⇔ ∀n. lookup n t1 = lookup n t2)

⊢ ∀P. P LN ∧ (∀a. P ⦕ 0 ↦ a ⦖) ∧ (∀s s0. P s ∧ P s0 ⇒ P (BN s s0)) ∧
      (∀s s0. P s ∧ P s0 ⇒ ∀a. P (BS s a s0)) ⇒
      ∀s. P s

⊢ ∀ss.
    isEmpty ss ∨ (∃a. ss = ⦕ 0 ↦ a ⦖) ∨ (∃s s0. ss = BN s s0) ∨
    ∃s a s0. ss = BS s a s0

⊢ ∀xs repeat i acc_right acc_left acc_cent.
    spts_to_alist_aux i xs acc_cent acc_right acc_left repeat =
    case xs of
      [] => (i,REVERSE acc_right ⧺ REVERSE acc_left,acc_cent,repeat)
    | (j,LN)::ys =>
      spts_to_alist_aux (i + j) ys acc_cent (add_pause j acc_right)
        (add_pause j acc_left) repeat
    | (j,spt)::ys =>
      spts_to_alist_aux (i + j) ys
        ((case spt_center spt of NONE => [] | SOME c => [(i,c)]) ⧺ acc_cent)
        ((j,spt_right spt)::acc_right) ((j,spt_left spt)::acc_left) T

⊢ ∀P. (∀i xs acc_cent acc_right acc_left repeat.
         (∀v ys j spt.
            xs = v::ys ∧ v = (j,spt) ∧ spt ≠ LN ⇒
            P (i + j) ys
              ((case spt_center spt of NONE => [] | SOME c => [(i,c)]) ⧺
               acc_cent) ((j,spt_right spt)::acc_right)
              ((j,spt_left spt)::acc_left) T) ∧
         (∀v ys j spt.
            xs = v::ys ∧ v = (j,spt) ∧ isEmpty spt ⇒
            P (i + j) ys acc_cent (add_pause j acc_right)
              (add_pause j acc_left) repeat) ⇒
         P i xs acc_cent acc_right acc_left repeat) ⇒
      ∀v v1 v2 v3 v4 v5. P v v1 v2 v3 v4 v5

⊢ ∀i xs acc_cent acc_right acc_left repeat j ys acc2 repeat2.
    spts_to_alist_aux i xs acc_cent acc_right acc_left repeat =
    (j,ys,acc2,repeat2) ⇒
    j = i + SUM (MAP FST xs) ∧
    SUM (MAP FST ys) = SUM (MAP FST (acc_right ⧺ acc_left ⧺ xs ⧺ xs)) ∧
    inclist_stable ys =
    inclist_stable
      (REVERSE acc_right ⧺ MAP (I ## spt_right) xs ⧺ REVERSE acc_left ⧺
       MAP (I ## spt_left) xs) ∧
    acc2 =
    REVERSE
      (FLAT
         (MAP
            (λ(j,spt).
                 case spt_center spt of NONE => [] | SOME v => [(i + j,v)])
            (inclist_stable xs))) ⧺ acc_cent ∧
    (repeat2 ⇔ repeat ∨ ¬NULL (inclist_stable xs))

⊢ ∀i xs acc_cent acc_right acc_left repeat j ys acc2 repeat2.
    spts_to_alist_aux i xs acc_cent acc_right acc_left repeat =
    (j,ys,acc2,repeat2) ⇒
    (let
       sz = SUM ∘ MAP (spt_size (K 0) ∘ SND)
     in
       sz ys ≤ sz (xs ⧺ acc_right ⧺ acc_left) ∧
       (repeat2 ⇒ ¬repeat ⇒ sz ys < sz (xs ⧺ acc_right ⧺ acc_left)))

⊢ ∀xs i acc_cent.
    spts_to_alist i xs acc_cent =
    (let
       (i',xs',acc_cent',repeat) = spts_to_alist_aux i xs acc_cent [] [] F
     in
       if repeat then spts_to_alist i' xs' acc_cent' else REVERSE acc_cent')

⊢ ∀P. (∀i xs acc_cent.
         (∀i' xs' acc_cent' repeat.
            (i',xs',acc_cent',repeat) =
            spts_to_alist_aux i xs acc_cent [] [] F ∧ repeat ⇒
            P i' xs' acc_cent') ⇒
         P i xs acc_cent) ⇒
      ∀v v1 v2. P v v1 v2

⊢ ∀ls t. subspt t (FOLDL union t ls)

⊢ (subspt LN sp ⇔ T) ∧ (subspt sp LN ⇔ domain sp = ∅)

⊢ ∀sp1 sp2.
    subspt sp1 sp2 ⇔
    ∀k. k ∈ domain sp1 ⇒ k ∈ domain sp2 ∧ lookup k sp2 = lookup k sp1

⊢ ∀t1 t2. subspt t1 t2 ⇔ domain t1 ⊆ domain t2

⊢ ∀t1 t2. subspt t1 t2 ⇔ ∀x y. lookup x t1 = SOME y ⇒ lookup x t2 = SOME y

⊢ subspt sp sp

⊢ subspt sp1 sp2 ∧ subspt sp2 sp3 ⇒ subspt sp1 sp3

⊢ subspt s (union s t)

⊢ ∀t acc. toListA acc t = toListA [] t ⧺ acc

⊢ ∀s. toList (map f s) = MAP f (toList s)

⊢ toSortedAList (fromList ls) = ZIP (COUNT_LIST (LENGTH ls),ls)

⊢ ∀t. union t LN = t ∧ union LN t = t

⊢ ∀t1 t2 t3. union t1 (union t2 t3) = union (union t1 t2) t3

⊢ ∀t1 t2.
    wf t1 ∧ wf t2 ∧ DISJOINT (domain t1) (domain t2) ⇒
    union t1 t2 = union t2 t1

⊢ ∀x y t2. union (insert x y LN) t2 = insert x y t2

⊢ ∀t1 t2. union (mk_wf t1) (mk_wf t2) = mk_wf (union t1 t2)

⊢ ∀t1 t2. union t1 t2 = union t2 t1

⊢ wf LN

⊢ ∀t k. wf t ⇒ wf (delete k t)

⊢ ∀t1 t2. wf t1 ∧ wf t2 ⇒ wf (difference t1 t2)

⊢ ∀t f. wf t ⇒ wf (filter_v f t)

⊢ ∀ls. wf (fromAList ls)

⊢ wf (fromList ls)

⊢ ∀k a t. wf t ⇒ wf (insert k a t)

⊢ ∀m1 m2. wf (inter m1 m2)

⊢ ∀ls. wf (list_to_num_set ls)

⊢ ∀t f. wf (map f t) ⇔ wf t

⊢ wf (mapi f pt)

⊢ wf t1 ∧ wf t2 ⇒ wf (mk_BN t1 t2)

⊢ wf t1 ∧ wf t2 ⇒ wf (mk_BS t1 a t2)

⊢ ∀t. wf t ⇒ mk_wf t = t

⊢ ∀t. wf (mk_wf t)

⊢ ∀m1 m2. wf m1 ∧ wf m2 ⇒ wf (union m1 m2)