Structure sptreeTheory


Source File Identifier index Theory binding index

signature sptreeTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val apsnd_cons_def : thm
    val delete_def : thm
    val difference_def : thm
    val domain_def : thm
    val expand_rle_def : thm
    val filter_v_def : thm
    val foldi_def : thm
    val fromAList_def_primitive : thm
    val fromList_def : thm
    val inter_def : thm
    val inter_eq_def : thm
    val list_insert_def : thm
    val list_to_num_set_def : thm
    val lrnext_def_primitive : thm
    val map_def : thm
    val mapi0_def : thm
    val mapi_def : thm
    val mk_wf_def : thm
    val size_def : thm
    val spt_TY_DEF : thm
    val spt_case_def : thm
    val spt_center_def_primitive : thm
    val spt_fold_def : thm
    val spt_left_def : thm
    val spt_right_def : thm
    val spt_size_def : thm
    val subspt_eq : thm
    val toAList_def : thm
    val toListA_def : thm
    val toList_def : thm
    val toSortedAList_def : thm
    val union_def : thm
    val wf_def : thm
  
  (*  Theorems  *)
    val ALL_DISTINCT_MAP_FST_toAList : thm
    val ALL_DISTINCT_MAP_FST_toSortedAList : thm
    val ALOOKUP_toAList : thm
    val ALOOKUP_toSortedAList : thm
    val EVERY_combine_rle : thm
    val EVERY_empty_SND_combine : thm
    val FINITE_domain : thm
    val IMP_size_LESS_size : thm
    val IN_domain : thm
    val LENGTH_toAList : thm
    val LENGTH_toSortedAList : thm
    val MAP_foldi : thm
    val MEM_spts_to_alist : thm
    val MEM_toAList : thm
    val MEM_toList : thm
    val MEM_toSortedAList : thm
    val SORTED_spts_to_alist_lemma : thm
    val SORTED_toSortedAList : thm
    val SUM_MAP_same_LE : thm
    val SUM_MAP_same_LESS : thm
    val alist_insert_REVERSE : thm
    val alist_insert_append : thm
    val alist_insert_def : thm
    val alist_insert_ind : thm
    val alist_insert_pull_insert : thm
    val apsnd_cons_is_case : thm
    val combine_rle_def : thm
    val combine_rle_ind : thm
    val combine_rle_ind2 : thm
    val combine_rle_props : thm
    val datatype_spt : thm
    val delete_compute : thm
    val delete_delete : thm
    val delete_fail : thm
    val delete_mk_wf : thm
    val difference_sub : thm
    val domain_FOLDR_delete : thm
    val domain_alist_insert : thm
    val domain_delete : thm
    val domain_difference : thm
    val domain_empty : thm
    val domain_eq : thm
    val domain_foldi : thm
    val domain_fromAList : thm
    val domain_fromList : thm
    val domain_insert : thm
    val domain_inter : thm
    val domain_list_insert : thm
    val domain_list_to_num_set : thm
    val domain_lookup : thm
    val domain_map : thm
    val domain_mapi : thm
    val domain_mk_wf : thm
    val domain_sing : thm
    val domain_union : thm
    val expand_rle_append : thm
    val expand_rle_combine_rle : thm
    val expand_rle_map : thm
    val foldi_FOLDR_toAList : thm
    val fromAList_append : thm
    val fromAList_def : thm
    val fromAList_ind : thm
    val fromAList_toAList : thm
    val fromList_fromAList : thm
    val fst_spt_centers_imp : thm
    val insert_compute : thm
    val insert_def : thm
    val insert_fromList_IN_domain : thm
    val insert_ind : thm
    val insert_insert : thm
    val insert_mk_wf : thm
    val insert_notEmpty : thm
    val insert_shadow : thm
    val insert_swap : thm
    val insert_unchanged : thm
    val insert_union : thm
    val inter_LN : thm
    val inter_assoc : thm
    val inter_eq : thm
    val inter_eq_LN : thm
    val inter_mk_wf : thm
    val isEmpty_toList : thm
    val isEmpty_toListA : thm
    val isEmpty_union : thm
    val list_size_APPEND : thm
    val list_to_num_set_append : thm
    val lookup_0_spt_center : thm
    val lookup_FOLDL_union : thm
    val lookup_NONE_domain : thm
    val lookup_SOME_left_right_cases : thm
    val lookup_alist_insert : thm
    val lookup_compute : thm
    val lookup_def : thm
    val lookup_delete : thm
    val lookup_difference : thm
    val lookup_filter_v : thm
    val lookup_fromAList : thm
    val lookup_fromAList_toAList : thm
    val lookup_fromList : thm
    val lookup_fromList_outside : thm
    val lookup_ind : thm
    val lookup_insert : thm
    val lookup_insert1 : thm
    val lookup_inter : thm
    val lookup_inter_EQ : thm
    val lookup_inter_alt : thm
    val lookup_inter_assoc : thm
    val lookup_inter_eq : thm
    val lookup_list_to_num_set : thm
    val lookup_map : thm
    val lookup_map_K : thm
    val lookup_mapi : thm
    val lookup_mapi0 : thm
    val lookup_mk_BN : thm
    val lookup_mk_wf : thm
    val lookup_rwts : thm
    val lookup_spt_left : thm
    val lookup_spt_right : thm
    val lookup_union : thm
    val lrnext_def : thm
    val lrnext_eq : thm
    val lrnext_ind : thm
    val lrnext_thm : thm
    val map_LN : thm
    val map_fromAList : thm
    val map_insert : thm
    val map_map_K : thm
    val map_map_o : thm
    val map_union : thm
    val mapi_Alist : thm
    val mapi_fromList : thm
    val mk_BN_def : thm
    val mk_BN_ind : thm
    val mk_BS_def : thm
    val mk_BS_ind : thm
    val mk_wf_eq : thm
    val num_set_domain_eq : thm
    val set_MAP_FST_toAList_domain : thm
    val set_foldi_keys : thm
    val size_delete : thm
    val size_diff_less : thm
    val size_domain : thm
    val size_fromList : thm
    val size_insert : thm
    val size_map : thm
    val size_mapi : thm
    val size_zero_empty : thm
    val spt_11 : thm
    val spt_Axiom : thm
    val spt_acc_0 : thm
    val spt_acc_compute : thm
    val spt_acc_def : thm
    val spt_acc_eqn : thm
    val spt_acc_ind : thm
    val spt_acc_thm : thm
    val spt_case_cong : thm
    val spt_case_eq : thm
    val spt_center_def : thm
    val spt_center_ind : thm
    val spt_centers_def : thm
    val spt_centers_expand_rle : thm
    val spt_centers_expand_rle_imp : thm
    val spt_centers_ind : thm
    val spt_centers_ord : thm
    val spt_distinct : thm
    val spt_eq_thm : thm
    val spt_induction : thm
    val spt_nchotomy : thm
    val spts_to_alist_def : thm
    val spts_to_alist_ind : thm
    val subspt_FOLDL_union : thm
    val subspt_LN : thm
    val subspt_def : thm
    val subspt_domain : thm
    val subspt_lookup : thm
    val subspt_refl : thm
    val subspt_trans : thm
    val subspt_union : thm
    val sum_size_combine_rle_LE : thm
    val toListA_append : thm
    val toList_map : thm
    val toSortedAList_fromList : thm
    val union_LN : thm
    val union_assoc : thm
    val union_disjoint_sym : thm
    val union_insert_LN : thm
    val union_mk_wf : thm
    val union_num_set_sym : thm
    val wf_LN : thm
    val wf_delete : thm
    val wf_difference : thm
    val wf_filter_v : thm
    val wf_fromAList : thm
    val wf_fromList : thm
    val wf_insert : thm
    val wf_inter : thm
    val wf_map : thm
    val wf_mapi : thm
    val wf_mk_BN : thm
    val wf_mk_BS : thm
    val wf_mk_id : thm
    val wf_mk_wf : thm
    val wf_union : thm
  
  val sptree_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [alist] Parent theory of "sptree"
   
   [logroot] Parent theory of "sptree"
   
   [apsnd_cons_def]  Definition
      
      ⊢ ∀x y xs. apsnd_cons x (y,xs) = (y,x::xs)
   
   [delete_def]  Definition
      
      ⊢ (∀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)
   
   [difference_def]  Definition
      
      ⊢ (∀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_def]  Definition
      
      ⊢ 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)
   
   [expand_rle_def]  Definition
      
      ⊢ ∀xs. expand_rle xs = FLAT (MAP (λ(i,t). REPLICATE i t) xs)
   
   [filter_v_def]  Definition
      
      ⊢ (∀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)
   
   [foldi_def]  Definition
      
      ⊢ (∀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_def_primitive]  Definition
      
      ⊢ 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)))
   
   [fromList_def]  Definition
      
      ⊢ ∀l. fromList l =
            SND (FOLDL (λ(i,t) a. (i + 1,insert i a t)) (0,LN) l)
   
   [inter_def]  Definition
      
      ⊢ (∀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'')
   
   [inter_eq_def]  Definition
      
      ⊢ (∀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'')
   
   [list_insert_def]  Definition
      
      ⊢ (∀t. list_insert [] t = t) ∧
        ∀n ns t. list_insert (n::ns) t = list_insert ns (insert n () t)
   
   [list_to_num_set_def]  Definition
      
      ⊢ isEmpty (list_to_num_set []) ∧
        ∀n ns. list_to_num_set (n::ns) = insert n () (list_to_num_set ns)
   
   [lrnext_def_primitive]  Definition
      
      ⊢ 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)))
   
   [map_def]  Definition
      
      ⊢ (∀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)
   
   [mapi0_def]  Definition
      
      ⊢ (∀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))
   
   [mapi_def]  Definition
      
      ⊢ ∀f pt. mapi f pt = mapi0 f 0 pt
   
   [mk_wf_def]  Definition
      
      ⊢ 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_def]  Definition
      
      ⊢ 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
   
   [spt_TY_DEF]  Definition
      
      ⊢ ∃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
   
   [spt_case_def]  Definition
      
      ⊢ (∀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_def_primitive]  Definition
      
      ⊢ 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'))
   
   [spt_fold_def]  Definition
      
      ⊢ (∀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
   
   [spt_left_def]  Definition
      
      ⊢ 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
   
   [spt_right_def]  Definition
      
      ⊢ 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
   
   [spt_size_def]  Definition
      
      ⊢ (∀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))
   
   [subspt_eq]  Definition
      
      ⊢ (∀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_def]  Definition
      
      ⊢ toAList = foldi (λk v a. (k,v)::a) 0 []
   
   [toListA_def]  Definition
      
      ⊢ (∀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
   
   [toList_def]  Definition
      
      ⊢ ∀m. toList m = toListA [] m
   
   [toSortedAList_def]  Definition
      
      ⊢ ∀spt. toSortedAList spt = spts_to_alist 0 [(1,spt)]
   
   [union_def]  Definition
      
      ⊢ (∀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_def]  Definition
      
      ⊢ (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)
   
   [ALL_DISTINCT_MAP_FST_toAList]  Theorem
      
      ⊢ ∀t. ALL_DISTINCT (MAP FST (toAList t))
   
   [ALL_DISTINCT_MAP_FST_toSortedAList]  Theorem
      
      ⊢ ALL_DISTINCT (MAP FST (toSortedAList t))
   
   [ALOOKUP_toAList]  Theorem
      
      ⊢ ∀t x. ALOOKUP (toAList t) x = lookup x t
   
   [ALOOKUP_toSortedAList]  Theorem
      
      ⊢ ALOOKUP (toSortedAList spt) i = lookup i spt
   
   [EVERY_combine_rle]  Theorem
      
      ⊢ ∀P xs. EVERY (Q ∘ SND) (combine_rle P xs) ⇔ EVERY (Q ∘ SND) xs
   
   [EVERY_empty_SND_combine]  Theorem
      
      ⊢ ∀xs.
          EVERY ((λt. isEmpty t) ∘ SND) xs ⇒
          xs = [] ∨
          ∃n. combine_rle (λt. isEmpty t) xs = [(n,LN)] ∧
              expand_rle xs = REPLICATE n LN
   
   [FINITE_domain]  Theorem
      
      ⊢ FINITE (domain t)
   
   [IMP_size_LESS_size]  Theorem
      
      ⊢ ∀x y. subspt x y ∧ domain x ≠ domain y ⇒ size x < size y
   
   [IN_domain]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ LENGTH (toAList t) = size t
   
   [LENGTH_toSortedAList]  Theorem
      
      ⊢ LENGTH (toSortedAList t) = size t
   
   [MAP_foldi]  Theorem
      
      ⊢ ∀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
   
   [MEM_spts_to_alist]  Theorem
      
      ⊢ ∀n xs i x.
          rle_wf xs ⇒
          (MEM (i,x) (spts_to_alist n xs) ⇔
           ∃j k.
             j < LENGTH (expand_rle xs) ∧
             lookup k (EL j (expand_rle xs)) = SOME x ∧
             i = n + j + k * LENGTH (expand_rle xs))
   
   [MEM_toAList]  Theorem
      
      ⊢ ∀t k v. MEM (k,v) (toAList t) ⇔ lookup k t = SOME v
   
   [MEM_toList]  Theorem
      
      ⊢ ∀x t. MEM x (toList t) ⇔ ∃k. lookup k t = SOME x
   
   [MEM_toSortedAList]  Theorem
      
      ⊢ MEM (i,x) (toSortedAList spt) ⇔ lookup i spt = SOME x
   
   [SORTED_spts_to_alist_lemma]  Theorem
      
      ⊢ ∀n xs.
          rle_wf xs ⇒
          SORTED $< (MAP FST (spts_to_alist n xs)) ∧
          ∀k. k ≤ n ⇒ EVERY (λt. FST t ≥ k) (spts_to_alist n xs)
   
   [SORTED_toSortedAList]  Theorem
      
      ⊢ SORTED $< (MAP FST (toSortedAList spt))
   
   [SUM_MAP_same_LE]  Theorem
      
      ⊢ EVERY (λx. f x ≤ g x) xs ⇒ SUM (MAP f xs) ≤ SUM (MAP g xs)
   
   [SUM_MAP_same_LESS]  Theorem
      
      ⊢ EVERY (λx. f x ≤ g x) xs ∧ EXISTS (λx. f x < g x) xs ⇒
        SUM (MAP f xs) < SUM (MAP g xs)
   
   [alist_insert_REVERSE]  Theorem
      
      ⊢ ∀xs ys s.
          ALL_DISTINCT xs ∧ LENGTH xs = LENGTH ys ⇒
          alist_insert (REVERSE xs) (REVERSE ys) s = alist_insert xs ys s
   
   [alist_insert_append]  Theorem
      
      ⊢ ∀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)
   
   [alist_insert_def]  Theorem
      
      ⊢ (∀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)
   
   [alist_insert_ind]  Theorem
      
      ⊢ ∀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
   
   [alist_insert_pull_insert]  Theorem
      
      ⊢ ∀xs ys z.
          ¬MEM x xs ⇒
          alist_insert xs ys (insert x y z) =
          insert x y (alist_insert xs ys z)
   
   [apsnd_cons_is_case]  Theorem
      
      ⊢ apsnd_cons x t = case t of (y,xs) => (y,x::xs)
   
   [combine_rle_def]  Theorem
      
      ⊢ (∀v0. combine_rle v0 [] = []) ∧ (∀v1 t. combine_rle v1 [t] = [t]) ∧
        ∀y xs x j i P.
          combine_rle P ((i,x)::(j,y)::xs) =
          if P x ∧ x = y then combine_rle P ((i + j,x)::xs)
          else (i,x)::combine_rle P ((j,y)::xs)
   
   [combine_rle_ind]  Theorem
      
      ⊢ ∀P'.
          (∀v0. P' v0 []) ∧ (∀v1 t. P' v1 [t]) ∧
          (∀P i x j y xs.
             (¬(P x ∧ x = y) ⇒ P' P ((j,y)::xs)) ∧
             (P x ∧ x = y ⇒ P' P ((i + j,x)::xs)) ⇒
             P' P ((i,x)::(j,y)::xs)) ⇒
          ∀v v1. P' v v1
   
   [combine_rle_ind2]  Theorem
      
      ⊢ ∀P3 P4.
          P4 [] ∧ (∀t. P4 [t]) ∧
          (∀i x j y xs.
             ((x = y ⇒ ¬P3 y) ⇒ P4 ((j,y)::xs)) ∧
             (P3 x ∧ x = y ⇒ P4 ((i + j,y)::xs)) ⇒
             P4 ((i,x)::(j,y)::xs)) ⇒
          ∀v1. P4 v1
   
   [combine_rle_props]  Theorem
      
      ⊢ ∀xs.
          rle_wf xs ⇒
          rle_wf (combine_rle (λt. isEmpty t) xs) ∧
          rle_wf
            (MAP (λ(i,t). (i,spt_right t)) (combine_rle (λt. isEmpty t) xs)) ∧
          rle_wf
            (MAP (λ(i,t). (i,spt_left t)) (combine_rle (λt. isEmpty t) xs))
   
   [datatype_spt]  Theorem
      
      ⊢ DATATYPE (spt LN LS BN BS)
   
   [delete_compute]  Theorem
      
      ⊢ 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
   
   [delete_delete]  Theorem
      
      ⊢ ∀f n k.
          delete n (delete k f) =
          if n = k then delete n f else delete k (delete n f)
   
   [delete_fail]  Theorem
      
      ⊢ ∀n t. wf t ⇒ (n ∉ domain t ⇔ delete n t = t)
   
   [delete_mk_wf]  Theorem
      
      ⊢ ∀x t. delete x (mk_wf t) = mk_wf (delete x t)
   
   [difference_sub]  Theorem
      
      ⊢ isEmpty (difference a b) ⇒ domain a ⊆ domain b
   
   [domain_FOLDR_delete]  Theorem
      
      ⊢ ∀ls live. domain (FOLDR delete live ls) = domain live DIFF set ls
   
   [domain_alist_insert]  Theorem
      
      ⊢ ∀a b locs.
          LENGTH a = LENGTH b ⇒
          domain (alist_insert a b locs) = domain locs ∪ set a
   
   [domain_delete]  Theorem
      
      ⊢ domain (delete k t) = domain t DELETE k
   
   [domain_difference]  Theorem
      
      ⊢ ∀t1 t2. domain (difference t1 t2) = domain t1 DIFF domain t2
   
   [domain_empty]  Theorem
      
      ⊢ ∀t. wf t ⇒ (isEmpty t ⇔ domain t = ∅)
   
   [domain_eq]  Theorem
      
      ⊢ ∀t1 t2.
          domain t1 = domain t2 ⇔
          ∀k. lookup k t1 = NONE ⇔ lookup k t2 = NONE
   
   [domain_foldi]  Theorem
      
      ⊢ domain t = foldi (λk v a. k INSERT a) 0 ∅ t
   
   [domain_fromAList]  Theorem
      
      ⊢ ∀ls. domain (fromAList ls) = set (MAP FST ls)
   
   [domain_fromList]  Theorem
      
      ⊢ domain (fromList l) = count (LENGTH l)
   
   [domain_insert]  Theorem
      
      ⊢ domain (insert k v t) = k INSERT domain t
   
   [domain_inter]  Theorem
      
      ⊢ domain (inter t1 t2) = domain t1 ∩ domain t2
   
   [domain_list_insert]  Theorem
      
      ⊢ ∀xs x t. x ∈ domain (list_insert xs t) ⇔ MEM x xs ∨ x ∈ domain t
   
   [domain_list_to_num_set]  Theorem
      
      ⊢ ∀xs. x ∈ domain (list_to_num_set xs) ⇔ MEM x xs
   
   [domain_lookup]  Theorem
      
      ⊢ ∀t k. k ∈ domain t ⇔ ∃v. lookup k t = SOME v
   
   [domain_map]  Theorem
      
      ⊢ ∀s. domain (map f s) = domain s
   
   [domain_mapi]  Theorem
      
      ⊢ domain (mapi f x) = domain x
   
   [domain_mk_wf]  Theorem
      
      ⊢ ∀t. domain (mk_wf t) = domain t
   
   [domain_sing]  Theorem
      
      ⊢ domain (insert k v LN) = {k}
   
   [domain_union]  Theorem
      
      ⊢ domain (union t1 t2) = domain t1 ∪ domain t2
   
   [expand_rle_append]  Theorem
      
      ⊢ expand_rle (xs ⧺ ys) = expand_rle xs ⧺ expand_rle ys
   
   [expand_rle_combine_rle]  Theorem
      
      ⊢ ∀P xs. expand_rle (combine_rle P xs) = expand_rle xs
   
   [expand_rle_map]  Theorem
      
      ⊢ expand_rle (MAP (λ(i,x). (i,f x)) xs) = MAP f (expand_rle xs)
   
   [foldi_FOLDR_toAList]  Theorem
      
      ⊢ ∀f a t. foldi f 0 a t = FOLDR (UNCURRY f) a (toAList t)
   
   [fromAList_append]  Theorem
      
      ⊢ ∀l1 l2. fromAList (l1 ⧺ l2) = union (fromAList l1) (fromAList l2)
   
   [fromAList_def]  Theorem
      
      ⊢ isEmpty (fromAList []) ∧
        ∀y xs x. fromAList ((x,y)::xs) = insert x y (fromAList xs)
   
   [fromAList_ind]  Theorem
      
      ⊢ ∀P. P [] ∧ (∀x y xs. P xs ⇒ P ((x,y)::xs)) ⇒ ∀v. P v
   
   [fromAList_toAList]  Theorem
      
      ⊢ ∀t. wf t ⇒ fromAList (toAList t) = t
   
   [fromList_fromAList]  Theorem
      
      ⊢ ∀l. fromList l = fromAList (ZIP (COUNT_LIST (LENGTH l),l))
   
   [fst_spt_centers_imp]  Theorem
      
      ⊢ ∀i xs j ys.
          spt_centers i xs = (j,ys) ⇒ j = i + LENGTH (expand_rle xs)
   
   [insert_compute]  Theorem
      
      ⊢ 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
   
   [insert_def]  Theorem
      
      ⊢ (∀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)
   
   [insert_fromList_IN_domain]  Theorem
      
      ⊢ ∀ls k v.
          k < LENGTH ls ⇒
          insert k v (fromList ls) =
          fromList (TAKE k ls ⧺ [v] ⧺ DROP (SUC k) ls)
   
   [insert_ind]  Theorem
      
      ⊢ ∀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
   
   [insert_insert]  Theorem
      
      ⊢ ∀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)
   
   [insert_mk_wf]  Theorem
      
      ⊢ ∀x v t. insert x v (mk_wf t) = mk_wf (insert x v t)
   
   [insert_notEmpty]  Theorem
      
      ⊢ insert k a t ≠ LN
   
   [insert_shadow]  Theorem
      
      ⊢ ∀t a b c. insert a b (insert a c t) = insert a b t
   
   [insert_swap]  Theorem
      
      ⊢ ∀t a b c d.
          a ≠ c ⇒ insert a b (insert c d t) = insert c d (insert a b t)
   
   [insert_unchanged]  Theorem
      
      ⊢ ∀t x. lookup x t = SOME y ⇒ insert x y t = t
   
   [insert_union]  Theorem
      
      ⊢ ∀k v s. insert k v s = union (insert k v LN) s
   
   [inter_LN]  Theorem
      
      ⊢ ∀t. isEmpty (inter t LN) ∧ isEmpty (inter LN t)
   
   [inter_assoc]  Theorem
      
      ⊢ ∀t1 t2 t3. inter t1 (inter t2 t3) = inter (inter t1 t2) t3
   
   [inter_eq]  Theorem
      
      ⊢ ∀t1 t2 t3 t4.
          inter t1 t2 = inter t3 t4 ⇔
          ∀x. lookup x (inter t1 t2) = lookup x (inter t3 t4)
   
   [inter_eq_LN]  Theorem
      
      ⊢ ∀x y. isEmpty (inter x y) ⇔ DISJOINT (domain x) (domain y)
   
   [inter_mk_wf]  Theorem
      
      ⊢ ∀t1 t2. inter (mk_wf t1) (mk_wf t2) = mk_wf (inter t1 t2)
   
   [isEmpty_toList]  Theorem
      
      ⊢ ∀t. wf t ⇒ (isEmpty t ⇔ toList t = [])
   
   [isEmpty_toListA]  Theorem
      
      ⊢ ∀t acc. wf t ⇒ (isEmpty t ⇔ toListA acc t = acc)
   
   [isEmpty_union]  Theorem
      
      ⊢ isEmpty (union m1 m2) ⇔ isEmpty m1 ∧ isEmpty m2
   
   [list_size_APPEND]  Theorem
      
      ⊢ list_size f (xs ⧺ ys) = list_size f xs + list_size f ys
   
   [list_to_num_set_append]  Theorem
      
      ⊢ ∀l1 l2.
          list_to_num_set (l1 ⧺ l2) =
          union (list_to_num_set l1) (list_to_num_set l2)
   
   [lookup_0_spt_center]  Theorem
      
      ⊢ ∀spt. lookup 0 spt = spt_center spt
   
   [lookup_FOLDL_union]  Theorem
      
      ⊢ lookup k (FOLDL union t ls) =
        FOLDL OPTION_CHOICE (lookup k t) (MAP (lookup k) ls)
   
   [lookup_NONE_domain]  Theorem
      
      ⊢ lookup k t = NONE ⇔ k ∉ domain t
   
   [lookup_SOME_left_right_cases]  Theorem
      
      ⊢ lookup i spt = SOME v ⇔
        i = 0 ∧ spt_center spt = SOME v ∨
        (∃j. i = j * 2 + 1 ∧ lookup j (spt_right spt) = SOME v) ∨
        ∃j. i = j * 2 + 2 ∧ lookup j (spt_left spt) = SOME v
   
   [lookup_alist_insert]  Theorem
      
      ⊢ ∀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_compute]  Theorem
      
      ⊢ 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
   
   [lookup_def]  Theorem
      
      ⊢ (∀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)
   
   [lookup_delete]  Theorem
      
      ⊢ ∀t k1 k2.
          lookup k1 (delete k2 t) = if k1 = k2 then NONE else lookup k1 t
   
   [lookup_difference]  Theorem
      
      ⊢ ∀m1 m2 k.
          lookup k (difference m1 m2) =
          if lookup k m2 = NONE then lookup k m1 else NONE
   
   [lookup_filter_v]  Theorem
      
      ⊢ ∀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
   
   [lookup_fromAList]  Theorem
      
      ⊢ ∀ls x. lookup x (fromAList ls) = ALOOKUP ls x
   
   [lookup_fromAList_toAList]  Theorem
      
      ⊢ ∀t x. lookup x (fromAList (toAList t)) = lookup x t
   
   [lookup_fromList]  Theorem
      
      ⊢ lookup n (fromList l) =
        if n < LENGTH l then SOME (EL n l) else NONE
   
   [lookup_fromList_outside]  Theorem
      
      ⊢ ∀k. LENGTH args ≤ k ⇒ lookup k (fromList args) = NONE
   
   [lookup_ind]  Theorem
      
      ⊢ ∀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
   
   [lookup_insert]  Theorem
      
      ⊢ ∀k2 v t k1.
          lookup k1 (insert k2 v t) =
          if k1 = k2 then SOME v else lookup k1 t
   
   [lookup_insert1]  Theorem
      
      ⊢ ∀k a t. lookup k (insert k a t) = SOME a
   
   [lookup_inter]  Theorem
      
      ⊢ ∀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_inter_EQ]  Theorem
      
      ⊢ (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_inter_alt]  Theorem
      
      ⊢ lookup x (inter t1 t2) =
        if x ∈ domain t2 then lookup x t1 else NONE
   
   [lookup_inter_assoc]  Theorem
      
      ⊢ lookup x (inter t1 (inter t2 t3)) =
        lookup x (inter (inter t1 t2) t3)
   
   [lookup_inter_eq]  Theorem
      
      ⊢ ∀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
   
   [lookup_list_to_num_set]  Theorem
      
      ⊢ ∀xs.
          lookup x (list_to_num_set xs) =
          if MEM x xs then SOME () else NONE
   
   [lookup_map]  Theorem
      
      ⊢ ∀s x. lookup x (map f s) = OPTION_MAP f (lookup x s)
   
   [lookup_map_K]  Theorem
      
      ⊢ ∀t n.
          lookup n (map (K x) t) = if n ∈ domain t then SOME x else NONE
   
   [lookup_mapi]  Theorem
      
      ⊢ lookup k (mapi f pt) = OPTION_MAP (f k) (lookup k pt)
   
   [lookup_mapi0]  Theorem
      
      ⊢ ∀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_mk_BN]  Theorem
      
      ⊢ lookup i (mk_BN t1 t2) =
        if i = 0 then NONE
        else lookup ((i − 1) DIV 2) (if EVEN i then t1 else t2)
   
   [lookup_mk_wf]  Theorem
      
      ⊢ ∀x t. lookup x (mk_wf t) = lookup x t
   
   [lookup_rwts]  Theorem
      
      ⊢ 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_spt_left]  Theorem
      
      ⊢ lookup i (spt_left spt) = lookup (i * 2 + 2) spt
   
   [lookup_spt_right]  Theorem
      
      ⊢ lookup i (spt_right spt) = lookup (i * 2 + 1) spt
   
   [lookup_union]  Theorem
      
      ⊢ ∀m1 m2 k.
          lookup k (union m1 m2) =
          case lookup k m1 of NONE => lookup k m2 | SOME v => SOME v
   
   [lrnext_def]  Theorem
      
      ⊢ ∀n. sptree$lrnext n =
            if n = 0 then 1 else 2 * sptree$lrnext ((n − 1) DIV 2)
   
   [lrnext_eq]  Theorem
      
      ⊢ ∀n. sptree$lrnext n = 2 ** LOG 2 (n + 1)
   
   [lrnext_ind]  Theorem
      
      ⊢ ∀P. (∀n. (n ≠ 0 ⇒ P ((n − 1) DIV 2)) ⇒ P n) ⇒ ∀v. P v
   
   [lrnext_thm]  Theorem
      
      ⊢ 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
   
   [map_LN]  Theorem
      
      ⊢ ∀t. isEmpty (map f t) ⇔ isEmpty t
   
   [map_fromAList]  Theorem
      
      ⊢ map f (fromAList ls) = fromAList (MAP (λ(k,v). (k,f v)) ls)
   
   [map_insert]  Theorem
      
      ⊢ ∀f x y z. map f (insert x y z) = insert x (f y) (map f z)
   
   [map_map_K]  Theorem
      
      ⊢ ∀t. map (K a) (map f t) = map (K a) t
   
   [map_map_o]  Theorem
      
      ⊢ ∀t f g. map f (map g t) = map (f ∘ g) t
   
   [map_union]  Theorem
      
      ⊢ ∀t1 t2. map f (union t1 t2) = union (map f t1) (map f t2)
   
   [mapi_Alist]  Theorem
      
      ⊢ mapi f pt =
        fromAList (MAP (λkv. (FST kv,f (FST kv) (SND kv))) (toAList pt))
   
   [mapi_fromList]  Theorem
      
      ⊢ mapi f (fromList ls) = fromList (MAPi f ls)
   
   [mk_BN_def]  Theorem
      
      ⊢ 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
   
   [mk_BN_ind]  Theorem
      
      ⊢ ∀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_def]  Theorem
      
      ⊢ 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)
   
   [mk_BS_ind]  Theorem
      
      ⊢ ∀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
   
   [mk_wf_eq]  Theorem
      
      ⊢ ∀t1 t2. mk_wf t1 = mk_wf t2 ⇔ ∀x. lookup x t1 = lookup x t2
   
   [num_set_domain_eq]  Theorem
      
      ⊢ ∀t1 t2. wf t1 ∧ wf t2 ⇒ (domain t1 = domain t2 ⇔ t1 = t2)
   
   [set_MAP_FST_toAList_domain]  Theorem
      
      ⊢ set (MAP FST (toAList t)) = domain t
   
   [set_foldi_keys]  Theorem
      
      ⊢ ∀t a i.
          foldi (λk v a. k INSERT a) i a t =
          a ∪ IMAGE (λn. i + sptree$lrnext i * n) (domain t)
   
   [size_delete]  Theorem
      
      ⊢ ∀n t.
          size (delete n t) =
          if lookup n t = NONE then size t else size t − 1
   
   [size_diff_less]  Theorem
      
      ⊢ ∀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)
   
   [size_domain]  Theorem
      
      ⊢ ∀t. size t = CARD (domain t)
   
   [size_fromList]  Theorem
      
      ⊢ size (fromList ls) = LENGTH ls
   
   [size_insert]  Theorem
      
      ⊢ ∀k v m.
          size (insert k v m) = if k ∈ domain m then size m else size m + 1
   
   [size_map]  Theorem
      
      ⊢ size (map f t) = size t
   
   [size_mapi]  Theorem
      
      ⊢ size (mapi f t) = size t
   
   [size_zero_empty]  Theorem
      
      ⊢ ∀x. size x = 0 ⇔ domain x = ∅
   
   [spt_11]  Theorem
      
      ⊢ (∀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'
   
   [spt_Axiom]  Theorem
      
      ⊢ ∀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)
   
   [spt_acc_0]  Theorem
      
      ⊢ ∀k. spt_acc 0 k = k
   
   [spt_acc_compute]  Theorem
      
      ⊢ (∀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)
   
   [spt_acc_def]  Theorem
      
      ⊢ (∀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)
   
   [spt_acc_eqn]  Theorem
      
      ⊢ ∀k i. spt_acc i k = sptree$lrnext i * k + i
   
   [spt_acc_ind]  Theorem
      
      ⊢ ∀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_thm]  Theorem
      
      ⊢ 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)
   
   [spt_case_cong]  Theorem
      
      ⊢ ∀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_eq]  Theorem
      
      ⊢ 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_def]  Theorem
      
      ⊢ spt_center ⦕ 0 ↦ x ⦖ = SOME x ∧ spt_center (BS t1 x t2) = SOME x ∧
        spt_center LN = NONE ∧ spt_center (BN v1 v2) = NONE
   
   [spt_center_ind]  Theorem
      
      ⊢ ∀P. (∀x. P ⦕ 0 ↦ x ⦖) ∧ (∀t1 x t2. P (BS t1 x t2)) ∧ P LN ∧
            (∀v1 v2. P (BN v1 v2)) ⇒
            ∀v. P v
   
   [spt_centers_def]  Theorem
      
      ⊢ (∀i. spt_centers i [] = (i,[])) ∧
        ∀xs x j i.
          spt_centers i ((j,x)::xs) =
          case spt_center x of
            NONE => spt_centers (i + j) xs
          | SOME y => apsnd_cons (i,y) (spt_centers (i + j) xs)
   
   [spt_centers_expand_rle]  Theorem
      
      ⊢ ∀i xs.
          rle_wf xs ⇒
          ∀j x.
            MEM (j,x) (SND (spt_centers i xs)) ⇔
            ∃k. j = i + k ∧ k < LENGTH (expand_rle xs) ∧
                spt_center (EL k (expand_rle xs)) = SOME x
   
   [spt_centers_expand_rle_imp]  Theorem
      
      ⊢ ∀n xs.
          spt_centers n xs = (n2,centers) ∧ rle_wf xs ⇒
          ∀j x.
            MEM (j,x) centers ⇔
            ∃k. j = n + k ∧ k < LENGTH (expand_rle xs) ∧
                spt_center (EL k (expand_rle xs)) = SOME x
   
   [spt_centers_ind]  Theorem
      
      ⊢ ∀P. (∀i. P i []) ∧
            (∀i j x xs.
               (∀y. spt_center x = SOME y ⇒ P (i + j) xs) ∧
               (spt_center x = NONE ⇒ P (i + j) xs) ⇒
               P i ((j,x)::xs)) ⇒
            ∀v v1. P v v1
   
   [spt_centers_ord]  Theorem
      
      ⊢ ∀n xs n2 ys.
          spt_centers n xs = (n2,ys) ∧ rle_wf xs ⇒
          SORTED $< (MAP FST ys) ∧ (∀k. k ≤ n ⇒ EVERY (λt. FST t ≥ k) ys) ∧
          EVERY (λt. FST t < n2) ys
   
   [spt_distinct]  Theorem
      
      ⊢ (∀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
   
   [spt_eq_thm]  Theorem
      
      ⊢ ∀t1 t2. wf t1 ∧ wf t2 ⇒ (t1 = t2 ⇔ ∀n. lookup n t1 = lookup n t2)
   
   [spt_induction]  Theorem
      
      ⊢ ∀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
   
   [spt_nchotomy]  Theorem
      
      ⊢ ∀ss.
          isEmpty ss ∨ (∃a. ss = ⦕ 0 ↦ a ⦖) ∨ (∃s s0. ss = BN s s0) ∨
          ∃s a s0. ss = BS s a s0
   
   [spts_to_alist_def]  Theorem
      
      ⊢ ∀xs i.
          spts_to_alist i xs =
          (let
             ys = combine_rle (λt. isEmpty t) xs
           in
             if EVERY ((λt. isEmpty t) ∘ SND) ys then []
             else
               (let
                  (j,centers) = spt_centers i ys;
                  rights = MAP (λ(i,t). (i,spt_right t)) ys;
                  lefts = MAP (λ(i,t). (i,spt_left t)) ys
                in
                  centers ⧺ spts_to_alist j (rights ⧺ lefts)))
   
   [spts_to_alist_ind]  Theorem
      
      ⊢ ∀P. (∀i xs.
               (∀ys j centers rights lefts.
                  ys = combine_rle (λt. isEmpty t) xs ∧
                  ¬EVERY ((λt. isEmpty t) ∘ SND) ys ∧
                  (j,centers) = spt_centers i ys ∧
                  rights = MAP (λ(i,t). (i,spt_right t)) ys ∧
                  lefts = MAP (λ(i,t). (i,spt_left t)) ys ⇒
                  P j (rights ⧺ lefts)) ⇒
               P i xs) ⇒
            ∀v v1. P v v1
   
   [subspt_FOLDL_union]  Theorem
      
      ⊢ ∀ls t. subspt t (FOLDL union t ls)
   
   [subspt_LN]  Theorem
      
      ⊢ (subspt LN sp ⇔ T) ∧ (subspt sp LN ⇔ domain sp = ∅)
   
   [subspt_def]  Theorem
      
      ⊢ ∀sp1 sp2.
          subspt sp1 sp2 ⇔
          ∀k. k ∈ domain sp1 ⇒ k ∈ domain sp2 ∧ lookup k sp2 = lookup k sp1
   
   [subspt_domain]  Theorem
      
      ⊢ ∀t1 t2. subspt t1 t2 ⇔ domain t1 ⊆ domain t2
   
   [subspt_lookup]  Theorem
      
      ⊢ ∀t1 t2.
          subspt t1 t2 ⇔ ∀x y. lookup x t1 = SOME y ⇒ lookup x t2 = SOME y
   
   [subspt_refl]  Theorem
      
      ⊢ subspt sp sp
   
   [subspt_trans]  Theorem
      
      ⊢ subspt sp1 sp2 ∧ subspt sp2 sp3 ⇒ subspt sp1 sp3
   
   [subspt_union]  Theorem
      
      ⊢ subspt s (union s t)
   
   [sum_size_combine_rle_LE]  Theorem
      
      ⊢ ∀P xs.
          SUM (MAP (f ∘ SND) (combine_rle P xs)) ≤ SUM (MAP (f ∘ SND) xs)
   
   [toListA_append]  Theorem
      
      ⊢ ∀t acc. toListA acc t = toListA [] t ⧺ acc
   
   [toList_map]  Theorem
      
      ⊢ ∀s. toList (map f s) = MAP f (toList s)
   
   [toSortedAList_fromList]  Theorem
      
      ⊢ toSortedAList (fromList ls) = ZIP (COUNT_LIST (LENGTH ls),ls)
   
   [union_LN]  Theorem
      
      ⊢ ∀t. union t LN = t ∧ union LN t = t
   
   [union_assoc]  Theorem
      
      ⊢ ∀t1 t2 t3. union t1 (union t2 t3) = union (union t1 t2) t3
   
   [union_disjoint_sym]  Theorem
      
      ⊢ ∀t1 t2.
          wf t1 ∧ wf t2 ∧ DISJOINT (domain t1) (domain t2) ⇒
          union t1 t2 = union t2 t1
   
   [union_insert_LN]  Theorem
      
      ⊢ ∀x y t2. union (insert x y LN) t2 = insert x y t2
   
   [union_mk_wf]  Theorem
      
      ⊢ ∀t1 t2. union (mk_wf t1) (mk_wf t2) = mk_wf (union t1 t2)
   
   [union_num_set_sym]  Theorem
      
      ⊢ ∀t1 t2. union t1 t2 = union t2 t1
   
   [wf_LN]  Theorem
      
      ⊢ wf LN
   
   [wf_delete]  Theorem
      
      ⊢ ∀t k. wf t ⇒ wf (delete k t)
   
   [wf_difference]  Theorem
      
      ⊢ ∀t1 t2. wf t1 ∧ wf t2 ⇒ wf (difference t1 t2)
   
   [wf_filter_v]  Theorem
      
      ⊢ ∀t f. wf t ⇒ wf (filter_v f t)
   
   [wf_fromAList]  Theorem
      
      ⊢ ∀ls. wf (fromAList ls)
   
   [wf_fromList]  Theorem
      
      ⊢ wf (fromList ls)
   
   [wf_insert]  Theorem
      
      ⊢ ∀k a t. wf t ⇒ wf (insert k a t)
   
   [wf_inter]  Theorem
      
      ⊢ ∀m1 m2. wf (inter m1 m2)
   
   [wf_map]  Theorem
      
      ⊢ ∀t f. wf (map f t) ⇔ wf t
   
   [wf_mapi]  Theorem
      
      ⊢ wf (mapi f pt)
   
   [wf_mk_BN]  Theorem
      
      ⊢ wf t1 ∧ wf t2 ⇒ wf (mk_BN t1 t2)
   
   [wf_mk_BS]  Theorem
      
      ⊢ wf t1 ∧ wf t2 ⇒ wf (mk_BS t1 a t2)
   
   [wf_mk_id]  Theorem
      
      ⊢ ∀t. wf t ⇒ mk_wf t = t
   
   [wf_mk_wf]  Theorem
      
      ⊢ ∀t. wf (mk_wf t)
   
   [wf_union]  Theorem
      
      ⊢ ∀m1 m2. wf m1 ∧ wf m2 ⇒ wf (union m1 m2)
   
   
*)
end


Source File Identifier index Theory binding index

HOL 4, Trindemossen-1