Theory "sptree"

Signature

Definitions

wf_def

⊢ (wf LN ⇔ T) ∧ (∀a. wf (LS 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)

union_def

⊢ (∀t. union LN t = t) ∧
  (∀a t.
       union (LS a) t =
       case t of
         LN => LS a
       | LS b => LS 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
       | LS 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
      | LS 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'')

toSortedAList_def

⊢ ∀spt. toSortedAList spt = aux_alist 0 [spt]

toListA_def

⊢ (∀acc. toListA acc LN = acc) ∧ (∀acc a. toListA acc (LS 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

⊢ ∀m. toList m = toListA [] m

toAList_def

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

spt_TY_DEF

⊢ ∃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_size_def

⊢ (∀f. spt_size f LN = 0) ∧ (∀f a. spt_size f (LS 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))

spt_size_alt_def

⊢ (spt_size_alt LN = 0) ∧ (∀a. spt_size_alt (LS a) = 1) ∧
  (∀t1 t2. spt_size_alt (BN t1 t2) = spt_size_alt t1 + spt_size_alt t2 + 1) ∧
  ∀t1 a t2. spt_size_alt (BS t1 a t2) = spt_size_alt t1 + spt_size_alt t2 + 1

spt_right_def

⊢ isEmpty (spt_right LN) ∧ (∀x. isEmpty (spt_right (LS x))) ∧
  (∀t1 t2. spt_right (BN t1 t2) = t2) ∧ ∀t1 x t2. spt_right (BS t1 x t2) = t2

spt_left_def

⊢ isEmpty (spt_left LN) ∧ (∀x. isEmpty (spt_left (LS x))) ∧
  (∀t1 t2. spt_left (BN t1 t2) = t1) ∧ ∀t1 x t2. spt_left (BS t1 x t2) = t1

spt_fold_def

⊢ (∀f acc. spt_fold f acc LN = acc) ∧
  (∀f acc a. spt_fold f acc (LS 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_centers_def

⊢ (∀i. spt_centers i [] = []) ∧
  ∀i x xs.
      spt_centers i (x::xs) =
      (case spt_center x of NONE => [] | SOME y => [(i,y)]) ++
      spt_centers (SUC i) xs

spt_center_primitive_def

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

spt_case_def

⊢ (∀v f f1 f2. spt_CASE LN v f f1 f2 = v) ∧
  (∀a v f f1 f2. spt_CASE (LS 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

size_def

⊢ (size LN = 0) ∧ (∀a. size (LS 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

mk_wf_def

⊢ isEmpty (mk_wf LN) ∧ (∀x. mk_wf (LS x) = LS 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)

mapi_def

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

mapi0_def

⊢ (∀f i. isEmpty (mapi0 f i LN)) ∧ (∀f i a. mapi0 f i (LS a) = LS (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))

map_def

⊢ (∀f. isEmpty (map f LN)) ∧ (∀f a. map f (LS a) = LS (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)

lrnext_primitive_def

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

list_to_num_set_def

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

list_insert_def

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

inter_eq_def

⊢ (∀t. isEmpty (inter_eq LN t)) ∧
  (∀a t.
       inter_eq (LS a) t =
       case t of
         LN => LN
       | LS b => if a = b then LS a else LN
       | BN t1 t2 => LN
       | BS t1' b' t2' => if a = b' then LS a else LN) ∧
  (∀t1 t2 t.
       inter_eq (BN t1 t2) t =
       case t of
         LN => LN
       | LS 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
      | LS a' => if a' = a then LS 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'')

inter_def

⊢ (∀t. isEmpty (inter LN t)) ∧
  (∀a t.
       inter (LS a) t =
       case t of
         LN => LN
       | LS b => LS a
       | BN t1 t2 => LN
       | BS t1' v4 t2' => LS a) ∧
  (∀t1 t2 t.
       inter (BN t1 t2) t =
       case t of
         LN => LN
       | LS 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
      | LS a' => LS 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'')

fromList_def

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

fromAList_primitive_def

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

foldi_def

⊢ (∀f i acc. foldi f i acc LN = acc) ∧
  (∀f i acc a. foldi f i acc (LS 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)

filter_v_def

⊢ (∀f. isEmpty (filter_v f LN)) ∧
  (∀f x. filter_v f (LS x) = if f x then LS 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)

domain_def

⊢ (domain LN = ∅) ∧ (∀v0. domain (LS 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)

difference_def

⊢ (∀t. isEmpty (difference LN t)) ∧
  (∀a t.
       difference (LS a) t =
       case t of
         LN => LS a
       | LS b => LN
       | BN t1 t2 => LS a
       | BS t1' b' t2' => LN) ∧
  (∀t1 t2 t.
       difference (BN t1 t2) t =
       case t of
         LN => BN t1 t2
       | LS 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
      | LS 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'')

delete_def

⊢ (∀k. isEmpty (delete k LN)) ∧
  (∀k a. delete k (LS a) = if k = 0 then LN else LS 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)

Theorems

wf_union

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

wf_mk_wf

⊢ ∀t. wf (mk_wf t)

wf_mk_id

⊢ ∀t. wf t ⇒ (mk_wf t = t)

wf_mk_BS

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

wf_mk_BN

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

wf_mapi

⊢ wf (mapi f pt)

wf_map

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

wf_LN

⊢ wf LN

wf_inter

⊢ ∀m1 m2. wf (inter m1 m2)

wf_insert

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

wf_fromAList

⊢ ∀ls. wf (fromAList ls)

wf_filter_v

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

wf_difference

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

wf_delete

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

union_num_set_sym

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

union_mk_wf

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

union_LN

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

union_insert_LN

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

union_assoc

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

toListA_append

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

toList_map

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

sum_spt_size_less

⊢ EXISTS ($~ ∘ (λx. isEmpty x)) xs ⇒
  SUM (MAP (spt_size_alt ∘ spt_left) xs) +
  SUM (MAP (spt_size_alt ∘ spt_right) xs) < SUM (MAP spt_size_alt xs)

sum_spt_size_alt_lemma

⊢ let
    mksum f = SUM (MAP (spt_size_alt ∘ f) xs) ;
    tsum = mksum spt_left + mksum spt_right
  in
    tsum ≤ mksum I ∧ (EXISTS ($~ ∘ (λx. isEmpty x)) xs ⇒ tsum < mksum I)

subspt_union

⊢ subspt s (union s t)

subspt_trans

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

subspt_refl

⊢ subspt sp sp

subspt_lookup

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

subspt_LN

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

subspt_FOLDL_union

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

subspt_eq

⊢ (∀t. subspt LN t ⇔ T) ∧ (∀x t. subspt (LS 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)

subspt_domain

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

subspt_def

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

spt_nchotomy

⊢ ∀ss.
      isEmpty ss ∨ (∃a. ss = LS a) ∨ (∃s s0. ss = BN s s0) ∨
      ∃s a s0. ss = BS s a s0

spt_induction

⊢ ∀P.
      P LN ∧ (∀a. P (LS 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_eq_thm

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

spt_distinct

⊢ (∀a. LN ≠ LS a) ∧ (∀a1 a0. LN ≠ BN a0 a1) ∧ (∀a2 a1 a0. LN ≠ BS a0 a1 a2) ∧
  (∀a1 a0 a. LS a ≠ BN a0 a1) ∧ (∀a2 a1 a0 a. LS a ≠ BS a0 a1 a2) ∧
  ∀a2 a1' a1 a0' a0. BN a0 a1 ≠ BS a0' a1' a2

spt_centers_eq_map

⊢ ∀xs i.
      spt_centers i xs =
      MAP THE
        (FILTER (λx. x ≠ NONE)
           (MAPi
              (λj t.
                   case spt_center t of
                     NONE => NONE
                   | SOME x => SOME (i + j,x)) xs))

spt_centers_add_lemma

⊢ ∀xs i j. MAP (λ(j,v). (i + j,v)) (spt_centers j xs) = spt_centers (i + j) xs

spt_center_ind

⊢ ∀P.
      (∀x. P (LS x)) ∧ (∀t1 x t2. P (BS t1 x t2)) ∧ P LN ∧
      (∀v1 v2. P (BN v1 v2)) ⇒
      ∀v. P v

spt_center_def

⊢ (spt_center (LS x) = SOME x) ∧ (spt_center (BS t1 x t2) = SOME x) ∧
  (spt_center LN = NONE) ∧ (spt_center (BN v1 v2) = NONE)

spt_case_eq

⊢ (spt_CASE x v f f1 f2 = v') ⇔
  isEmpty x ∧ (v = v') ∨ (∃a. (x = LS 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_case_cong

⊢ ∀M M' v f f1 f2.
      (M = M') ∧ (isEmpty M' ⇒ (v = v')) ∧ (∀a. (M' = LS 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_Axiom

⊢ ∀f0 f1 f2 f3.
      ∃fn.
          (fn LN = f0) ∧ (∀a. fn (LS 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_thm

⊢ 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_acc_ind

⊢ ∀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_eqn

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

spt_acc_def

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

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

⊢ ∀k. spt_acc 0 k = k

spt_11

⊢ (∀a a'. (LS a = LS 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')

SORTED_spt_centers

⊢ ∀xs i. SORTED $< (MAP FST (spt_centers i xs))

SORTED_MAP_FST_toSortedAList

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

SORTED_MAP_FST_alist_aux

⊢ ∀i. SORTED $< (MAP FST (aux_alist i xs))

size_insert

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

size_domain

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

size_diff_less

⊢ ∀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_delete

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

set_foldi_keys

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

num_set_domain_eq

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

mk_wf_eq

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

mk_BS_ind

⊢ ∀P.
      (∀x. P LN x LN) ∧ (∀v16 x. P (LS 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 (LS 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_BS_def

⊢ (mk_BS LN x LN = LS x) ∧ (mk_BS (LS v16) x LN = BS (LS v16) x LN) ∧
  (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 (LS v4) = BS t1 x (LS 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_BN_ind

⊢ ∀P.
      P LN LN ∧ (∀v14. P LN (LS v14)) ∧ (∀v15 v16. P LN (BN v15 v16)) ∧
      (∀v17 v18 v19. P LN (BS v17 v18 v19)) ∧ (∀v2 t2. P (LS 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_BN_def

⊢ isEmpty (mk_BN LN LN) ∧ (mk_BN LN (LS v14) = BN LN (LS 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 (LS v2) t2 = BN (LS 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)

MEM_toSortedAList

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

MEM_toList

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

MEM_toAList

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

MEM_FST_ALOOKUP_SOME

⊢ MEM x xs ⇒ ∃y. ALOOKUP xs (FST x) = SOME y

mapi_Alist

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

map_union

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

map_map_o

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

map_map_K

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

map_LN

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

map_insert

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

map_fromAList

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

MAP_foldi

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

lrnext_thm

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

lrnext_ind

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

lrnext_def

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

lookup_union

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

lookup_spt_right

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

lookup_spt_left

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

lookup_NONE_domain

⊢ (lookup k t = NONE) ⇔ k ∉ domain t

lookup_mk_wf

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

lookup_mk_BN

⊢ 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_mapi0

⊢ ∀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_mapi

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

lookup_map_K

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

lookup_map

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

lookup_list_to_num_set

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

lookup_inter_eq

⊢ ∀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_inter_EQ

⊢ ((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_assoc

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

lookup_inter_alt

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

lookup_inter

⊢ ∀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_insert1

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

lookup_insert

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

lookup_ind

⊢ ∀P.
      (∀k. P k LN) ∧ (∀k a. P k (LS 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_fromList_outside

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

lookup_fromList

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

lookup_fromAList_toAList

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

lookup_fromAList

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

lookup_FOLDL_union

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

lookup_filter_v

⊢ ∀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_difference

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

lookup_delete

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

lookup_def

⊢ (∀k. lookup k LN = NONE) ∧
  (∀k a. lookup k (LS 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_compute

⊢ (lookup (NUMERAL n) t = lookup n t) ∧ (lookup 0 LN = NONE) ∧
  (lookup 0 (LS a) = SOME a) ∧ (lookup 0 (BN t1 t2) = NONE) ∧
  (lookup 0 (BS t1 a t2) = SOME a) ∧ (lookup ZERO LN = NONE) ∧
  (lookup ZERO (LS 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) (LS 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) (LS a) = NONE) ∧
  (lookup (BIT2 n) (BN t1 t2) = lookup n t1) ∧
  (lookup (BIT2 n) (BS t1 a t2) = lookup n t1)

lookup_alist_insert

⊢ ∀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_0_spt_center

⊢ ∀spt. lookup 0 spt = spt_center spt

list_to_num_set_append

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

list_size_APPEND

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

LESS_spt_centers

⊢ ∀xs i. MEM p (spt_centers i xs) ⇒ FST p < i + LENGTH xs

isEmpty_union

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

isEmpty_toListA

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

isEmpty_toList

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

inter_mk_wf

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

inter_LN

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

inter_eq_LN

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

inter_eq

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

inter_assoc

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

insert_union

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

insert_unchanged

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

insert_swap

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

insert_shadow

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

insert_notEmpty

⊢ insert k a t ≠ LN

insert_mk_wf

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

insert_insert

⊢ ∀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_ind

⊢ ∀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 (LS 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_def

⊢ (∀k a.
       insert k a LN =
       if k = 0 then LS 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 (LS a') =
       if k = 0 then LS 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_compute

⊢ (insert (NUMERAL n) a t = insert n a t) ∧ (insert 0 a LN = LS a) ∧
  (insert 0 a (LS a') = LS 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 = LS a) ∧
  (insert ZERO a (LS a') = LS 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 (LS 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 (LS 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)

IN_domain

⊢ ∀n x t1 t2.
      (n ∈ domain LN ⇔ F) ∧ (n ∈ domain (LS 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)

IMP_size_LESS_size

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

GREATER_EQ_alist_aux

⊢ MEM x (aux_alist i xs) ⇒ i ≤ FST x

fromAList_toAList

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

fromAList_ind

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

fromAList_def

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

fromAList_append

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

foldi_FOLDR_toAList

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

FINITE_domain

⊢ FINITE (domain t)

EL_CONS_IF

⊢ EL n (x::xs) = if n = 0 then x else EL (PRE n) xs

domain_union

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

domain_sing

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

domain_mk_wf

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

domain_mapi

⊢ domain (mapi f x) = domain x

domain_map

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

domain_lookup

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

domain_list_to_num_set

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

domain_list_insert

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

domain_inter

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

domain_insert

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

domain_fromList

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

domain_fromAList

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

domain_FOLDR_delete

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

domain_foldi

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

domain_eq

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

domain_empty

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

domain_difference

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

domain_delete

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

domain_alist_insert

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

DIV_MOD_TIMES_2

⊢ ∀n i.
      0 < n ⇒
      (i DIV n = 2 * (i DIV (2 * n)) + if i MOD (2 * n) < n then 0 else 1) ∧
      (i MOD n = i MOD (2 * n) − if i MOD (2 * n) < n then 0 else n)

difference_sub

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

delete_mk_wf

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

delete_fail

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

delete_compute

⊢ (delete (NUMERAL n) t = delete n t) ∧ isEmpty (delete 0 LN) ∧
  isEmpty (delete 0 (LS 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 (LS 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) (LS a) = LS 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) (LS a) = LS 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)

datatype_spt

⊢ DATATYPE (spt LN LS BN BS)

aux_alist_ind

⊢ ∀P.
      (∀i xs.
           (¬EVERY (λx. isEmpty x) xs ⇒
            P (LENGTH xs + i) (MAP spt_right xs ++ MAP spt_left xs)) ⇒
           P i xs) ⇒
      ∀v v1. P v v1

aux_alist_def

⊢ ∀xs i.
      aux_alist i xs =
      if EVERY (λx. isEmpty x) xs then []
      else
        spt_centers i xs ++
        aux_alist (LENGTH xs + i) (MAP spt_right xs ++ MAP spt_left xs)

ALOOKUP_toSortedAList

⊢ ALOOKUP (toSortedAList t) k = lookup k t

ALOOKUP_toAList

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

ALOOKUP_spt_centers

⊢ ∀i j.
      ALOOKUP (spt_centers j xs) i =
      if j ≤ i ∧ i − j < LENGTH xs then spt_center (EL (i − j) xs) else NONE

ALOOKUP_aux_alist

⊢ ∀i j.
      LENGTH xs > 0 ⇒
      (ALOOKUP (aux_alist j xs) i =
       if i < j then NONE
       else lookup ((i − j) DIV LENGTH xs) (EL ((i − j) MOD LENGTH xs) xs))

ALL_DISTINCT_MAP_FST_toAList

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

alist_insert_REVERSE

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

alist_insert_pull_insert

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

alist_insert_ind

⊢ ∀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_def

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

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

ADD_1_SUC

⊢ (N + 1 = SUC N) ∧ (1 + N = SUC N)