Structure cv_stdTheory
signature cv_stdTheory =
sig
type thm = Thm.thm
(* Definitions *)
val FOLDL_lam_lam_pair_CASE_lam_la_def : thm
val combine_rle_isEmpty_def : thm
val cv_ALL_DISTINCT_def : thm
val cv_ALOOKUP_def : thm
val cv_DROP_def : thm
val cv_EL_def : thm
val cv_FLAT_def_primitive : thm
val cv_FOLDL_lam_lam_pair_CASE_lam_la_def : thm
val cv_FRONT_def_primitive : thm
val cv_ISL_def : thm
val cv_ISR_def : thm
val cv_LAST_def : thm
val cv_LENGTH_def : thm
val cv_LEN_def : thm
val cv_NULL_def : thm
val cv_OUTL_def : thm
val cv_OUTR_def : thm
val cv_PAD_LEFT_def : thm
val cv_PAD_RIGHT_def : thm
val cv_REPLICATE_def : thm
val cv_REVERSE_def : thm
val cv_REV_def : thm
val cv_SUM_ACC_def : thm
val cv_SUM_def : thm
val cv_UNZIP_def_primitive : thm
val cv_ZIP_def_primitive : thm
val cv_apsnd_cons_def : thm
val cv_combine_rle_isEmpty_def_primitive : thm
val cv_every_empty_snd_def : thm
val cv_fromList_def : thm
val cv_isPREFIX_def : thm
val cv_list_insert_def : thm
val cv_list_mem_def : thm
val cv_list_to_num_set_def_primitive : thm
val cv_lookup_def : thm
val cv_lrnext_def_primitive : thm
val cv_map_fst_def_primitive : thm
val cv_map_snd_def_primitive : thm
val cv_mk_BN_def : thm
val cv_mk_BS_def : thm
val cv_mk_wf_def_primitive : thm
val cv_nub_def_primitive : thm
val cv_oEL_def : thm
val cv_oHD_def : thm
val cv_replicate_acc_def : thm
val cv_right_depth_def : thm
val cv_size'_def_primitive : thm
val cv_spt_center_def : thm
val cv_spt_left_def : thm
val cv_spt_right_def : thm
val cv_subspt_def_tupled_AUX : thm
val cv_toAList_def : thm
val cv_toAList_foldi_def_tupled_AUX : thm
val cv_toListA_def_tupled_AUX : thm
val cv_toList_def : thm
val cv_v2n_custom_def : thm
val every_empty_snd_def_primitive : thm
val from_fmap_def : thm
val from_sptree_sptree_spt_def : thm
val genlist_def : thm
val list_mapi_def : thm
val list_mem_def : thm
val map_spt_left_def_primitive : thm
val map_spt_right_def_primitive : thm
val toAList_foldi_def : thm
val to_fmap_def : thm
(* Theorems *)
val EL_pre : thm
val EL_pre_cases : thm
val EL_pre_ind : thm
val EL_pre_rules : thm
val EL_pre_strongind : thm
val FOLDL_lam_lam_pair_CASE_lam_la_ho : thm
val FRONT_pre : thm
val FRONT_pre_cases : thm
val FRONT_pre_ind : thm
val FRONT_pre_rules : thm
val FRONT_pre_strongind : thm
val INDEX_OF_pre_cases : thm
val INDEX_OF_pre_ind : thm
val INDEX_OF_pre_rules : thm
val INDEX_OF_pre_strongind : thm
val I_THM : thm
val K_THM : thm
val LAST_pre : thm
val LAST_pre_cases : thm
val LAST_pre_ind : thm
val LAST_pre_rules : thm
val LAST_pre_strongind : thm
val MAPi_eq_list_mapi : thm
val OUTL_pre : thm
val OUTL_pre_cases : thm
val OUTL_pre_ind : thm
val OUTL_pre_rules : thm
val OUTL_pre_strongind : thm
val OUTR_pre : thm
val OUTR_pre_cases : thm
val OUTR_pre_ind : thm
val OUTR_pre_rules : thm
val OUTR_pre_strongind : thm
val REPLICATE : thm
val UNZIP_eq : thm
val combine_rle_isEmpty_eq : thm
val combine_rle_isEmpty_pre : thm
val combine_rle_isEmpty_pre_cases : thm
val combine_rle_isEmpty_pre_ind : thm
val combine_rle_isEmpty_pre_rules : thm
val combine_rle_isEmpty_pre_strongind : thm
val cv_ALL_DISTINCT_thm : thm
val cv_ALOOKUP_thm : thm
val cv_APPEND_def : thm
val cv_APPEND_ind : thm
val cv_APPEND_thm : thm
val cv_DROP_thm : thm
val cv_EL_thm : thm
val cv_FLAT_def : thm
val cv_FLAT_ind : thm
val cv_FLAT_thm : thm
val cv_FOLDL_lam_lam_pair_CASE_lam_la_thm : thm
val cv_FRONT_def : thm
val cv_FRONT_ind : thm
val cv_FRONT_thm : thm
val cv_FST : thm
val cv_HD : thm
val cv_INDEX_OF_def : thm
val cv_INDEX_OF_ind : thm
val cv_INDEX_OF_thm : thm
val cv_ISL_thm : thm
val cv_ISR_thm : thm
val cv_IS_NONE : thm
val cv_IS_SOME : thm
val cv_LAST_thm : thm
val cv_LENGTH_thm : thm
val cv_LEN_thm : thm
val cv_LUPDATE_def : thm
val cv_LUPDATE_ind : thm
val cv_LUPDATE_thm : thm
val cv_MAP_FST : thm
val cv_MAP_SND : thm
val cv_NULL_thm : thm
val cv_OUTL_thm : thm
val cv_OUTR_thm : thm
val cv_PAD_LEFT_thm : thm
val cv_PAD_RIGHT_thm : thm
val cv_REPLICATE_thm : thm
val cv_REVERSE_thm : thm
val cv_REV_thm : thm
val cv_SND : thm
val cv_SNOC_def : thm
val cv_SNOC_ind : thm
val cv_SNOC_thm : thm
val cv_SUM_ACC_thm : thm
val cv_SUM_thm : thm
val cv_TAKE_def : thm
val cv_TAKE_ind : thm
val cv_TAKE_thm : thm
val cv_THE : thm
val cv_TL : thm
val cv_UNZIP_def : thm
val cv_UNZIP_ind : thm
val cv_UNZIP_thm : thm
val cv_ZIP_def : thm
val cv_ZIP_ind : thm
val cv_ZIP_thm : thm
val cv_alist_insert_def : thm
val cv_alist_insert_ind : thm
val cv_alist_insert_thm : thm
val cv_apsnd_cons_thm : thm
val cv_combine_rle_isEmpty_def : thm
val cv_combine_rle_isEmpty_ind : thm
val cv_combine_rle_isEmpty_thm : thm
val cv_delete_def : thm
val cv_delete_ind : thm
val cv_delete_thm : thm
val cv_difference_def : thm
val cv_difference_ind : thm
val cv_difference_thm : thm
val cv_every_empty_snd_thm : thm
val cv_findi_def : thm
val cv_findi_ind : thm
val cv_findi_thm : thm
val cv_fromList_thm : thm
val cv_insert_def : thm
val cv_insert_ind : thm
val cv_insert_thm : thm
val cv_inter_def : thm
val cv_inter_ind : thm
val cv_inter_thm : thm
val cv_isPREFIX_thm : thm
val cv_list_insert_thm : thm
val cv_list_mem_thm : thm
val cv_list_to_num_set_def : thm
val cv_list_to_num_set_ind : thm
val cv_list_to_num_set_thm : thm
val cv_lookup_thm : thm
val cv_lrnext_def : thm
val cv_lrnext_ind : thm
val cv_lrnext_thm : thm
val cv_map_fst_def : thm
val cv_map_fst_ind : thm
val cv_map_snd_def : thm
val cv_map_snd_ind : thm
val cv_mk_BN_thm : thm
val cv_mk_BS_thm : thm
val cv_mk_wf_def : thm
val cv_mk_wf_ind : thm
val cv_mk_wf_thm : thm
val cv_nub_def : thm
val cv_nub_ind : thm
val cv_nub_thm : thm
val cv_oEL_thm : thm
val cv_oHD_thm : thm
val cv_rep_FEMPTY : thm
val cv_rep_FLOOKUP : thm
val cv_rep_FUPDATE : thm
val cv_rep_MEM : thm
val cv_rep_list_datatype : thm
val cv_rep_option_datatype : thm
val cv_rep_pair_datatype : thm
val cv_rep_sptree_sptree_spt_datatype : thm
val cv_rep_sum_datatype : thm
val cv_rep_unit_datatype : thm
val cv_replicate_acc_thm : thm
val cv_size'_def : thm
val cv_size'_ind : thm
val cv_size'_thm : thm
val cv_spt_center_thm : thm
val cv_spt_centers_def : thm
val cv_spt_centers_ind : thm
val cv_spt_centers_thm : thm
val cv_spt_left_thm : thm
val cv_spt_right_thm : thm
val cv_subspt_def : thm
val cv_subspt_ind : thm
val cv_subspt_thm : thm
val cv_toAList_foldi_def : thm
val cv_toAList_foldi_ind : thm
val cv_toAList_foldi_thm : thm
val cv_toAList_thm : thm
val cv_toListA_def : thm
val cv_toListA_ind : thm
val cv_toListA_thm : thm
val cv_toList_thm : thm
val cv_union_def : thm
val cv_union_ind : thm
val cv_union_thm : thm
val cv_v2n_custom_thm : thm
val every_empty_snd : thm
val every_empty_snd_def : thm
val every_empty_snd_ind : thm
val from_sptree_spt_def : thm
val from_sptree_to_sptree_spt_thm : thm
val from_to_fmap : thm
val genlist_compute : thm
val genlist_eq_GENLIST : thm
val map_spt_left_def : thm
val map_spt_left_ind : thm
val map_spt_right_def : thm
val map_spt_right_ind : thm
val map_spt_right_left : thm
val o_THM : thm
val replicate_acc_def : thm
val replicate_acc_ind : thm
val spt_centers_pre_cases : thm
val spt_centers_pre_ind : thm
val spt_centers_pre_rules : thm
val spt_centers_pre_strongind : thm
val toAList_foldi_pre : thm
val toAList_foldi_pre_cases : thm
val toAList_foldi_pre_ind : thm
val toAList_foldi_pre_rules : thm
val toAList_foldi_pre_strongind : thm
val to_sptree_spt_def : thm
val cv_std_grammars : type_grammar.grammar * term_grammar.grammar
(*
[cv_prim] Parent theory of "cv_std"
[sptree] Parent theory of "cv_std"
[FOLDL_lam_lam_pair_CASE_lam_la_def] Definition
⊢ ∀x_v x_e.
FOLDL_lam_lam_pair_CASE_lam_la x_v x_e =
FOLDL (λv0 v1. case v0 of (v2,v3) => (v2 + 1,insert v2 v1 v3))
x_e x_v
[combine_rle_isEmpty_def] Definition
⊢ combine_rle_isEmpty = combine_rle (λt. isEmpty t)
[cv_ALL_DISTINCT_def] Definition
⊢ ∀cv_v.
cv_ALL_DISTINCT cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_list_mem (cv_fst cv_v) (cv_snd cv_v)) (Num 0)
(cv_ALL_DISTINCT (cv_snd cv_v))) (Num 1)
[cv_ALOOKUP_def] Definition
⊢ ∀cv_v cv_q.
cv_ALOOKUP cv_v cv_q =
cv_if (cv_ispair cv_v)
(cv_if (cv_ispair (cv_fst cv_v))
(cv_if (cv_eq (cv_fst (cv_fst cv_v)) cv_q)
(Pair (Num 1) (cv_snd (cv_fst cv_v)))
(cv_ALOOKUP (cv_snd cv_v) cv_q)) (Num 0)) (Num 0)
[cv_DROP_def] Definition
⊢ ∀cv_n cv_v.
cv_DROP cv_n cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 0) cv_n)
(cv_DROP (cv_sub cv_n (Num 1)) (cv_snd cv_v))
(Pair (cv_fst cv_v) (cv_snd cv_v))) (Num 0)
[cv_EL_def] Definition
⊢ ∀cv_v cv_l.
cv_EL cv_v cv_l =
cv_if (cv_lt (Num 0) cv_v)
(let cv0 = cv_sub cv_v (Num 1) in cv_EL cv0 (cv_snd cv_l))
(cv_fst cv_l)
[cv_FLAT_def_primitive] Definition
⊢ cv_FLAT =
WFREC
(@R. WF R ∧ ∀cv_v. cv$c2b (cv_ispair cv_v) ⇒ R (cv_snd cv_v) cv_v)
(λcv_FLAT a.
I
(cv_if (cv_ispair a)
(cv_APPEND (cv_fst a) (cv_FLAT (cv_snd a))) (Num 0)))
[cv_FOLDL_lam_lam_pair_CASE_lam_la_def] Definition
⊢ ∀cv_x_v cv_x_e.
cv_FOLDL_lam_lam_pair_CASE_lam_la cv_x_v cv_x_e =
cv_if (cv_ispair cv_x_v)
(cv_FOLDL_lam_lam_pair_CASE_lam_la (cv_snd cv_x_v)
(cv_if (cv_ispair cv_x_e)
(Pair (cv_add (cv_fst cv_x_e) (Num 1))
(cv_insert (cv_fst cv_x_e) (cv_fst cv_x_v)
(cv_snd cv_x_e))) (Num 0))) cv_x_e
[cv_FRONT_def_primitive] Definition
⊢ cv_FRONT =
WFREC
(@R. WF R ∧
∀cv_v.
cv$c2b (cv_ispair cv_v) ∧ cv$c2b (cv_ispair (cv_snd cv_v)) ⇒
R (cv_snd cv_v) cv_v)
(λcv_FRONT a.
I
(cv_if (cv_ispair a)
(cv_if (cv_ispair (cv_snd a))
(Pair (cv_fst a) (cv_FRONT (cv_snd a))) (Num 0))
(Num 0)))
[cv_ISL_def] Definition
⊢ ∀cv_v.
cv_ISL cv_v =
cv_if (cv_lt (Num 0) (cv_fst cv_v)) (Num 0)
(cv_if (cv_ispair cv_v) (Num 1) (Num 0))
[cv_ISR_def] Definition
⊢ ∀cv_v.
cv_ISR cv_v = cv_if (cv_lt (Num 0) (cv_fst cv_v)) (Num 1) (Num 0)
[cv_LAST_def] Definition
⊢ ∀cv_v.
cv_LAST cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_ispair (cv_snd cv_v)) (cv_LAST (cv_snd cv_v))
(cv_fst cv_v)) (Num 0)
[cv_LENGTH_def] Definition
⊢ ∀cv_L. cv_LENGTH cv_L = cv_LEN cv_L (Num 0)
[cv_LEN_def] Definition
⊢ ∀cv_v cv_n.
cv_LEN cv_v cv_n =
cv_if (cv_ispair cv_v)
(cv_LEN (cv_snd cv_v) (cv_add cv_n (Num 1))) cv_n
[cv_NULL_def] Definition
⊢ ∀cv_v. cv_NULL cv_v = cv_if (cv_ispair cv_v) (Num 0) (Num 1)
[cv_OUTL_def] Definition
⊢ ∀cv_v.
cv_OUTL cv_v =
cv_if (cv_lt (Num 0) (cv_fst cv_v)) (Num 0)
(cv_if (cv_ispair cv_v) (cv_snd cv_v) (Num 0))
[cv_OUTR_def] Definition
⊢ ∀cv_v.
cv_OUTR cv_v =
cv_if (cv_lt (Num 0) (cv_fst cv_v)) (cv_snd cv_v) (Num 0)
[cv_PAD_LEFT_def] Definition
⊢ ∀cv_c cv_n cv_s.
cv_PAD_LEFT cv_c cv_n cv_s =
cv_APPEND (cv_REPLICATE (cv_sub cv_n (cv_LENGTH cv_s)) cv_c) cv_s
[cv_PAD_RIGHT_def] Definition
⊢ ∀cv_c cv_n cv_s.
cv_PAD_RIGHT cv_c cv_n cv_s =
cv_APPEND cv_s (cv_REPLICATE (cv_sub cv_n (cv_LENGTH cv_s)) cv_c)
[cv_REPLICATE_def] Definition
⊢ ∀cv_n cv_c.
cv_REPLICATE cv_n cv_c = cv_replicate_acc cv_n cv_c (Num 0)
[cv_REVERSE_def] Definition
⊢ ∀cv_L. cv_REVERSE cv_L = cv_REV cv_L (Num 0)
[cv_REV_def] Definition
⊢ ∀cv_v cv_acc.
cv_REV cv_v cv_acc =
cv_if (cv_ispair cv_v)
(cv_REV (cv_snd cv_v) (Pair (cv_fst cv_v) cv_acc)) cv_acc
[cv_SUM_ACC_def] Definition
⊢ ∀cv_v cv_acc.
cv_SUM_ACC cv_v cv_acc =
cv_if (cv_ispair cv_v)
(cv_SUM_ACC (cv_snd cv_v) (cv_add (cv_fst cv_v) cv_acc)) cv_acc
[cv_SUM_def] Definition
⊢ ∀cv_L. cv_SUM cv_L = cv_SUM_ACC cv_L (Num 0)
[cv_UNZIP_def_primitive] Definition
⊢ cv_UNZIP =
WFREC
(@R. WF R ∧
∀cv_ts. cv$c2b (cv_ispair cv_ts) ⇒ R (cv_snd cv_ts) cv_ts)
(λcv_UNZIP a.
I
(cv_if (cv_ispair a)
(let
cv0 = cv_UNZIP (cv_snd a)
in
cv_if (cv_ispair cv0)
(Pair (Pair (cv_fst (cv_fst a)) (cv_fst cv0))
(Pair (cv_snd (cv_fst a)) (cv_snd cv0)))
(Num 0)) (Pair (Num 0) (Num 0))))
[cv_ZIP_def_primitive] Definition
⊢ cv_ZIP =
WFREC
(@R. WF R ∧
∀cv_v.
cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_ispair (cv_fst cv_v)) ∧
cv$c2b (cv_ispair (cv_snd cv_v)) ⇒
R (Pair (cv_snd (cv_fst cv_v)) (cv_snd (cv_snd cv_v)))
cv_v)
(λcv_ZIP a.
I
(cv_if (cv_ispair a)
(cv_if (cv_ispair (cv_fst a))
(cv_if (cv_ispair (cv_snd a))
(Pair
(Pair (cv_fst (cv_fst a)) (cv_fst (cv_snd a)))
(cv_ZIP
(Pair (cv_snd (cv_fst a))
(cv_snd (cv_snd a))))) (Num 0)) (Num 0))
(Num 0)))
[cv_apsnd_cons_def] Definition
⊢ ∀cv_x cv_v.
cv_apsnd_cons cv_x cv_v =
cv_if (cv_ispair cv_v)
(Pair (cv_fst cv_v) (Pair cv_x (cv_snd cv_v))) (Num 0)
[cv_combine_rle_isEmpty_def_primitive] Definition
⊢ cv_combine_rle_isEmpty =
WFREC
(@R. WF R ∧
(∀cv_xs.
cv$c2b (cv_ispair cv_xs) ∧
cv$c2b (cv_ispair (cv_snd cv_xs)) ∧
cv$c2b (cv_ispair (cv_fst (cv_snd cv_xs))) ∧
cv$c2b (cv_ispair (cv_fst cv_xs)) ∧
cv$c2b
(cv_if (cv_eq (cv_snd (cv_fst cv_xs)) (Num 0))
(cv_eq (cv_snd (cv_fst (cv_snd cv_xs))) (Num 0))
(Num 0)) ⇒
R
(Pair
(Pair
(cv_add (cv_fst (cv_fst cv_xs))
(cv_fst (cv_fst (cv_snd cv_xs))))
(cv_snd (cv_fst cv_xs))) (cv_snd (cv_snd cv_xs)))
cv_xs) ∧
∀cv_xs.
cv$c2b (cv_ispair cv_xs) ∧
cv$c2b (cv_ispair (cv_snd cv_xs)) ∧
cv$c2b (cv_ispair (cv_fst (cv_snd cv_xs))) ∧
cv$c2b (cv_ispair (cv_fst cv_xs)) ∧
¬cv$c2b
(cv_if (cv_eq (cv_snd (cv_fst cv_xs)) (Num 0))
(cv_eq (cv_snd (cv_fst (cv_snd cv_xs))) (Num 0))
(Num 0)) ⇒
R
(Pair
(Pair (cv_fst (cv_fst (cv_snd cv_xs)))
(cv_snd (cv_fst (cv_snd cv_xs))))
(cv_snd (cv_snd cv_xs))) cv_xs)
(λcv_combine_rle_isEmpty a.
I
(cv_if (cv_ispair a)
(cv_if (cv_ispair (cv_snd a))
(cv_if (cv_ispair (cv_fst (cv_snd a)))
(cv_if (cv_ispair (cv_fst a))
(cv_if
(cv_if (cv_eq (cv_snd (cv_fst a)) (Num 0))
(cv_eq (cv_snd (cv_fst (cv_snd a)))
(Num 0)) (Num 0))
(cv_combine_rle_isEmpty
(Pair
(Pair
(cv_add (cv_fst (cv_fst a))
(cv_fst (cv_fst (cv_snd a))))
(cv_snd (cv_fst a)))
(cv_snd (cv_snd a))))
(Pair
(Pair (cv_fst (cv_fst a))
(cv_snd (cv_fst a)))
(cv_combine_rle_isEmpty
(Pair
(Pair (cv_fst (cv_fst (cv_snd a)))
(cv_snd (cv_fst (cv_snd a))))
(cv_snd (cv_snd a)))))) (Num 0))
(Num 0)) (Pair (cv_fst a) (Num 0))) (Num 0)))
[cv_every_empty_snd_def] Definition
⊢ ∀cv_v.
cv_every_empty_snd cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_ispair (cv_fst cv_v))
(cv_if (cv_eq (cv_snd (cv_fst cv_v)) (Num 0))
(cv_every_empty_snd (cv_snd cv_v)) (Num 0)) (Num 0))
(Num 1)
[cv_fromList_def] Definition
⊢ ∀cv_l.
cv_fromList cv_l =
cv_snd
(cv_FOLDL_lam_lam_pair_CASE_lam_la cv_l (Pair (Num 0) (Num 0)))
[cv_isPREFIX_def] Definition
⊢ ∀cv_v cv_l.
cv_isPREFIX cv_v cv_l =
cv_if (cv_ispair cv_v)
(cv_if (cv_ispair cv_l)
(cv_if (cv_eq (cv_fst cv_v) (cv_fst cv_l))
(cv_isPREFIX (cv_snd cv_v) (cv_snd cv_l)) (Num 0))
(Num 0)) (Num 1)
[cv_list_insert_def] Definition
⊢ ∀cv_v cv_t.
cv_list_insert cv_v cv_t =
cv_if (cv_ispair cv_v)
(cv_list_insert (cv_snd cv_v)
(cv_insert (cv_fst cv_v) (Num 0) cv_t)) cv_t
[cv_list_mem_def] Definition
⊢ ∀cv_y cv_v.
cv_list_mem cv_y cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_eq (cv_fst cv_v) cv_y) (Num 1)
(cv_list_mem cv_y (cv_snd cv_v))) (Num 0)
[cv_list_to_num_set_def_primitive] Definition
⊢ cv_list_to_num_set =
WFREC
(@R. WF R ∧ ∀cv_v. cv$c2b (cv_ispair cv_v) ⇒ R (cv_snd cv_v) cv_v)
(λcv_list_to_num_set a.
I
(cv_if (cv_ispair a)
(cv_insert (cv_fst a) (Num 0)
(cv_list_to_num_set (cv_snd a))) (Num 0)))
[cv_lookup_def] Definition
⊢ ∀cv_k cv_v.
cv_lookup cv_k cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 1) (cv_fst cv_v))
(cv_if (cv_lt (Num 2) (cv_fst cv_v))
(cv_if (cv_lt (Num 0) cv_k)
(cv_lookup (cv_div (cv_sub cv_k (Num 1)) (Num 2))
(cv_if (cv_sub (Num 1) (cv_mod cv_k (Num 2)))
(cv_fst (cv_snd cv_v))
(cv_snd (cv_snd (cv_snd cv_v)))))
(Pair (Num 1) (cv_fst (cv_snd (cv_snd cv_v)))))
(cv_if (cv_lt (Num 0) cv_k)
(cv_lookup (cv_div (cv_sub cv_k (Num 1)) (Num 2))
(cv_if (cv_sub (Num 1) (cv_mod cv_k (Num 2)))
(cv_fst (cv_snd cv_v)) (cv_snd (cv_snd cv_v))))
(Num 0)))
(cv_if (cv_lt (Num 0) cv_k) (Num 0)
(Pair (Num 1) (cv_snd cv_v)))) (Num 0)
[cv_lrnext_def_primitive] Definition
⊢ cv_lrnext =
WFREC
(@R. WF R ∧
∀cv_n.
cv$c2b (cv_lt (Num 0) cv_n) ⇒
R (cv_div (cv_sub cv_n (Num 1)) (Num 2)) cv_n)
(λcv_lrnext a.
I
(cv_if (cv_lt (Num 0) a)
(cv_mul (Num 2)
(cv_lrnext (cv_div (cv_sub a (Num 1)) (Num 2))))
(Num 1)))
[cv_map_fst_def_primitive] Definition
⊢ cv_map_fst =
WFREC (@R. WF R ∧ ∀cv. cv$c2b (cv_ispair cv) ⇒ R (cv_snd cv) cv)
(λcv_map_fst a.
I
(cv_if (cv_ispair a)
(Pair (cv_fst (cv_fst a)) (cv_map_fst (cv_snd a)))
(Num 0)))
[cv_map_snd_def_primitive] Definition
⊢ cv_map_snd =
WFREC (@R. WF R ∧ ∀cv. cv$c2b (cv_ispair cv) ⇒ R (cv_snd cv) cv)
(λcv_map_snd a.
I
(cv_if (cv_ispair a)
(Pair (cv_snd (cv_fst a)) (cv_map_snd (cv_snd a)))
(Num 0)))
[cv_mk_BN_def] Definition
⊢ ∀cv_v0 cv_v.
cv_mk_BN cv_v0 cv_v =
(let
cv0 = Pair cv_v0 cv_v
in
cv_if (cv_ispair cv0)
(cv_if (cv_ispair (cv_fst cv0))
(cv_if (cv_lt (Num 1) (cv_fst (cv_fst cv0)))
(cv_if (cv_lt (Num 2) (cv_fst (cv_fst cv0)))
(Pair (Num 2)
(Pair
(Pair (Num 3)
(Pair (cv_fst (cv_snd (cv_fst cv0)))
(Pair
(cv_fst
(cv_snd (cv_snd (cv_fst cv0))))
(cv_snd
(cv_snd (cv_snd (cv_fst cv0)))))))
(cv_snd cv0)))
(Pair (Num 2)
(Pair
(Pair (Num 2)
(Pair (cv_fst (cv_snd (cv_fst cv0)))
(cv_snd (cv_snd (cv_fst cv0)))))
(cv_snd cv0))))
(Pair (Num 2)
(Pair (Pair (Num 1) (cv_snd (cv_fst cv0)))
(cv_snd cv0))))
(cv_if (cv_ispair (cv_snd cv0))
(cv_if (cv_lt (Num 1) (cv_fst (cv_snd cv0)))
(cv_if (cv_lt (Num 2) (cv_fst (cv_snd cv0)))
(Pair (Num 2)
(Pair (Num 0)
(Pair (Num 3)
(Pair (cv_fst (cv_snd (cv_snd cv0)))
(Pair
(cv_fst
(cv_snd (cv_snd (cv_snd cv0))))
(cv_snd
(cv_snd (cv_snd (cv_snd cv0)))))))))
(Pair (Num 2)
(Pair (Num 0)
(Pair (Num 2)
(Pair (cv_fst (cv_snd (cv_snd cv0)))
(cv_snd (cv_snd (cv_snd cv0))))))))
(Pair (Num 2)
(Pair (Num 0)
(Pair (Num 1) (cv_snd (cv_snd cv0))))))
(Num 0))) (Num 0))
[cv_mk_BS_def] Definition
⊢ ∀cv_v0 cv_x cv_v.
cv_mk_BS cv_v0 cv_x cv_v =
(let
cv0 = Pair cv_v0 cv_v
in
cv_if (cv_ispair cv0)
(cv_if (cv_ispair (cv_fst cv0))
(cv_if (cv_lt (Num 1) (cv_fst (cv_fst cv0)))
(cv_if (cv_lt (Num 2) (cv_fst (cv_fst cv0)))
(cv_if (cv_ispair (cv_snd cv0))
(cv_if (cv_lt (Num 1) (cv_fst (cv_snd cv0)))
(cv_if (cv_lt (Num 2) (cv_fst (cv_snd cv0)))
(Pair (Num 3)
(Pair
(Pair (Num 3)
(Pair
(cv_fst (cv_snd (cv_fst cv0)))
(Pair
(cv_fst
(cv_snd
(cv_snd (cv_fst cv0))))
(cv_snd
(cv_snd
(cv_snd (cv_fst cv0)))))))
(Pair cv_x
(Pair (Num 3)
(Pair
(cv_fst
(cv_snd (cv_snd cv0)))
(Pair
(cv_fst
(cv_snd
(cv_snd
(cv_snd cv0))))
(cv_snd
(cv_snd
(cv_snd
(cv_snd cv0))))))))))
(Pair (Num 3)
(Pair
(Pair (Num 3)
(Pair
(cv_fst (cv_snd (cv_fst cv0)))
(Pair
(cv_fst
(cv_snd
(cv_snd (cv_fst cv0))))
(cv_snd
(cv_snd
(cv_snd (cv_fst cv0)))))))
(Pair cv_x
(Pair (Num 2)
(Pair
(cv_fst
(cv_snd (cv_snd cv0)))
(cv_snd
(cv_snd (cv_snd cv0)))))))))
(Pair (Num 3)
(Pair
(Pair (Num 3)
(Pair (cv_fst (cv_snd (cv_fst cv0)))
(Pair
(cv_fst
(cv_snd
(cv_snd (cv_fst cv0))))
(cv_snd
(cv_snd
(cv_snd (cv_fst cv0)))))))
(Pair cv_x
(Pair (Num 1) (cv_snd (cv_snd cv0)))))))
(Pair (Num 3)
(Pair
(Pair (Num 3)
(Pair (cv_fst (cv_snd (cv_fst cv0)))
(Pair
(cv_fst
(cv_snd (cv_snd (cv_fst cv0))))
(cv_snd
(cv_snd (cv_snd (cv_fst cv0)))))))
(Pair cv_x (Num 0)))))
(cv_if (cv_ispair (cv_snd cv0))
(cv_if (cv_lt (Num 1) (cv_fst (cv_snd cv0)))
(cv_if (cv_lt (Num 2) (cv_fst (cv_snd cv0)))
(Pair (Num 3)
(Pair
(Pair (Num 2)
(Pair
(cv_fst (cv_snd (cv_fst cv0)))
(cv_snd (cv_snd (cv_fst cv0)))))
(Pair cv_x
(Pair (Num 3)
(Pair
(cv_fst
(cv_snd (cv_snd cv0)))
(Pair
(cv_fst
(cv_snd
(cv_snd
(cv_snd cv0))))
(cv_snd
(cv_snd
(cv_snd
(cv_snd cv0))))))))))
(Pair (Num 3)
(Pair
(Pair (Num 2)
(Pair
(cv_fst (cv_snd (cv_fst cv0)))
(cv_snd (cv_snd (cv_fst cv0)))))
(Pair cv_x
(Pair (Num 2)
(Pair
(cv_fst
(cv_snd (cv_snd cv0)))
(cv_snd
(cv_snd (cv_snd cv0)))))))))
(Pair (Num 3)
(Pair
(Pair (Num 2)
(Pair (cv_fst (cv_snd (cv_fst cv0)))
(cv_snd (cv_snd (cv_fst cv0)))))
(Pair cv_x
(Pair (Num 1) (cv_snd (cv_snd cv0)))))))
(Pair (Num 3)
(Pair
(Pair (Num 2)
(Pair (cv_fst (cv_snd (cv_fst cv0)))
(cv_snd (cv_snd (cv_fst cv0)))))
(Pair cv_x (Num 0))))))
(cv_if (cv_ispair (cv_snd cv0))
(cv_if (cv_lt (Num 1) (cv_fst (cv_snd cv0)))
(cv_if (cv_lt (Num 2) (cv_fst (cv_snd cv0)))
(Pair (Num 3)
(Pair (Pair (Num 1) (cv_snd (cv_fst cv0)))
(Pair cv_x
(Pair (Num 3)
(Pair
(cv_fst (cv_snd (cv_snd cv0)))
(Pair
(cv_fst
(cv_snd
(cv_snd (cv_snd cv0))))
(cv_snd
(cv_snd
(cv_snd (cv_snd cv0))))))))))
(Pair (Num 3)
(Pair (Pair (Num 1) (cv_snd (cv_fst cv0)))
(Pair cv_x
(Pair (Num 2)
(Pair
(cv_fst (cv_snd (cv_snd cv0)))
(cv_snd (cv_snd (cv_snd cv0)))))))))
(Pair (Num 3)
(Pair (Pair (Num 1) (cv_snd (cv_fst cv0)))
(Pair cv_x
(Pair (Num 1) (cv_snd (cv_snd cv0)))))))
(Pair (Num 3)
(Pair (Pair (Num 1) (cv_snd (cv_fst cv0)))
(Pair cv_x (Num 0))))))
(cv_if (cv_ispair (cv_snd cv0))
(cv_if (cv_lt (Num 1) (cv_fst (cv_snd cv0)))
(cv_if (cv_lt (Num 2) (cv_fst (cv_snd cv0)))
(Pair (Num 3)
(Pair (Num 0)
(Pair cv_x
(Pair (Num 3)
(Pair (cv_fst (cv_snd (cv_snd cv0)))
(Pair
(cv_fst
(cv_snd
(cv_snd (cv_snd cv0))))
(cv_snd
(cv_snd
(cv_snd (cv_snd cv0))))))))))
(Pair (Num 3)
(Pair (Num 0)
(Pair cv_x
(Pair (Num 2)
(Pair (cv_fst (cv_snd (cv_snd cv0)))
(cv_snd (cv_snd (cv_snd cv0)))))))))
(Pair (Num 3)
(Pair (Num 0)
(Pair cv_x
(Pair (Num 1) (cv_snd (cv_snd cv0)))))))
(Pair (Num 1) cv_x))) (Num 0))
[cv_mk_wf_def_primitive] Definition
⊢ cv_mk_wf =
WFREC
(@R. WF R ∧
(∀cv_v.
cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ⇒
R (cv_fst (cv_snd cv_v)) cv_v) ∧
(∀cv_v.
cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ⇒
R (cv_snd (cv_snd (cv_snd cv_v))) cv_v) ∧
(∀cv_v.
cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ⇒
R (cv_fst (cv_snd cv_v)) cv_v) ∧
∀cv_v.
cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ⇒
R (cv_snd (cv_snd cv_v)) cv_v)
(λcv_mk_wf a.
I
(cv_if (cv_ispair a)
(cv_if (cv_lt (Num 1) (cv_fst a))
(cv_if (cv_lt (Num 2) (cv_fst a))
(cv_mk_BS (cv_mk_wf (cv_fst (cv_snd a)))
(cv_fst (cv_snd (cv_snd a)))
(cv_mk_wf (cv_snd (cv_snd (cv_snd a)))))
(cv_mk_BN (cv_mk_wf (cv_fst (cv_snd a)))
(cv_mk_wf (cv_snd (cv_snd a)))))
(Pair (Num 1) (cv_snd a))) (Num 0)))
[cv_nub_def_primitive] Definition
⊢ cv_nub =
WFREC
(@R. WF R ∧
(∀cv_v.
cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_list_mem (cv_fst cv_v) (cv_snd cv_v)) ⇒
R (cv_snd cv_v) cv_v) ∧
∀cv_v.
cv$c2b (cv_ispair cv_v) ∧
¬cv$c2b (cv_list_mem (cv_fst cv_v) (cv_snd cv_v)) ⇒
R (cv_snd cv_v) cv_v)
(λcv_nub a.
I
(cv_if (cv_ispair a)
(cv_if (cv_list_mem (cv_fst a) (cv_snd a))
(cv_nub (cv_snd a))
(Pair (cv_fst a) (cv_nub (cv_snd a)))) (Num 0)))
[cv_oEL_def] Definition
⊢ ∀cv_n cv_v.
cv_oEL cv_n cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 0) cv_n)
(cv_oEL (cv_sub cv_n (Num 1)) (cv_snd cv_v))
(Pair (Num 1) (cv_fst cv_v))) (Num 0)
[cv_oHD_def] Definition
⊢ ∀cv_l.
cv_oHD cv_l =
cv_if (cv_ispair cv_l) (Pair (Num 1) (cv_fst cv_l)) (Num 0)
[cv_replicate_acc_def] Definition
⊢ ∀cv_n cv_x cv_acc.
cv_replicate_acc cv_n cv_x cv_acc =
cv_if (cv_lt (Num 0) cv_n)
(cv_replicate_acc (cv_sub cv_n (Num 1)) cv_x (Pair cv_x cv_acc))
cv_acc
[cv_right_depth_def] Definition
⊢ (∀v0. cv_right_depth (Num v0) = 0) ∧
∀x y. cv_right_depth (Pair x y) = cv_right_depth y + 1
[cv_size'_def_primitive] Definition
⊢ cv_size' =
WFREC
(@R. WF R ∧
(∀cv_v.
cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ⇒
R (cv_fst (cv_snd cv_v)) cv_v) ∧
(∀cv_v.
cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ⇒
R (cv_snd (cv_snd (cv_snd cv_v))) cv_v) ∧
(∀cv_v.
cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ⇒
R (cv_fst (cv_snd cv_v)) cv_v) ∧
∀cv_v.
cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ⇒
R (cv_snd (cv_snd cv_v)) cv_v)
(λcv_size' a.
I
(cv_if (cv_ispair a)
(cv_if (cv_lt (Num 1) (cv_fst a))
(cv_if (cv_lt (Num 2) (cv_fst a))
(cv_add
(cv_add (cv_size' (cv_fst (cv_snd a)))
(cv_size' (cv_snd (cv_snd (cv_snd a)))))
(Num 1))
(cv_add (cv_size' (cv_fst (cv_snd a)))
(cv_size' (cv_snd (cv_snd a))))) (Num 1))
(Num 0)))
[cv_spt_center_def] Definition
⊢ ∀cv_v.
cv_spt_center cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 1) (cv_fst cv_v))
(cv_if (cv_lt (Num 2) (cv_fst cv_v))
(Pair (Num 1) (cv_fst (cv_snd (cv_snd cv_v)))) (Num 0))
(Pair (Num 1) (cv_snd cv_v))) (Num 0)
[cv_spt_left_def] Definition
⊢ ∀cv_v.
cv_spt_left cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 1) (cv_fst cv_v)) (cv_fst (cv_snd cv_v))
(Num 0)) (Num 0)
[cv_spt_right_def] Definition
⊢ ∀cv_v.
cv_spt_right cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 1) (cv_fst cv_v))
(cv_if (cv_lt (Num 2) (cv_fst cv_v))
(cv_snd (cv_snd (cv_snd cv_v))) (cv_snd (cv_snd cv_v)))
(Num 0)) (Num 0)
[cv_subspt_def_tupled_AUX] Definition
⊢ ∀R. cv_subspt_def_tupled_aux R =
WFREC R
(λcv_subspt_def_tupled a.
case a of
(cv_v,cv_t) =>
I
(cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 1) (cv_fst cv_v))
(cv_if (cv_lt (Num 2) (cv_fst cv_v))
(cv_if
(cv_eq (cv_spt_center cv_t)
(Pair (Num 1)
(cv_fst (cv_snd (cv_snd cv_v)))))
(cv_if
(cv_subspt_def_tupled
(cv_fst (cv_snd cv_v),
cv_spt_left cv_t))
(cv_subspt_def_tupled
(cv_snd (cv_snd (cv_snd cv_v)),
cv_spt_right cv_t)) (Num 0))
(Num 0))
(cv_if
(cv_subspt_def_tupled
(cv_fst (cv_snd cv_v),
cv_spt_left cv_t))
(cv_subspt_def_tupled
(cv_snd (cv_snd cv_v),
cv_spt_right cv_t)) (Num 0)))
(cv_eq (cv_spt_center cv_t)
(Pair (Num 1) (cv_snd cv_v)))) (Num 1)))
[cv_toAList_def] Definition
⊢ ∀cv_x. cv_toAList cv_x = cv_toAList_foldi (Num 0) (Num 0) cv_x
[cv_toAList_foldi_def_tupled_AUX] Definition
⊢ ∀R. cv_toAList_foldi_def_tupled_aux R =
WFREC R
(λcv_toAList_foldi_def_tupled a.
case a of
(cv_i,cv_acc,cv_v) =>
I
(cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 1) (cv_fst cv_v))
(cv_if (cv_lt (Num 2) (cv_fst cv_v))
(let
cv0 = cv_lrnext cv_i
in
cv_toAList_foldi_def_tupled
(cv_add cv_i cv0,
Pair
(Pair cv_i
(cv_fst (cv_snd (cv_snd cv_v))))
(cv_toAList_foldi_def_tupled
(cv_add cv_i
(cv_mul (Num 2) cv0),
cv_acc,cv_fst (cv_snd cv_v))),
cv_snd (cv_snd (cv_snd cv_v))))
(let
cv0 = cv_lrnext cv_i
in
cv_toAList_foldi_def_tupled
(cv_add cv_i cv0,
cv_toAList_foldi_def_tupled
(cv_add cv_i (cv_mul (Num 2) cv0),
cv_acc,cv_fst (cv_snd cv_v)),
cv_snd (cv_snd cv_v))))
(Pair (Pair cv_i (cv_snd cv_v)) cv_acc))
cv_acc))
[cv_toListA_def_tupled_AUX] Definition
⊢ ∀R. cv_toListA_def_tupled_aux R =
WFREC R
(λcv_toListA_def_tupled a.
case a of
(cv_acc,cv_v) =>
I
(cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 1) (cv_fst cv_v))
(cv_if (cv_lt (Num 2) (cv_fst cv_v))
(cv_toListA_def_tupled
(Pair (cv_fst (cv_snd (cv_snd cv_v)))
(cv_toListA_def_tupled
(cv_acc,
cv_snd (cv_snd (cv_snd cv_v)))),
cv_fst (cv_snd cv_v)))
(cv_toListA_def_tupled
(cv_toListA_def_tupled
(cv_acc,cv_snd (cv_snd cv_v)),
cv_fst (cv_snd cv_v))))
(Pair (cv_snd cv_v) cv_acc)) cv_acc))
[cv_toList_def] Definition
⊢ ∀cv_m. cv_toList cv_m = cv_toListA (Num 0) cv_m
[cv_v2n_custom_def] Definition
⊢ ∀cv_acc cv_v.
cv_v2n_custom cv_acc cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_fst cv_v)
(cv_v2n_custom (cv_add (cv_mul (Num 2) cv_acc) (Num 1))
(cv_snd cv_v))
(cv_v2n_custom (cv_mul (Num 2) cv_acc) (cv_snd cv_v)))
cv_acc
[every_empty_snd_def_primitive] Definition
⊢ every_empty_snd =
WFREC (@R. WF R ∧ ∀n xs x. isEmpty x ⇒ R xs ((n,x)::xs))
(λevery_empty_snd a.
case a of
[] => I T
| (n,x)::xs =>
I (if isEmpty x then every_empty_snd xs else F))
[from_fmap_def] Definition
⊢ ∀f m.
from_fmap f m =
from_sptree_sptree_spt f (fromAList (fmap_to_alist m))
[from_sptree_sptree_spt_def] Definition
⊢ (∀f0. from_sptree_sptree_spt f0 LN = Num 0) ∧
(∀f0 v0.
from_sptree_sptree_spt f0 ⦕ 0 ↦ v0 ⦖ = Pair (Num 1) (f0 v0)) ∧
(∀f0 v0 v1.
from_sptree_sptree_spt f0 (BN v0 v1) =
Pair (Num 2)
(Pair (from_sptree_sptree_spt f0 v0)
(from_sptree_sptree_spt f0 v1))) ∧
∀f0 v0 v1 v2.
from_sptree_sptree_spt f0 (BS v0 v1 v2) =
Pair (Num 3)
(Pair (from_sptree_sptree_spt f0 v0)
(Pair (f0 v1) (from_sptree_sptree_spt f0 v2)))
[genlist_def] Definition
⊢ (∀i f. genlist i f 0 = []) ∧
∀i f n. genlist i f (SUC n) = f i::genlist (i + 1) f n
[list_mapi_def] Definition
⊢ (∀i f. list_mapi i f [] = []) ∧
∀i f x xs. list_mapi i f (x::xs) = f i x::list_mapi (i + 1) f xs
[list_mem_def] Definition
⊢ (∀y. list_mem y [] ⇔ F) ∧
∀y x xs. list_mem y (x::xs) ⇔ if x = y then T else list_mem y xs
[map_spt_left_def_primitive] Definition
⊢ map_spt_left =
WFREC (@R. WF R ∧ ∀x i xs. R xs ((i,x)::xs))
(λmap_spt_left a.
case a of
[] => I []
| (i,x)::xs => I ((i,spt_left x)::map_spt_left xs))
[map_spt_right_def_primitive] Definition
⊢ map_spt_right =
WFREC (@R. WF R ∧ ∀x i xs. R xs ((i,x)::xs))
(λmap_spt_right a.
case a of
[] => I []
| (i,x)::xs => I ((i,spt_right x)::map_spt_right xs))
[toAList_foldi_def] Definition
⊢ toAList_foldi = foldi (λk v a. (k,v)::a)
[to_fmap_def] Definition
⊢ ∀t m. to_fmap t m = alist_to_fmap (toAList (to_sptree_spt t m))
[EL_pre] Theorem
⊢ ∀n xs. EL_pre n xs ⇔ n < LENGTH xs
[EL_pre_cases] Theorem
⊢ ∀a0 a1.
EL_pre a0 a1 ⇔
(a0 = 0 ⇒ a1 ≠ []) ∧ ∀n. a0 = SUC n ⇒ EL_pre n (TL a1)
[EL_pre_ind] Theorem
⊢ ∀EL_pre'.
(∀v l.
(v = 0 ⇒ l ≠ []) ∧ (∀n. v = SUC n ⇒ EL_pre' n (TL l)) ⇒
EL_pre' v l) ⇒
∀a0 a1. EL_pre a0 a1 ⇒ EL_pre' a0 a1
[EL_pre_rules] Theorem
⊢ ∀v l.
(v = 0 ⇒ l ≠ []) ∧ (∀n. v = SUC n ⇒ EL_pre n (TL l)) ⇒ EL_pre v l
[EL_pre_strongind] Theorem
⊢ ∀EL_pre'.
(∀v l.
(v = 0 ⇒ l ≠ []) ∧
(∀n. v = SUC n ⇒ EL_pre n (TL l) ∧ EL_pre' n (TL l)) ⇒
EL_pre' v l) ⇒
∀a0 a1. EL_pre a0 a1 ⇒ EL_pre' a0 a1
[FOLDL_lam_lam_pair_CASE_lam_la_ho] Theorem
⊢ T ⇒
from_pair Num (from_sptree_sptree_spt f_a)
(FOLDL (λv0 v1. case v0 of (v2,v3) => (v2 + 1,insert v2 v1 v3))
x_e x_v) =
cv_FOLDL_lam_lam_pair_CASE_lam_la (from_list f_a x_v)
(from_pair Num (from_sptree_sptree_spt f_a) x_e)
[FRONT_pre] Theorem
⊢ ∀xs. FRONT_pre xs ⇔ xs ≠ []
[FRONT_pre_cases] Theorem
⊢ ∀a0.
FRONT_pre a0 ⇔
(∃xs x. a0 = x::xs) ∧ a0 ≠ [] ∧
∀v0 v1. a0 = v0::v1 ⇒ ∀v0 v1'. v1 = v0::v1' ⇒ FRONT_pre v1
[FRONT_pre_ind] Theorem
⊢ ∀FRONT_pre'.
(∀v. (∃xs x. v = x::xs) ∧ v ≠ [] ∧
(∀v0 v1. v = v0::v1 ⇒ ∀v0 v1'. v1 = v0::v1' ⇒ FRONT_pre' v1) ⇒
FRONT_pre' v) ⇒
∀a0. FRONT_pre a0 ⇒ FRONT_pre' a0
[FRONT_pre_rules] Theorem
⊢ ∀v. (∃xs x. v = x::xs) ∧ v ≠ [] ∧
(∀v0 v1. v = v0::v1 ⇒ ∀v0 v1'. v1 = v0::v1' ⇒ FRONT_pre v1) ⇒
FRONT_pre v
[FRONT_pre_strongind] Theorem
⊢ ∀FRONT_pre'.
(∀v. (∃xs x. v = x::xs) ∧ v ≠ [] ∧
(∀v0 v1.
v = v0::v1 ⇒
∀v0 v1'. v1 = v0::v1' ⇒ FRONT_pre v1 ∧ FRONT_pre' v1) ⇒
FRONT_pre' v) ⇒
∀a0. FRONT_pre a0 ⇒ FRONT_pre' a0
[INDEX_OF_pre_cases] Theorem
⊢ ∀a0 a1.
INDEX_OF_pre a0 a1 ⇔
∀v0 v1. a1 = v0::v1 ⇒ a0 ≠ v0 ⇒ INDEX_OF_pre a0 v1
[INDEX_OF_pre_ind] Theorem
⊢ ∀INDEX_OF_pre'.
(∀x v.
(∀v0 v1. v = v0::v1 ⇒ x ≠ v0 ⇒ INDEX_OF_pre' x v1) ⇒
INDEX_OF_pre' x v) ⇒
∀a0 a1. INDEX_OF_pre a0 a1 ⇒ INDEX_OF_pre' a0 a1
[INDEX_OF_pre_rules] Theorem
⊢ ∀x v.
(∀v0 v1. v = v0::v1 ⇒ x ≠ v0 ⇒ INDEX_OF_pre x v1) ⇒
INDEX_OF_pre x v
[INDEX_OF_pre_strongind] Theorem
⊢ ∀INDEX_OF_pre'.
(∀x v.
(∀v0 v1.
v = v0::v1 ⇒
x ≠ v0 ⇒
INDEX_OF_pre x v1 ∧ INDEX_OF_pre' x v1) ⇒
INDEX_OF_pre' x v) ⇒
∀a0 a1. INDEX_OF_pre a0 a1 ⇒ INDEX_OF_pre' a0 a1
[I_THM] Theorem
⊢ ∀x. I x = x
[K_THM] Theorem
⊢ ∀x y. K x y = x
[LAST_pre] Theorem
⊢ ∀xs. LAST_pre xs ⇔ xs ≠ []
[LAST_pre_cases] Theorem
⊢ ∀a0.
LAST_pre a0 ⇔
(∃xs x. a0 = x::xs) ∧ a0 ≠ [] ∧
∀v0 v1. a0 = v0::v1 ⇒ ∀v0 v1'. v1 = v0::v1' ⇒ LAST_pre v1
[LAST_pre_ind] Theorem
⊢ ∀LAST_pre'.
(∀v. (∃xs x. v = x::xs) ∧ v ≠ [] ∧
(∀v0 v1. v = v0::v1 ⇒ ∀v0 v1'. v1 = v0::v1' ⇒ LAST_pre' v1) ⇒
LAST_pre' v) ⇒
∀a0. LAST_pre a0 ⇒ LAST_pre' a0
[LAST_pre_rules] Theorem
⊢ ∀v. (∃xs x. v = x::xs) ∧ v ≠ [] ∧
(∀v0 v1. v = v0::v1 ⇒ ∀v0 v1'. v1 = v0::v1' ⇒ LAST_pre v1) ⇒
LAST_pre v
[LAST_pre_strongind] Theorem
⊢ ∀LAST_pre'.
(∀v. (∃xs x. v = x::xs) ∧ v ≠ [] ∧
(∀v0 v1.
v = v0::v1 ⇒
∀v0 v1'. v1 = v0::v1' ⇒ LAST_pre v1 ∧ LAST_pre' v1) ⇒
LAST_pre' v) ⇒
∀a0. LAST_pre a0 ⇒ LAST_pre' a0
[MAPi_eq_list_mapi] Theorem
⊢ MAPi = list_mapi 0
[OUTL_pre] Theorem
⊢ OUTL_pre x ⇔ ISL x
[OUTL_pre_cases] Theorem
⊢ ∀a0. OUTL_pre a0 ⇔ (∃x. a0 = INL x) ∧ ∀v0. a0 ≠ INR v0
[OUTL_pre_ind] Theorem
⊢ ∀OUTL_pre'.
(∀v. (∃x. v = INL x) ∧ (∀v0. v ≠ INR v0) ⇒ OUTL_pre' v) ⇒
∀a0. OUTL_pre a0 ⇒ OUTL_pre' a0
[OUTL_pre_rules] Theorem
⊢ ∀v. (∃x. v = INL x) ∧ (∀v0. v ≠ INR v0) ⇒ OUTL_pre v
[OUTL_pre_strongind] Theorem
⊢ ∀OUTL_pre'.
(∀v. (∃x. v = INL x) ∧ (∀v0. v ≠ INR v0) ⇒ OUTL_pre' v) ⇒
∀a0. OUTL_pre a0 ⇒ OUTL_pre' a0
[OUTR_pre] Theorem
⊢ OUTR_pre x ⇔ ISR x
[OUTR_pre_cases] Theorem
⊢ ∀a0. OUTR_pre a0 ⇔ (∃x. a0 = INR x) ∧ ∀v0. a0 ≠ INL v0
[OUTR_pre_ind] Theorem
⊢ ∀OUTR_pre'.
(∀v. (∃x. v = INR x) ∧ (∀v0. v ≠ INL v0) ⇒ OUTR_pre' v) ⇒
∀a0. OUTR_pre a0 ⇒ OUTR_pre' a0
[OUTR_pre_rules] Theorem
⊢ ∀v. (∃x. v = INR x) ∧ (∀v0. v ≠ INL v0) ⇒ OUTR_pre v
[OUTR_pre_strongind] Theorem
⊢ ∀OUTR_pre'.
(∀v. (∃x. v = INR x) ∧ (∀v0. v ≠ INL v0) ⇒ OUTR_pre' v) ⇒
∀a0. OUTR_pre a0 ⇒ OUTR_pre' a0
[REPLICATE] Theorem
⊢ REPLICATE n c = replicate_acc n c []
[UNZIP_eq] Theorem
⊢ UNZIP ts =
case ts of
[] => ([],[])
| x::xs => (let (t1,t2) = UNZIP xs in (FST x::t1,SND x::t2))
[combine_rle_isEmpty_eq] Theorem
⊢ combine_rle_isEmpty xs =
case xs of
[] => []
| [t] => [t]
| (i,x)::(j,y)::xs =>
if isEmpty x ∧ isEmpty y then combine_rle_isEmpty ((i + j,x)::xs)
else (i,x)::combine_rle_isEmpty ((j,y)::xs)
[combine_rle_isEmpty_pre] Theorem
⊢ combine_rle_isEmpty_pre xs
[combine_rle_isEmpty_pre_cases] Theorem
⊢ ∀a0.
combine_rle_isEmpty_pre a0 ⇔
∀v0 v1.
a0 = v0::v1 ⇒
∀v0' v1'.
v1 = v0'::v1' ⇒
∀v0'' v1''.
v0' = (v0'',v1'') ⇒
∀v0'³' v1'³'.
v0 = (v0'³',v1'³') ⇒
(isEmpty v1'³' ∧ isEmpty v1'' ⇒
combine_rle_isEmpty_pre ((v0'³' + v0'',v1'³')::v1')) ∧
((isEmpty v1'³' ⇒ v1'' ≠ LN) ⇒
combine_rle_isEmpty_pre ((v0'',v1'')::v1'))
[combine_rle_isEmpty_pre_ind] Theorem
⊢ ∀combine_rle_isEmpty_pre'.
(∀xs.
(∀v0 v1.
xs = v0::v1 ⇒
∀v0' v1'.
v1 = v0'::v1' ⇒
∀v0'' v1''.
v0' = (v0'',v1'') ⇒
∀v0'³' v1'³'.
v0 = (v0'³',v1'³') ⇒
(isEmpty v1'³' ∧ isEmpty v1'' ⇒
combine_rle_isEmpty_pre' ((v0'³' + v0'',v1'³')::v1')) ∧
((isEmpty v1'³' ⇒ v1'' ≠ LN) ⇒
combine_rle_isEmpty_pre' ((v0'',v1'')::v1'))) ⇒
combine_rle_isEmpty_pre' xs) ⇒
∀a0. combine_rle_isEmpty_pre a0 ⇒ combine_rle_isEmpty_pre' a0
[combine_rle_isEmpty_pre_rules] Theorem
⊢ ∀xs.
(∀v0 v1.
xs = v0::v1 ⇒
∀v0' v1'.
v1 = v0'::v1' ⇒
∀v0'' v1''.
v0' = (v0'',v1'') ⇒
∀v0'³' v1'³'.
v0 = (v0'³',v1'³') ⇒
(isEmpty v1'³' ∧ isEmpty v1'' ⇒
combine_rle_isEmpty_pre ((v0'³' + v0'',v1'³')::v1')) ∧
((isEmpty v1'³' ⇒ v1'' ≠ LN) ⇒
combine_rle_isEmpty_pre ((v0'',v1'')::v1'))) ⇒
combine_rle_isEmpty_pre xs
[combine_rle_isEmpty_pre_strongind] Theorem
⊢ ∀combine_rle_isEmpty_pre'.
(∀xs.
(∀v0 v1.
xs = v0::v1 ⇒
∀v0' v1'.
v1 = v0'::v1' ⇒
∀v0'' v1''.
v0' = (v0'',v1'') ⇒
∀v0'³' v1'³'.
v0 = (v0'³',v1'³') ⇒
(isEmpty v1'³' ∧ isEmpty v1'' ⇒
combine_rle_isEmpty_pre ((v0'³' + v0'',v1'³')::v1') ∧
combine_rle_isEmpty_pre' ((v0'³' + v0'',v1'³')::v1')) ∧
((isEmpty v1'³' ⇒ v1'' ≠ LN) ⇒
combine_rle_isEmpty_pre ((v0'',v1'')::v1') ∧
combine_rle_isEmpty_pre' ((v0'',v1'')::v1'))) ⇒
combine_rle_isEmpty_pre' xs) ⇒
∀a0. combine_rle_isEmpty_pre a0 ⇒ combine_rle_isEmpty_pre' a0
[cv_ALL_DISTINCT_thm] Theorem
[oracles: DISK_THM] [axioms: ] [from_to f_a t_a]
⊢ b2c (ALL_DISTINCT v) = cv_ALL_DISTINCT (from_list f_a v)
[cv_ALOOKUP_thm] Theorem
[oracles: DISK_THM] [axioms: ] [from_to f_b t_b]
⊢ from_option f_a (ALOOKUP v q) =
cv_ALOOKUP (from_list (from_pair f_b f_a) v) (f_b q)
[cv_APPEND_def] Theorem
⊢ ∀cv_v cv_l.
cv_APPEND cv_v cv_l =
cv_if (cv_ispair cv_v)
(Pair (cv_fst cv_v) (cv_APPEND (cv_snd cv_v) cv_l)) cv_l
[cv_APPEND_ind] Theorem
⊢ ∀P. (∀cv_v cv_l.
(cv$c2b (cv_ispair cv_v) ⇒ P (cv_snd cv_v) cv_l) ⇒
P cv_v cv_l) ⇒
∀v v1. P v v1
[cv_APPEND_thm] Theorem
⊢ from_list f_a (v ⧺ l) =
cv_APPEND (from_list f_a v) (from_list f_a l)
[cv_DROP_thm] Theorem
⊢ from_list f_a (DROP n v) = cv_DROP (Num n) (from_list f_a v)
[cv_EL_thm] Theorem
⊢ EL_pre v l ⇒ f_a (EL v l) = cv_EL (Num v) (from_list f_a l)
[cv_FLAT_def] Theorem
⊢ ∀cv_v.
cv_FLAT cv_v =
cv_if (cv_ispair cv_v)
(cv_APPEND (cv_fst cv_v) (cv_FLAT (cv_snd cv_v))) (Num 0)
[cv_FLAT_ind] Theorem
⊢ ∀P. (∀cv_v. (cv$c2b (cv_ispair cv_v) ⇒ P (cv_snd cv_v)) ⇒ P cv_v) ⇒
∀v. P v
[cv_FLAT_thm] Theorem
⊢ from_list f_a (FLAT v) = cv_FLAT (from_list (from_list f_a) v)
[cv_FOLDL_lam_lam_pair_CASE_lam_la_thm] Theorem
⊢ from_pair Num (from_sptree_sptree_spt f_a)
(FOLDL_lam_lam_pair_CASE_lam_la x_v x_e) =
cv_FOLDL_lam_lam_pair_CASE_lam_la (from_list f_a x_v)
(from_pair Num (from_sptree_sptree_spt f_a) x_e)
[cv_FRONT_def] Theorem
⊢ ∀cv_v.
cv_FRONT cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_ispair (cv_snd cv_v))
(Pair (cv_fst cv_v) (cv_FRONT (cv_snd cv_v))) (Num 0))
(Num 0)
[cv_FRONT_ind] Theorem
⊢ ∀P. (∀cv_v.
(cv$c2b (cv_ispair cv_v) ∧ cv$c2b (cv_ispair (cv_snd cv_v)) ⇒
P (cv_snd cv_v)) ⇒
P cv_v) ⇒
∀v. P v
[cv_FRONT_thm] Theorem
⊢ FRONT_pre v ⇒ from_list f_a (FRONT v) = cv_FRONT (from_list f_a v)
[cv_FST] Theorem
⊢ f_a (FST v) = cv_fst (from_pair f_a f_b v)
[cv_HD] Theorem
⊢ v ≠ [] ⇒ f_a (HD v) = cv_fst (from_list f_a v)
[cv_INDEX_OF_def] Theorem
⊢ ∀cv_x cv_v.
cv_INDEX_OF cv_x cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_eq cv_x (cv_fst cv_v)) (Pair (Num 1) (Num 0))
(let
cv0 = cv_INDEX_OF cv_x (cv_snd cv_v)
in
cv_if (cv_ispair cv0)
(Pair (Num 1) (cv_add (cv_snd cv0) (Num 1))) (Num 0)))
(Num 0)
[cv_INDEX_OF_ind] Theorem
⊢ ∀P. (∀cv_x cv_v.
(cv$c2b (cv_ispair cv_v) ∧
¬cv$c2b (cv_eq cv_x (cv_fst cv_v)) ⇒ P cv_x (cv_snd cv_v)) ⇒
P cv_x cv_v) ⇒
∀v v1. P v v1
[cv_INDEX_OF_thm] Theorem
[oracles: DISK_THM] [axioms: ] [from_to f_a t_a]
⊢ INDEX_OF_pre x v ⇒
from_option Num (INDEX_OF x v) =
cv_INDEX_OF (f_a x) (from_list f_a v)
[cv_ISL_thm] Theorem
⊢ b2c (ISL v) = cv_ISL (from_sum f_a f_b v)
[cv_ISR_thm] Theorem
⊢ b2c (ISR v) = cv_ISR (from_sum f_a f_b v)
[cv_IS_NONE] Theorem
⊢ b2c (IS_NONE v) = cv_sub (Num 1) (cv_ispair (from_option f_a v))
[cv_IS_SOME] Theorem
⊢ b2c (IS_SOME v) = cv_ispair (from_option f_a v)
[cv_LAST_thm] Theorem
⊢ LAST_pre v ⇒ f_a (LAST v) = cv_LAST (from_list f_a v)
[cv_LENGTH_thm] Theorem
⊢ Num (LENGTH L) = cv_LENGTH (from_list f_a L)
[cv_LEN_thm] Theorem
⊢ Num (LEN v n) = cv_LEN (from_list f_a v) (Num n)
[cv_LUPDATE_def] Theorem
⊢ ∀cv_v cv_n cv_e.
cv_LUPDATE cv_e cv_n cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 0) cv_n)
(Pair (cv_fst cv_v)
(cv_LUPDATE cv_e (cv_sub cv_n (Num 1)) (cv_snd cv_v)))
(Pair cv_e (cv_snd cv_v))) (Num 0)
[cv_LUPDATE_ind] Theorem
⊢ ∀P. (∀cv_e cv_n cv_v.
(cv$c2b (cv_ispair cv_v) ∧ cv$c2b (cv_lt (Num 0) cv_n) ⇒
P cv_e (cv_sub cv_n (Num 1)) (cv_snd cv_v)) ⇒
P cv_e cv_n cv_v) ⇒
∀v v1 v2. P v v1 v2
[cv_LUPDATE_thm] Theorem
⊢ from_list f_a (LUPDATE e n v) =
cv_LUPDATE (f_a e) (Num n) (from_list f_a v)
[cv_MAP_FST] Theorem
⊢ from_list a (MAP FST l) = cv_map_fst (from_list (from_pair a b) l)
[cv_MAP_SND] Theorem
⊢ from_list b (MAP SND l) = cv_map_snd (from_list (from_pair a b) l)
[cv_NULL_thm] Theorem
⊢ b2c (NULL v) = cv_NULL (from_list f_a v)
[cv_OUTL_thm] Theorem
⊢ OUTL_pre v ⇒ f_a (OUTL v) = cv_OUTL (from_sum f_a f_b v)
[cv_OUTR_thm] Theorem
⊢ OUTR_pre v ⇒ f_b (OUTR v) = cv_OUTR (from_sum f_a f_b v)
[cv_PAD_LEFT_thm] Theorem
⊢ from_list f_a (PAD_LEFT c n s) =
cv_PAD_LEFT (f_a c) (Num n) (from_list f_a s)
[cv_PAD_RIGHT_thm] Theorem
⊢ from_list f_a (PAD_RIGHT c n s) =
cv_PAD_RIGHT (f_a c) (Num n) (from_list f_a s)
[cv_REPLICATE_thm] Theorem
⊢ from_list f_a (REPLICATE n c) = cv_REPLICATE (Num n) (f_a c)
[cv_REVERSE_thm] Theorem
⊢ from_list f_a (REVERSE L) = cv_REVERSE (from_list f_a L)
[cv_REV_thm] Theorem
⊢ from_list f_a (REV v acc) =
cv_REV (from_list f_a v) (from_list f_a acc)
[cv_SND] Theorem
⊢ f_b (SND v) = cv_snd (from_pair f_a f_b v)
[cv_SNOC_def] Theorem
⊢ ∀cv_x cv_v.
cv_SNOC cv_x cv_v =
cv_if (cv_ispair cv_v)
(Pair (cv_fst cv_v) (cv_SNOC cv_x (cv_snd cv_v)))
(Pair cv_x (Num 0))
[cv_SNOC_ind] Theorem
⊢ ∀P. (∀cv_x cv_v.
(cv$c2b (cv_ispair cv_v) ⇒ P cv_x (cv_snd cv_v)) ⇒
P cv_x cv_v) ⇒
∀v v1. P v v1
[cv_SNOC_thm] Theorem
⊢ from_list f_a (SNOC x v) = cv_SNOC (f_a x) (from_list f_a v)
[cv_SUM_ACC_thm] Theorem
⊢ Num (SUM_ACC v acc) = cv_SUM_ACC (from_list Num v) (Num acc)
[cv_SUM_thm] Theorem
⊢ Num (SUM L) = cv_SUM (from_list Num L)
[cv_TAKE_def] Theorem
⊢ ∀cv_v cv_n.
cv_TAKE cv_n cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 0) cv_n)
(Pair (cv_fst cv_v)
(cv_TAKE (cv_sub cv_n (Num 1)) (cv_snd cv_v))) (Num 0))
(Num 0)
[cv_TAKE_ind] Theorem
⊢ ∀P. (∀cv_n cv_v.
(cv$c2b (cv_ispair cv_v) ∧ cv$c2b (cv_lt (Num 0) cv_n) ⇒
P (cv_sub cv_n (Num 1)) (cv_snd cv_v)) ⇒
P cv_n cv_v) ⇒
∀v v1. P v v1
[cv_TAKE_thm] Theorem
⊢ from_list f_a (TAKE n v) = cv_TAKE (Num n) (from_list f_a v)
[cv_THE] Theorem
⊢ v ≠ NONE ⇒ f_a (THE v) = cv_snd (from_option f_a v)
[cv_TL] Theorem
⊢ from_list f_a (TL v) = cv_snd (from_list f_a v)
[cv_UNZIP_def] Theorem
⊢ ∀cv_ts.
cv_UNZIP cv_ts =
cv_if (cv_ispair cv_ts)
(let
cv0 = cv_UNZIP (cv_snd cv_ts)
in
cv_if (cv_ispair cv0)
(Pair (Pair (cv_fst (cv_fst cv_ts)) (cv_fst cv0))
(Pair (cv_snd (cv_fst cv_ts)) (cv_snd cv0))) (Num 0))
(Pair (Num 0) (Num 0))
[cv_UNZIP_ind] Theorem
⊢ ∀P. (∀cv_ts.
(cv$c2b (cv_ispair cv_ts) ⇒ P (cv_snd cv_ts)) ⇒ P cv_ts) ⇒
∀v. P v
[cv_UNZIP_thm] Theorem
⊢ from_pair (from_list f_a) (from_list f_b) (UNZIP ts) =
cv_UNZIP (from_list (from_pair f_a f_b) ts)
[cv_ZIP_def] Theorem
⊢ ∀cv_v.
cv_ZIP cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_ispair (cv_fst cv_v))
(cv_if (cv_ispair (cv_snd cv_v))
(Pair
(Pair (cv_fst (cv_fst cv_v)) (cv_fst (cv_snd cv_v)))
(cv_ZIP
(Pair (cv_snd (cv_fst cv_v)) (cv_snd (cv_snd cv_v)))))
(Num 0)) (Num 0)) (Num 0)
[cv_ZIP_ind] Theorem
⊢ ∀P. (∀cv_v.
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_ispair (cv_fst cv_v)) ∧
cv$c2b (cv_ispair (cv_snd cv_v)) ⇒
P (Pair (cv_snd (cv_fst cv_v)) (cv_snd (cv_snd cv_v)))) ⇒
P cv_v) ⇒
∀v. P v
[cv_ZIP_thm] Theorem
⊢ from_list (from_pair f_a f_b) (ZIP v) =
cv_ZIP (from_pair (from_list f_a) (from_list f_b) v)
[cv_alist_insert_def] Theorem
⊢ ∀cv_v0 cv_v cv_t.
cv_alist_insert cv_v0 cv_v cv_t =
(let
cv0 = Pair cv_v0 cv_v
in
cv_if (cv_ispair cv0)
(cv_if (cv_ispair (cv_fst cv0))
(cv_if (cv_ispair (cv_snd cv0))
(cv_insert (cv_fst (cv_fst cv0)) (cv_fst (cv_snd cv0))
(cv_alist_insert (cv_snd (cv_fst cv0))
(cv_snd (cv_snd cv0)) cv_t)) cv_t) cv_t) (Num 0))
[cv_alist_insert_ind] Theorem
⊢ ∀P. (∀cv_v0 cv_v cv_t.
(∀cv0.
cv0 = Pair cv_v0 cv_v ∧ cv$c2b (cv_ispair cv0) ∧
cv$c2b (cv_ispair (cv_fst cv0)) ∧
cv$c2b (cv_ispair (cv_snd cv0)) ⇒
P (cv_snd (cv_fst cv0)) (cv_snd (cv_snd cv0)) cv_t) ⇒
P cv_v0 cv_v cv_t) ⇒
∀v v1 v2. P v v1 v2
[cv_alist_insert_thm] Theorem
⊢ from_sptree_sptree_spt f_a (alist_insert v0 v t) =
cv_alist_insert (from_list Num v0) (from_list f_a v)
(from_sptree_sptree_spt f_a t)
[cv_apsnd_cons_thm] Theorem
⊢ from_pair f_a (from_list f_b) (apsnd_cons x v) =
cv_apsnd_cons (f_b x) (from_pair f_a (from_list f_b) v)
[cv_combine_rle_isEmpty_def] Theorem
⊢ ∀cv_xs.
cv_combine_rle_isEmpty cv_xs =
cv_if (cv_ispair cv_xs)
(cv_if (cv_ispair (cv_snd cv_xs))
(cv_if (cv_ispair (cv_fst (cv_snd cv_xs)))
(cv_if (cv_ispair (cv_fst cv_xs))
(cv_if
(cv_if (cv_eq (cv_snd (cv_fst cv_xs)) (Num 0))
(cv_eq (cv_snd (cv_fst (cv_snd cv_xs))) (Num 0))
(Num 0))
(cv_combine_rle_isEmpty
(Pair
(Pair
(cv_add (cv_fst (cv_fst cv_xs))
(cv_fst (cv_fst (cv_snd cv_xs))))
(cv_snd (cv_fst cv_xs)))
(cv_snd (cv_snd cv_xs))))
(Pair
(Pair (cv_fst (cv_fst cv_xs))
(cv_snd (cv_fst cv_xs)))
(cv_combine_rle_isEmpty
(Pair
(Pair (cv_fst (cv_fst (cv_snd cv_xs)))
(cv_snd (cv_fst (cv_snd cv_xs))))
(cv_snd (cv_snd cv_xs)))))) (Num 0))
(Num 0)) (Pair (cv_fst cv_xs) (Num 0))) (Num 0)
[cv_combine_rle_isEmpty_ind] Theorem
⊢ ∀P. (∀cv_xs.
(cv$c2b (cv_ispair cv_xs) ∧
cv$c2b (cv_ispair (cv_snd cv_xs)) ∧
cv$c2b (cv_ispair (cv_fst (cv_snd cv_xs))) ∧
cv$c2b (cv_ispair (cv_fst cv_xs)) ∧
cv$c2b
(cv_if (cv_eq (cv_snd (cv_fst cv_xs)) (Num 0))
(cv_eq (cv_snd (cv_fst (cv_snd cv_xs))) (Num 0))
(Num 0)) ⇒
P
(Pair
(Pair
(cv_add (cv_fst (cv_fst cv_xs))
(cv_fst (cv_fst (cv_snd cv_xs))))
(cv_snd (cv_fst cv_xs))) (cv_snd (cv_snd cv_xs)))) ∧
(cv$c2b (cv_ispair cv_xs) ∧
cv$c2b (cv_ispair (cv_snd cv_xs)) ∧
cv$c2b (cv_ispair (cv_fst (cv_snd cv_xs))) ∧
cv$c2b (cv_ispair (cv_fst cv_xs)) ∧
¬cv$c2b
(cv_if (cv_eq (cv_snd (cv_fst cv_xs)) (Num 0))
(cv_eq (cv_snd (cv_fst (cv_snd cv_xs))) (Num 0))
(Num 0)) ⇒
P
(Pair
(Pair (cv_fst (cv_fst (cv_snd cv_xs)))
(cv_snd (cv_fst (cv_snd cv_xs))))
(cv_snd (cv_snd cv_xs)))) ⇒
P cv_xs) ⇒
∀v. P v
[cv_combine_rle_isEmpty_thm] Theorem
[oracles: DISK_THM] [axioms: ] [from_to f_a t_a]
⊢ combine_rle_isEmpty_pre xs ⇒
from_list (from_pair Num (from_sptree_sptree_spt f_a))
(combine_rle_isEmpty xs) =
cv_combine_rle_isEmpty
(from_list (from_pair Num (from_sptree_sptree_spt f_a)) xs)
[cv_delete_def] Theorem
⊢ ∀cv_v cv_k.
cv_delete cv_k cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 1) (cv_fst cv_v))
(cv_if (cv_lt (Num 2) (cv_fst cv_v))
(cv_if (cv_lt (Num 0) cv_k)
(cv_if (cv_sub (Num 1) (cv_mod cv_k (Num 2)))
(cv_mk_BS
(cv_delete
(cv_div (cv_sub cv_k (Num 1)) (Num 2))
(cv_fst (cv_snd cv_v)))
(cv_fst (cv_snd (cv_snd cv_v)))
(cv_snd (cv_snd (cv_snd cv_v))))
(cv_mk_BS (cv_fst (cv_snd cv_v))
(cv_fst (cv_snd (cv_snd cv_v)))
(cv_delete
(cv_div (cv_sub cv_k (Num 1)) (Num 2))
(cv_snd (cv_snd (cv_snd cv_v))))))
(Pair (Num 2)
(Pair (cv_fst (cv_snd cv_v))
(cv_snd (cv_snd (cv_snd cv_v))))))
(cv_if (cv_lt (Num 0) cv_k)
(cv_if (cv_sub (Num 1) (cv_mod cv_k (Num 2)))
(cv_mk_BN
(cv_delete
(cv_div (cv_sub cv_k (Num 1)) (Num 2))
(cv_fst (cv_snd cv_v)))
(cv_snd (cv_snd cv_v)))
(cv_mk_BN (cv_fst (cv_snd cv_v))
(cv_delete
(cv_div (cv_sub cv_k (Num 1)) (Num 2))
(cv_snd (cv_snd cv_v)))))
(Pair (Num 2)
(Pair (cv_fst (cv_snd cv_v)) (cv_snd (cv_snd cv_v))))))
(cv_if (cv_lt (Num 0) cv_k) (Pair (Num 1) (cv_snd cv_v))
(Num 0))) (Num 0)
[cv_delete_ind] Theorem
⊢ ∀P. (∀cv_k cv_v.
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 0) cv_k) ∧
cv$c2b (cv_sub (Num 1) (cv_mod cv_k (Num 2))) ⇒
P (cv_div (cv_sub cv_k (Num 1)) (Num 2))
(cv_fst (cv_snd cv_v))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 0) cv_k) ∧
¬cv$c2b (cv_sub (Num 1) (cv_mod cv_k (Num 2))) ⇒
P (cv_div (cv_sub cv_k (Num 1)) (Num 2))
(cv_snd (cv_snd (cv_snd cv_v)))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 0) cv_k) ∧
cv$c2b (cv_sub (Num 1) (cv_mod cv_k (Num 2))) ⇒
P (cv_div (cv_sub cv_k (Num 1)) (Num 2))
(cv_fst (cv_snd cv_v))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 0) cv_k) ∧
¬cv$c2b (cv_sub (Num 1) (cv_mod cv_k (Num 2))) ⇒
P (cv_div (cv_sub cv_k (Num 1)) (Num 2))
(cv_snd (cv_snd cv_v))) ⇒
P cv_k cv_v) ⇒
∀v v1. P v v1
[cv_delete_thm] Theorem
⊢ from_sptree_sptree_spt f_a (delete k v) =
cv_delete (Num k) (from_sptree_sptree_spt f_a v)
[cv_difference_def] Theorem
⊢ ∀cv_v cv_t.
cv_difference cv_v cv_t =
cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 1) (cv_fst cv_v))
(cv_if (cv_lt (Num 2) (cv_fst cv_v))
(cv_if (cv_ispair cv_t)
(cv_if (cv_lt (Num 1) (cv_fst cv_t))
(cv_if (cv_lt (Num 2) (cv_fst cv_t))
(cv_mk_BN
(cv_difference (cv_fst (cv_snd cv_v))
(cv_fst (cv_snd cv_t)))
(cv_difference
(cv_snd (cv_snd (cv_snd cv_v)))
(cv_snd (cv_snd (cv_snd cv_t)))))
(cv_mk_BS
(cv_difference (cv_fst (cv_snd cv_v))
(cv_fst (cv_snd cv_t)))
(cv_fst (cv_snd (cv_snd cv_v)))
(cv_difference
(cv_snd (cv_snd (cv_snd cv_v)))
(cv_snd (cv_snd cv_t)))))
(Pair (Num 2)
(Pair (cv_fst (cv_snd cv_v))
(cv_snd (cv_snd (cv_snd cv_v))))))
(Pair (Num 3)
(Pair (cv_fst (cv_snd cv_v))
(Pair (cv_fst (cv_snd (cv_snd cv_v)))
(cv_snd (cv_snd (cv_snd cv_v)))))))
(cv_if (cv_ispair cv_t)
(cv_if (cv_lt (Num 1) (cv_fst cv_t))
(cv_if (cv_lt (Num 2) (cv_fst cv_t))
(cv_mk_BN
(cv_difference (cv_fst (cv_snd cv_v))
(cv_fst (cv_snd cv_t)))
(cv_difference (cv_snd (cv_snd cv_v))
(cv_snd (cv_snd (cv_snd cv_t)))))
(cv_mk_BN
(cv_difference (cv_fst (cv_snd cv_v))
(cv_fst (cv_snd cv_t)))
(cv_difference (cv_snd (cv_snd cv_v))
(cv_snd (cv_snd cv_t)))))
(Pair (Num 2)
(Pair (cv_fst (cv_snd cv_v))
(cv_snd (cv_snd cv_v)))))
(Pair (Num 2)
(Pair (cv_fst (cv_snd cv_v)) (cv_snd (cv_snd cv_v))))))
(cv_if (cv_ispair cv_t)
(cv_if (cv_lt (Num 1) (cv_fst cv_t))
(cv_if (cv_lt (Num 2) (cv_fst cv_t)) (Num 0)
(Pair (Num 1) (cv_snd cv_v))) (Num 0))
(Pair (Num 1) (cv_snd cv_v)))) (Num 0)
[cv_difference_ind] Theorem
⊢ ∀P. (∀cv_v cv_t.
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_ispair cv_t) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_t)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_t)) ⇒
P (cv_fst (cv_snd cv_v)) (cv_fst (cv_snd cv_t))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_ispair cv_t) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_t)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_t)) ⇒
P (cv_snd (cv_snd (cv_snd cv_v)))
(cv_snd (cv_snd (cv_snd cv_t)))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_ispair cv_t) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_t)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_t)) ⇒
P (cv_fst (cv_snd cv_v)) (cv_fst (cv_snd cv_t))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_ispair cv_t) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_t)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_t)) ⇒
P (cv_snd (cv_snd (cv_snd cv_v))) (cv_snd (cv_snd cv_t))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_ispair cv_t) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_t)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_t)) ⇒
P (cv_fst (cv_snd cv_v)) (cv_fst (cv_snd cv_t))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_ispair cv_t) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_t)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_t)) ⇒
P (cv_snd (cv_snd cv_v)) (cv_snd (cv_snd (cv_snd cv_t)))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_ispair cv_t) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_t)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_t)) ⇒
P (cv_fst (cv_snd cv_v)) (cv_fst (cv_snd cv_t))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_ispair cv_t) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_t)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_t)) ⇒
P (cv_snd (cv_snd cv_v)) (cv_snd (cv_snd cv_t))) ⇒
P cv_v cv_t) ⇒
∀v v1. P v v1
[cv_difference_thm] Theorem
⊢ from_sptree_sptree_spt f_a (difference v t) =
cv_difference (from_sptree_sptree_spt f_a v)
(from_sptree_sptree_spt f_b t)
[cv_every_empty_snd_thm] Theorem
[oracles: DISK_THM] [axioms: ] [from_to f_b t_b]
⊢ b2c (every_empty_snd v) =
cv_every_empty_snd
(from_list (from_pair f_a (from_sptree_sptree_spt f_b)) v)
[cv_findi_def] Theorem
⊢ ∀cv_x cv_v.
cv_findi cv_x cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_eq cv_x (cv_fst cv_v)) (Num 0)
(cv_add (Num 1) (cv_findi cv_x (cv_snd cv_v)))) (Num 0)
[cv_findi_ind] Theorem
⊢ ∀P. (∀cv_x cv_v.
(cv$c2b (cv_ispair cv_v) ∧
¬cv$c2b (cv_eq cv_x (cv_fst cv_v)) ⇒ P cv_x (cv_snd cv_v)) ⇒
P cv_x cv_v) ⇒
∀v v1. P v v1
[cv_findi_thm] Theorem
[oracles: DISK_THM] [axioms: ] [from_to f_a t_a]
⊢ Num (findi x v) = cv_findi (f_a x) (from_list f_a v)
[cv_fromList_thm] Theorem
⊢ from_sptree_sptree_spt f_a (fromList l) =
cv_fromList (from_list f_a l)
[cv_insert_def] Theorem
⊢ ∀cv_v cv_k cv_a.
cv_insert cv_k cv_a cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 1) (cv_fst cv_v))
(cv_if (cv_lt (Num 2) (cv_fst cv_v))
(cv_if (cv_lt (Num 0) cv_k)
(cv_if (cv_sub (Num 1) (cv_mod cv_k (Num 2)))
(Pair (Num 3)
(Pair
(cv_insert
(cv_div (cv_sub cv_k (Num 1)) (Num 2))
cv_a (cv_fst (cv_snd cv_v)))
(Pair (cv_fst (cv_snd (cv_snd cv_v)))
(cv_snd (cv_snd (cv_snd cv_v))))))
(Pair (Num 3)
(Pair (cv_fst (cv_snd cv_v))
(Pair (cv_fst (cv_snd (cv_snd cv_v)))
(cv_insert
(cv_div (cv_sub cv_k (Num 1)) (Num 2))
cv_a (cv_snd (cv_snd (cv_snd cv_v))))))))
(Pair (Num 3)
(Pair (cv_fst (cv_snd cv_v))
(Pair cv_a (cv_snd (cv_snd (cv_snd cv_v)))))))
(cv_if (cv_lt (Num 0) cv_k)
(cv_if (cv_sub (Num 1) (cv_mod cv_k (Num 2)))
(Pair (Num 2)
(Pair
(cv_insert
(cv_div (cv_sub cv_k (Num 1)) (Num 2))
cv_a (cv_fst (cv_snd cv_v)))
(cv_snd (cv_snd cv_v))))
(Pair (Num 2)
(Pair (cv_fst (cv_snd cv_v))
(cv_insert
(cv_div (cv_sub cv_k (Num 1)) (Num 2))
cv_a (cv_snd (cv_snd cv_v))))))
(Pair (Num 3)
(Pair (cv_fst (cv_snd cv_v))
(Pair cv_a (cv_snd (cv_snd cv_v)))))))
(cv_if (cv_lt (Num 0) cv_k)
(cv_if (cv_sub (Num 1) (cv_mod cv_k (Num 2)))
(Pair (Num 3)
(Pair
(cv_insert
(cv_div (cv_sub cv_k (Num 1)) (Num 2)) cv_a
(Num 0)) (Pair (cv_snd cv_v) (Num 0))))
(Pair (Num 3)
(Pair (Num 0)
(Pair (cv_snd cv_v)
(cv_insert
(cv_div (cv_sub cv_k (Num 1)) (Num 2))
cv_a (Num 0)))))) (Pair (Num 1) cv_a)))
(cv_if (cv_lt (Num 0) cv_k)
(cv_if (cv_sub (Num 1) (cv_mod cv_k (Num 2)))
(Pair (Num 2)
(Pair
(cv_insert (cv_div (cv_sub cv_k (Num 1)) (Num 2))
cv_a (Num 0)) (Num 0)))
(Pair (Num 2)
(Pair (Num 0)
(cv_insert (cv_div (cv_sub cv_k (Num 1)) (Num 2))
cv_a (Num 0))))) (Pair (Num 1) cv_a))
[cv_insert_ind] Theorem
⊢ ∀P. (∀cv_k cv_a cv_v.
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 0) cv_k) ∧
cv$c2b (cv_sub (Num 1) (cv_mod cv_k (Num 2))) ⇒
P (cv_div (cv_sub cv_k (Num 1)) (Num 2)) cv_a
(cv_fst (cv_snd cv_v))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 0) cv_k) ∧
¬cv$c2b (cv_sub (Num 1) (cv_mod cv_k (Num 2))) ⇒
P (cv_div (cv_sub cv_k (Num 1)) (Num 2)) cv_a
(cv_snd (cv_snd (cv_snd cv_v)))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 0) cv_k) ∧
cv$c2b (cv_sub (Num 1) (cv_mod cv_k (Num 2))) ⇒
P (cv_div (cv_sub cv_k (Num 1)) (Num 2)) cv_a
(cv_fst (cv_snd cv_v))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 0) cv_k) ∧
¬cv$c2b (cv_sub (Num 1) (cv_mod cv_k (Num 2))) ⇒
P (cv_div (cv_sub cv_k (Num 1)) (Num 2)) cv_a
(cv_snd (cv_snd cv_v))) ∧
(cv$c2b (cv_ispair cv_v) ∧
¬cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 0) cv_k) ∧
cv$c2b (cv_sub (Num 1) (cv_mod cv_k (Num 2))) ⇒
P (cv_div (cv_sub cv_k (Num 1)) (Num 2)) cv_a (Num 0)) ∧
(cv$c2b (cv_ispair cv_v) ∧
¬cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 0) cv_k) ∧
¬cv$c2b (cv_sub (Num 1) (cv_mod cv_k (Num 2))) ⇒
P (cv_div (cv_sub cv_k (Num 1)) (Num 2)) cv_a (Num 0)) ∧
(¬cv$c2b (cv_ispair cv_v) ∧ cv$c2b (cv_lt (Num 0) cv_k) ∧
cv$c2b (cv_sub (Num 1) (cv_mod cv_k (Num 2))) ⇒
P (cv_div (cv_sub cv_k (Num 1)) (Num 2)) cv_a (Num 0)) ∧
(¬cv$c2b (cv_ispair cv_v) ∧ cv$c2b (cv_lt (Num 0) cv_k) ∧
¬cv$c2b (cv_sub (Num 1) (cv_mod cv_k (Num 2))) ⇒
P (cv_div (cv_sub cv_k (Num 1)) (Num 2)) cv_a (Num 0)) ⇒
P cv_k cv_a cv_v) ⇒
∀v v1 v2. P v v1 v2
[cv_insert_thm] Theorem
⊢ from_sptree_sptree_spt f_a (insert k a v) =
cv_insert (Num k) (f_a a) (from_sptree_sptree_spt f_a v)
[cv_inter_def] Theorem
⊢ ∀cv_v cv_t.
cv_inter cv_v cv_t =
cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 1) (cv_fst cv_v))
(cv_if (cv_lt (Num 2) (cv_fst cv_v))
(cv_if (cv_ispair cv_t)
(cv_if (cv_lt (Num 1) (cv_fst cv_t))
(cv_if (cv_lt (Num 2) (cv_fst cv_t))
(cv_mk_BS
(cv_inter (cv_fst (cv_snd cv_v))
(cv_fst (cv_snd cv_t)))
(cv_fst (cv_snd (cv_snd cv_v)))
(cv_inter (cv_snd (cv_snd (cv_snd cv_v)))
(cv_snd (cv_snd (cv_snd cv_t)))))
(cv_mk_BN
(cv_inter (cv_fst (cv_snd cv_v))
(cv_fst (cv_snd cv_t)))
(cv_inter (cv_snd (cv_snd (cv_snd cv_v)))
(cv_snd (cv_snd cv_t)))))
(Pair (Num 1) (cv_fst (cv_snd (cv_snd cv_v)))))
(Num 0))
(cv_if (cv_ispair cv_t)
(cv_if (cv_lt (Num 1) (cv_fst cv_t))
(cv_if (cv_lt (Num 2) (cv_fst cv_t))
(cv_mk_BN
(cv_inter (cv_fst (cv_snd cv_v))
(cv_fst (cv_snd cv_t)))
(cv_inter (cv_snd (cv_snd cv_v))
(cv_snd (cv_snd (cv_snd cv_t)))))
(cv_mk_BN
(cv_inter (cv_fst (cv_snd cv_v))
(cv_fst (cv_snd cv_t)))
(cv_inter (cv_snd (cv_snd cv_v))
(cv_snd (cv_snd cv_t))))) (Num 0)) (Num 0)))
(cv_if (cv_ispair cv_t)
(cv_if (cv_lt (Num 1) (cv_fst cv_t))
(cv_if (cv_lt (Num 2) (cv_fst cv_t))
(Pair (Num 1) (cv_snd cv_v)) (Num 0))
(Pair (Num 1) (cv_snd cv_v))) (Num 0))) (Num 0)
[cv_inter_ind] Theorem
⊢ ∀P. (∀cv_v cv_t.
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_ispair cv_t) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_t)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_t)) ⇒
P (cv_fst (cv_snd cv_v)) (cv_fst (cv_snd cv_t))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_ispair cv_t) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_t)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_t)) ⇒
P (cv_snd (cv_snd (cv_snd cv_v)))
(cv_snd (cv_snd (cv_snd cv_t)))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_ispair cv_t) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_t)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_t)) ⇒
P (cv_fst (cv_snd cv_v)) (cv_fst (cv_snd cv_t))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_ispair cv_t) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_t)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_t)) ⇒
P (cv_snd (cv_snd (cv_snd cv_v))) (cv_snd (cv_snd cv_t))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_ispair cv_t) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_t)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_t)) ⇒
P (cv_fst (cv_snd cv_v)) (cv_fst (cv_snd cv_t))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_ispair cv_t) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_t)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_t)) ⇒
P (cv_snd (cv_snd cv_v)) (cv_snd (cv_snd (cv_snd cv_t)))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_ispair cv_t) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_t)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_t)) ⇒
P (cv_fst (cv_snd cv_v)) (cv_fst (cv_snd cv_t))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_ispair cv_t) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_t)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_t)) ⇒
P (cv_snd (cv_snd cv_v)) (cv_snd (cv_snd cv_t))) ⇒
P cv_v cv_t) ⇒
∀v v1. P v v1
[cv_inter_thm] Theorem
⊢ from_sptree_sptree_spt f_a (inter v t) =
cv_inter (from_sptree_sptree_spt f_a v)
(from_sptree_sptree_spt f_b t)
[cv_isPREFIX_thm] Theorem
[oracles: DISK_THM] [axioms: ] [from_to f_a t_a]
⊢ b2c (v ≼ l) = cv_isPREFIX (from_list f_a v) (from_list f_a l)
[cv_list_insert_thm] Theorem
⊢ from_sptree_sptree_spt from_unit (list_insert v t) =
cv_list_insert (from_list Num v)
(from_sptree_sptree_spt from_unit t)
[cv_list_mem_thm] Theorem
[oracles: DISK_THM] [axioms: ] [from_to f_a t_a]
⊢ b2c (list_mem y v) = cv_list_mem (f_a y) (from_list f_a v)
[cv_list_to_num_set_def] Theorem
⊢ ∀cv_v.
cv_list_to_num_set cv_v =
cv_if (cv_ispair cv_v)
(cv_insert (cv_fst cv_v) (Num 0)
(cv_list_to_num_set (cv_snd cv_v))) (Num 0)
[cv_list_to_num_set_ind] Theorem
⊢ ∀P. (∀cv_v. (cv$c2b (cv_ispair cv_v) ⇒ P (cv_snd cv_v)) ⇒ P cv_v) ⇒
∀v. P v
[cv_list_to_num_set_thm] Theorem
⊢ from_sptree_sptree_spt from_unit (list_to_num_set v) =
cv_list_to_num_set (from_list Num v)
[cv_lookup_thm] Theorem
⊢ from_option f_a (lookup k v) =
cv_lookup (Num k) (from_sptree_sptree_spt f_a v)
[cv_lrnext_def] Theorem
⊢ ∀cv_n.
cv_lrnext cv_n =
cv_if (cv_lt (Num 0) cv_n)
(cv_mul (Num 2)
(cv_lrnext (cv_div (cv_sub cv_n (Num 1)) (Num 2)))) (Num 1)
[cv_lrnext_ind] Theorem
⊢ ∀P. (∀cv_n.
(cv$c2b (cv_lt (Num 0) cv_n) ⇒
P (cv_div (cv_sub cv_n (Num 1)) (Num 2))) ⇒
P cv_n) ⇒
∀v. P v
[cv_lrnext_thm] Theorem
⊢ Num (sptree$lrnext n) = cv_lrnext (Num n)
[cv_map_fst_def] Theorem
⊢ ∀cv.
cv_map_fst cv =
cv_if (cv_ispair cv)
(Pair (cv_fst (cv_fst cv)) (cv_map_fst (cv_snd cv))) (Num 0)
[cv_map_fst_ind] Theorem
⊢ ∀P. (∀cv. (cv$c2b (cv_ispair cv) ⇒ P (cv_snd cv)) ⇒ P cv) ⇒ ∀v. P v
[cv_map_snd_def] Theorem
⊢ ∀cv.
cv_map_snd cv =
cv_if (cv_ispair cv)
(Pair (cv_snd (cv_fst cv)) (cv_map_snd (cv_snd cv))) (Num 0)
[cv_map_snd_ind] Theorem
⊢ ∀P. (∀cv. (cv$c2b (cv_ispair cv) ⇒ P (cv_snd cv)) ⇒ P cv) ⇒ ∀v. P v
[cv_mk_BN_thm] Theorem
⊢ from_sptree_sptree_spt f_a (mk_BN v0 v) =
cv_mk_BN (from_sptree_sptree_spt f_a v0)
(from_sptree_sptree_spt f_a v)
[cv_mk_BS_thm] Theorem
⊢ from_sptree_sptree_spt f_a (mk_BS v0 x v) =
cv_mk_BS (from_sptree_sptree_spt f_a v0) (f_a x)
(from_sptree_sptree_spt f_a v)
[cv_mk_wf_def] Theorem
⊢ ∀cv_v.
cv_mk_wf cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 1) (cv_fst cv_v))
(cv_if (cv_lt (Num 2) (cv_fst cv_v))
(cv_mk_BS (cv_mk_wf (cv_fst (cv_snd cv_v)))
(cv_fst (cv_snd (cv_snd cv_v)))
(cv_mk_wf (cv_snd (cv_snd (cv_snd cv_v)))))
(cv_mk_BN (cv_mk_wf (cv_fst (cv_snd cv_v)))
(cv_mk_wf (cv_snd (cv_snd cv_v)))))
(Pair (Num 1) (cv_snd cv_v))) (Num 0)
[cv_mk_wf_ind] Theorem
⊢ ∀P. (∀cv_v.
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ⇒
P (cv_fst (cv_snd cv_v))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ⇒
P (cv_snd (cv_snd (cv_snd cv_v)))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ⇒
P (cv_fst (cv_snd cv_v))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ⇒
P (cv_snd (cv_snd cv_v))) ⇒
P cv_v) ⇒
∀v. P v
[cv_mk_wf_thm] Theorem
⊢ from_sptree_sptree_spt f_a (mk_wf v) =
cv_mk_wf (from_sptree_sptree_spt f_a v)
[cv_nub_def] Theorem
⊢ ∀cv_v.
cv_nub cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_list_mem (cv_fst cv_v) (cv_snd cv_v))
(cv_nub (cv_snd cv_v))
(Pair (cv_fst cv_v) (cv_nub (cv_snd cv_v)))) (Num 0)
[cv_nub_ind] Theorem
⊢ ∀P. (∀cv_v.
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_list_mem (cv_fst cv_v) (cv_snd cv_v)) ⇒
P (cv_snd cv_v)) ∧
(cv$c2b (cv_ispair cv_v) ∧
¬cv$c2b (cv_list_mem (cv_fst cv_v) (cv_snd cv_v)) ⇒
P (cv_snd cv_v)) ⇒
P cv_v) ⇒
∀v. P v
[cv_nub_thm] Theorem
[oracles: DISK_THM] [axioms: ] [from_to f_a t_a]
⊢ from_list f_a (nub v) = cv_nub (from_list f_a v)
[cv_oEL_thm] Theorem
⊢ from_option f_a (oEL n v) = cv_oEL (Num n) (from_list f_a v)
[cv_oHD_thm] Theorem
⊢ from_option f_a (oHD l) = cv_oHD (from_list f_a l)
[cv_rep_FEMPTY] Theorem
⊢ from_fmap f FEMPTY = Num 0
[cv_rep_FLOOKUP] Theorem
⊢ from_option f (FLOOKUP m n) = cv_lookup (Num n) (from_fmap f m)
[cv_rep_FUPDATE] Theorem
⊢ from_fmap f (m |+ (k,v)) = cv_insert (Num k) (f v) (from_fmap f m)
[cv_rep_MEM] Theorem
⊢ from_to f_a t_a ⇒
cv_rep T (cv_list_mem (f_a x) (from_list f_a xs)) b2c (MEM x xs)
[cv_rep_list_datatype] Theorem
⊢ (cv_rep p cv (from_list f_a) x ∧ cv_rep NIL_pre NIL_cv f_b f0 ∧
(∀v0 v1.
cv_rep (CONS_pre v0 v1) (CONS_cv (f_a v0) (from_list f_a v1))
f_b (f1 v0 v1)) ⇒
cv_rep
(p ∧ (x = [] ⇒ NIL_pre) ∧ ∀v0 v1. x = v0::v1 ⇒ CONS_pre v0 v1)
(cv_if (cv_ispair cv) (CONS_cv (cv_fst cv) (cv_snd cv)) NIL_cv)
f_b (list_CASE x f0 f1)) ∧ from_list f [] = Num 0 ∧
from_list f (x::xs) = Pair (f x) (from_list f xs)
[cv_rep_option_datatype] Theorem
⊢ (cv_rep p cv (from_option f_a) x ∧ cv_rep NONE_pre NONE_cv f_b f0 ∧
(∀v0. cv_rep (SOME_pre v0) (SOME_cv (f_a v0)) f_b (f1 v0)) ⇒
cv_rep
(p ∧ (x = NONE ⇒ NONE_pre) ∧ ∀v0. x = SOME v0 ⇒ SOME_pre v0)
(cv_if (cv_ispair cv) (SOME_cv (cv_snd cv)) NONE_cv) f_b
(option_CASE x f0 f1)) ∧ from_option f NONE = Num 0 ∧
from_option f (SOME x) = Pair (Num 1) (f x)
[cv_rep_pair_datatype] Theorem
⊢ (cv_rep p cv (from_pair f_b f_c) x ∧
(∀v0 v1.
cv_rep ($var$(,_pre) v0 v1) ($var$(,_cv) (f_b v0) (f_c v1)) f_a
(f0 v0 v1)) ⇒
cv_rep (p ∧ ∀v0 v1. x = (v0,v1) ⇒ $var$(,_pre) v0 v1)
(cv_if (cv_ispair cv) ($var$(,_cv) (cv_fst cv) (cv_snd cv))
(Num 0)) f_a (pair_CASE x f0)) ∧
from_pair f1 f2 (x,y) = Pair (f1 x) (f2 y)
[cv_rep_sptree_sptree_spt_datatype] Theorem
⊢ (cv_rep p cv (from_sptree_sptree_spt f_a) x ∧
cv_rep LN_pre LN_cv f_b f0 ∧
(∀v0. cv_rep (LS_pre v0) (LS_cv (f_a v0)) f_b (f1 v0)) ∧
(∀v0 v1.
cv_rep (BN_pre v0 v1)
(BN_cv (from_sptree_sptree_spt f_a v0)
(from_sptree_sptree_spt f_a v1)) f_b (f2 v0 v1)) ∧
(∀v0 v1 v2.
cv_rep (BS_pre v0 v1 v2)
(BS_cv (from_sptree_sptree_spt f_a v0) (f_a v1)
(from_sptree_sptree_spt f_a v2)) f_b (f3 v0 v1 v2)) ⇒
cv_rep
(p ∧ (isEmpty x ⇒ LN_pre) ∧ (∀v0. x = ⦕ 0 ↦ v0 ⦖ ⇒ LS_pre v0) ∧
(∀v0 v1. x = BN v0 v1 ⇒ BN_pre v0 v1) ∧
∀v0 v1 v2. x = BS v0 v1 v2 ⇒ BS_pre v0 v1 v2)
(cv_if (cv_ispair cv)
(cv_if (cv_lt (Num 1) (cv_fst cv))
(cv_if (cv_lt (Num 2) (cv_fst cv))
(BS_cv (cv_fst (cv_snd cv))
(cv_fst (cv_snd (cv_snd cv)))
(cv_snd (cv_snd (cv_snd cv))))
(BN_cv (cv_fst (cv_snd cv)) (cv_snd (cv_snd cv))))
(LS_cv (cv_snd cv))) LN_cv) f_b (spt_CASE x f0 f1 f2 f3)) ∧
from_sptree_sptree_spt f0 LN = Num 0 ∧
from_sptree_sptree_spt f0 ⦕ 0 ↦ v0 ⦖ = Pair (Num 1) (f0 v0) ∧
from_sptree_sptree_spt f0 (BN v0 v1) =
Pair (Num 2)
(Pair (from_sptree_sptree_spt f0 v0)
(from_sptree_sptree_spt f0 v1)) ∧
from_sptree_sptree_spt f0 (BS v0 v1 v2) =
Pair (Num 3)
(Pair (from_sptree_sptree_spt f0 v0)
(Pair (f0 v1) (from_sptree_sptree_spt f0 v2)))
[cv_rep_sum_datatype] Theorem
⊢ (cv_rep p cv (from_sum f_a f_b) x ∧
(∀v0. cv_rep (INL_pre v0) (INL_cv (f_a v0)) f_c (f0 v0)) ∧
(∀v0. cv_rep (INR_pre v0) (INR_cv (f_b v0)) f_c (f1 v0)) ⇒
cv_rep
(p ∧ (∀v0. x = INL v0 ⇒ INL_pre v0) ∧
∀v0. x = INR v0 ⇒ INR_pre v0)
(cv_if (cv_lt (Num 0) (cv_fst cv)) (INR_cv (cv_snd cv))
(cv_if (cv_ispair cv) (INL_cv (cv_snd cv)) (Num 0))) f_c
(sum_CASE x f0 f1)) ∧
from_sum f1 f2 (INL x) = Pair (Num 0) (f1 x) ∧
from_sum f1 f2 (INR y) = Pair (Num 1) (f2 y)
[cv_rep_unit_datatype] Theorem
⊢ (cv_rep p cv from_unit x ∧ cv_rep one_pre one_cv f_a f0 ⇒
cv_rep (p ∧ one_pre) one_cv f_a (one_CASE x f0)) ∧
from_unit () = Num 0
[cv_replicate_acc_thm] Theorem
⊢ from_list f_a (replicate_acc n x acc) =
cv_replicate_acc (Num n) (f_a x) (from_list f_a acc)
[cv_size'_def] Theorem
⊢ ∀cv_v.
cv_size' cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 1) (cv_fst cv_v))
(cv_if (cv_lt (Num 2) (cv_fst cv_v))
(cv_add
(cv_add (cv_size' (cv_fst (cv_snd cv_v)))
(cv_size' (cv_snd (cv_snd (cv_snd cv_v))))) (Num 1))
(cv_add (cv_size' (cv_fst (cv_snd cv_v)))
(cv_size' (cv_snd (cv_snd cv_v))))) (Num 1)) (Num 0)
[cv_size'_ind] Theorem
⊢ ∀P. (∀cv_v.
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ⇒
P (cv_fst (cv_snd cv_v))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ⇒
P (cv_snd (cv_snd (cv_snd cv_v)))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ⇒
P (cv_fst (cv_snd cv_v))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ⇒
P (cv_snd (cv_snd cv_v))) ⇒
P cv_v) ⇒
∀v. P v
[cv_size'_thm] Theorem
⊢ Num (size v) = cv_size' (from_sptree_sptree_spt f_a v)
[cv_spt_center_thm] Theorem
⊢ from_option f_a (spt_center v) =
cv_spt_center (from_sptree_sptree_spt f_a v)
[cv_spt_centers_def] Theorem
⊢ ∀cv_v cv_i.
cv_spt_centers cv_i cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_ispair (cv_fst cv_v))
(let
cv0 = cv_spt_center (cv_snd (cv_fst cv_v))
in
cv_if (cv_ispair cv0)
(cv_apsnd_cons (Pair cv_i (cv_snd cv0))
(cv_spt_centers (cv_add cv_i (cv_fst (cv_fst cv_v)))
(cv_snd cv_v)))
(cv_spt_centers (cv_add cv_i (cv_fst (cv_fst cv_v)))
(cv_snd cv_v))) (Num 0)) (Pair cv_i (Num 0))
[cv_spt_centers_ind] Theorem
⊢ ∀P. (∀cv_i cv_v.
(∀cv0.
cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_ispair (cv_fst cv_v)) ∧
cv0 = cv_spt_center (cv_snd (cv_fst cv_v)) ∧
cv$c2b (cv_ispair cv0) ⇒
P (cv_add cv_i (cv_fst (cv_fst cv_v))) (cv_snd cv_v)) ∧
(∀cv0.
cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_ispair (cv_fst cv_v)) ∧
cv0 = cv_spt_center (cv_snd (cv_fst cv_v)) ∧
¬cv$c2b (cv_ispair cv0) ⇒
P (cv_add cv_i (cv_fst (cv_fst cv_v))) (cv_snd cv_v)) ⇒
P cv_i cv_v) ⇒
∀v v1. P v v1
[cv_spt_centers_thm] Theorem
⊢ spt_centers_pre i v ⇒
from_pair Num (from_list (from_pair Num f_a)) (spt_centers i v) =
cv_spt_centers (Num i)
(from_list (from_pair Num (from_sptree_sptree_spt f_a)) v)
[cv_spt_left_thm] Theorem
⊢ from_sptree_sptree_spt f_a (spt_left v) =
cv_spt_left (from_sptree_sptree_spt f_a v)
[cv_spt_right_thm] Theorem
⊢ from_sptree_sptree_spt f_a (spt_right v) =
cv_spt_right (from_sptree_sptree_spt f_a v)
[cv_subspt_def] Theorem
⊢ ∀cv_v cv_t.
cv_subspt cv_v cv_t =
cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 1) (cv_fst cv_v))
(cv_if (cv_lt (Num 2) (cv_fst cv_v))
(cv_if
(cv_eq (cv_spt_center cv_t)
(Pair (Num 1) (cv_fst (cv_snd (cv_snd cv_v)))))
(cv_if
(cv_subspt (cv_fst (cv_snd cv_v))
(cv_spt_left cv_t))
(cv_subspt (cv_snd (cv_snd (cv_snd cv_v)))
(cv_spt_right cv_t)) (Num 0)) (Num 0))
(cv_if
(cv_subspt (cv_fst (cv_snd cv_v)) (cv_spt_left cv_t))
(cv_subspt (cv_snd (cv_snd cv_v)) (cv_spt_right cv_t))
(Num 0)))
(cv_eq (cv_spt_center cv_t) (Pair (Num 1) (cv_snd cv_v))))
(Num 1)
[cv_subspt_ind] Theorem
⊢ ∀P. (∀cv_v cv_t.
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ⇒
P (cv_fst (cv_snd cv_v)) (cv_spt_left cv_t)) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b
(cv_eq (cv_spt_center cv_t)
(Pair (Num 1) (cv_fst (cv_snd (cv_snd cv_v))))) ⇒
P (cv_fst (cv_snd cv_v)) (cv_spt_left cv_t)) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b
(cv_eq (cv_spt_center cv_t)
(Pair (Num 1) (cv_fst (cv_snd (cv_snd cv_v))))) ∧
cv$c2b
(cv_subspt (cv_fst (cv_snd cv_v)) (cv_spt_left cv_t)) ⇒
P (cv_snd (cv_snd (cv_snd cv_v))) (cv_spt_right cv_t)) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b
(cv_subspt (cv_fst (cv_snd cv_v)) (cv_spt_left cv_t)) ⇒
P (cv_snd (cv_snd cv_v)) (cv_spt_right cv_t)) ⇒
P cv_v cv_t) ⇒
∀v v1. P v v1
[cv_subspt_thm] Theorem
[oracles: DISK_THM] [axioms: ] [from_to f_a t_a]
⊢ b2c (subspt v t) =
cv_subspt (from_sptree_sptree_spt f_a v)
(from_sptree_sptree_spt f_a t)
[cv_toAList_foldi_def] Theorem
⊢ ∀cv_v cv_i cv_acc.
cv_toAList_foldi cv_i cv_acc cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 1) (cv_fst cv_v))
(cv_if (cv_lt (Num 2) (cv_fst cv_v))
(let
cv0 = cv_lrnext cv_i
in
cv_toAList_foldi (cv_add cv_i cv0)
(Pair (Pair cv_i (cv_fst (cv_snd (cv_snd cv_v))))
(cv_toAList_foldi
(cv_add cv_i (cv_mul (Num 2) cv0)) cv_acc
(cv_fst (cv_snd cv_v))))
(cv_snd (cv_snd (cv_snd cv_v))))
(let
cv0 = cv_lrnext cv_i
in
cv_toAList_foldi (cv_add cv_i cv0)
(cv_toAList_foldi (cv_add cv_i (cv_mul (Num 2) cv0))
cv_acc (cv_fst (cv_snd cv_v)))
(cv_snd (cv_snd cv_v))))
(Pair (Pair cv_i (cv_snd cv_v)) cv_acc)) cv_acc
[cv_toAList_foldi_ind] Theorem
⊢ ∀P. (∀cv_i cv_acc cv_v.
(∀cv0.
cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv0 = cv_lrnext cv_i ⇒
P (cv_add cv_i cv0)
(Pair (Pair cv_i (cv_fst (cv_snd (cv_snd cv_v))))
(cv_toAList_foldi (cv_add cv_i (cv_mul (Num 2) cv0))
cv_acc (cv_fst (cv_snd cv_v))))
(cv_snd (cv_snd (cv_snd cv_v)))) ∧
(∀cv0.
cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv0 = cv_lrnext cv_i ⇒
P (cv_add cv_i (cv_mul (Num 2) cv0)) cv_acc
(cv_fst (cv_snd cv_v))) ∧
(∀cv0.
cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv0 = cv_lrnext cv_i ⇒
P (cv_add cv_i cv0)
(cv_toAList_foldi (cv_add cv_i (cv_mul (Num 2) cv0))
cv_acc (cv_fst (cv_snd cv_v)))
(cv_snd (cv_snd cv_v))) ∧
(∀cv0.
cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv0 = cv_lrnext cv_i ⇒
P (cv_add cv_i (cv_mul (Num 2) cv0)) cv_acc
(cv_fst (cv_snd cv_v))) ⇒
P cv_i cv_acc cv_v) ⇒
∀v v1 v2. P v v1 v2
[cv_toAList_foldi_thm] Theorem
⊢ toAList_foldi_pre i acc v ⇒
from_list (from_pair Num f_a) (toAList_foldi i acc v) =
cv_toAList_foldi (Num i) (from_list (from_pair Num f_a) acc)
(from_sptree_sptree_spt f_a v)
[cv_toAList_thm] Theorem
⊢ from_list (from_pair Num f_a) (toAList x) =
cv_toAList (from_sptree_sptree_spt f_a x)
[cv_toListA_def] Theorem
⊢ ∀cv_v cv_acc.
cv_toListA cv_acc cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 1) (cv_fst cv_v))
(cv_if (cv_lt (Num 2) (cv_fst cv_v))
(cv_toListA
(Pair (cv_fst (cv_snd (cv_snd cv_v)))
(cv_toListA cv_acc (cv_snd (cv_snd (cv_snd cv_v)))))
(cv_fst (cv_snd cv_v)))
(cv_toListA (cv_toListA cv_acc (cv_snd (cv_snd cv_v)))
(cv_fst (cv_snd cv_v)))) (Pair (cv_snd cv_v) cv_acc))
cv_acc
[cv_toListA_ind] Theorem
⊢ ∀P. (∀cv_acc cv_v.
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ⇒
P cv_acc (cv_snd (cv_snd (cv_snd cv_v)))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ⇒
P
(Pair (cv_fst (cv_snd (cv_snd cv_v)))
(cv_toListA cv_acc (cv_snd (cv_snd (cv_snd cv_v)))))
(cv_fst (cv_snd cv_v))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ⇒
P cv_acc (cv_snd (cv_snd cv_v))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ⇒
P (cv_toListA cv_acc (cv_snd (cv_snd cv_v)))
(cv_fst (cv_snd cv_v))) ⇒
P cv_acc cv_v) ⇒
∀v v1. P v v1
[cv_toListA_thm] Theorem
⊢ from_list f_a (toListA acc v) =
cv_toListA (from_list f_a acc) (from_sptree_sptree_spt f_a v)
[cv_toList_thm] Theorem
⊢ from_list f_a (toList m) = cv_toList (from_sptree_sptree_spt f_a m)
[cv_union_def] Theorem
⊢ ∀cv_v cv_t.
cv_union cv_v cv_t =
cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 1) (cv_fst cv_v))
(cv_if (cv_lt (Num 2) (cv_fst cv_v))
(cv_if (cv_ispair cv_t)
(cv_if (cv_lt (Num 1) (cv_fst cv_t))
(cv_if (cv_lt (Num 2) (cv_fst cv_t))
(Pair (Num 3)
(Pair
(cv_union (cv_fst (cv_snd cv_v))
(cv_fst (cv_snd cv_t)))
(Pair (cv_fst (cv_snd (cv_snd cv_v)))
(cv_union
(cv_snd (cv_snd (cv_snd cv_v)))
(cv_snd (cv_snd (cv_snd cv_t)))))))
(Pair (Num 3)
(Pair
(cv_union (cv_fst (cv_snd cv_v))
(cv_fst (cv_snd cv_t)))
(Pair (cv_fst (cv_snd (cv_snd cv_v)))
(cv_union
(cv_snd (cv_snd (cv_snd cv_v)))
(cv_snd (cv_snd cv_t)))))))
(Pair (Num 3)
(Pair (cv_fst (cv_snd cv_v))
(Pair (cv_fst (cv_snd (cv_snd cv_v)))
(cv_snd (cv_snd (cv_snd cv_v)))))))
(Pair (Num 3)
(Pair (cv_fst (cv_snd cv_v))
(Pair (cv_fst (cv_snd (cv_snd cv_v)))
(cv_snd (cv_snd (cv_snd cv_v)))))))
(cv_if (cv_ispair cv_t)
(cv_if (cv_lt (Num 1) (cv_fst cv_t))
(cv_if (cv_lt (Num 2) (cv_fst cv_t))
(Pair (Num 3)
(Pair
(cv_union (cv_fst (cv_snd cv_v))
(cv_fst (cv_snd cv_t)))
(Pair (cv_fst (cv_snd (cv_snd cv_t)))
(cv_union (cv_snd (cv_snd cv_v))
(cv_snd (cv_snd (cv_snd cv_t)))))))
(Pair (Num 2)
(Pair
(cv_union (cv_fst (cv_snd cv_v))
(cv_fst (cv_snd cv_t)))
(cv_union (cv_snd (cv_snd cv_v))
(cv_snd (cv_snd cv_t))))))
(Pair (Num 3)
(Pair (cv_fst (cv_snd cv_v))
(Pair (cv_snd cv_t) (cv_snd (cv_snd cv_v))))))
(Pair (Num 2)
(Pair (cv_fst (cv_snd cv_v)) (cv_snd (cv_snd cv_v))))))
(cv_if (cv_ispair cv_t)
(cv_if (cv_lt (Num 1) (cv_fst cv_t))
(cv_if (cv_lt (Num 2) (cv_fst cv_t))
(Pair (Num 3)
(Pair (cv_fst (cv_snd cv_t))
(Pair (cv_snd cv_v)
(cv_snd (cv_snd (cv_snd cv_t))))))
(Pair (Num 3)
(Pair (cv_fst (cv_snd cv_t))
(Pair (cv_snd cv_v) (cv_snd (cv_snd cv_t))))))
(Pair (Num 1) (cv_snd cv_v)))
(Pair (Num 1) (cv_snd cv_v)))) cv_t
[cv_union_ind] Theorem
⊢ ∀P. (∀cv_v cv_t.
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_ispair cv_t) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_t)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_t)) ⇒
P (cv_fst (cv_snd cv_v)) (cv_fst (cv_snd cv_t))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_ispair cv_t) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_t)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_t)) ⇒
P (cv_snd (cv_snd (cv_snd cv_v)))
(cv_snd (cv_snd (cv_snd cv_t)))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_ispair cv_t) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_t)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_t)) ⇒
P (cv_fst (cv_snd cv_v)) (cv_fst (cv_snd cv_t))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_ispair cv_t) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_t)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_t)) ⇒
P (cv_snd (cv_snd (cv_snd cv_v))) (cv_snd (cv_snd cv_t))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_ispair cv_t) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_t)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_t)) ⇒
P (cv_fst (cv_snd cv_v)) (cv_fst (cv_snd cv_t))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_ispair cv_t) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_t)) ∧
cv$c2b (cv_lt (Num 2) (cv_fst cv_t)) ⇒
P (cv_snd (cv_snd cv_v)) (cv_snd (cv_snd (cv_snd cv_t)))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_ispair cv_t) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_t)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_t)) ⇒
P (cv_fst (cv_snd cv_v)) (cv_fst (cv_snd cv_t))) ∧
(cv$c2b (cv_ispair cv_v) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_v)) ∧
cv$c2b (cv_ispair cv_t) ∧
cv$c2b (cv_lt (Num 1) (cv_fst cv_t)) ∧
¬cv$c2b (cv_lt (Num 2) (cv_fst cv_t)) ⇒
P (cv_snd (cv_snd cv_v)) (cv_snd (cv_snd cv_t))) ⇒
P cv_v cv_t) ⇒
∀v v1. P v v1
[cv_union_thm] Theorem
⊢ from_sptree_sptree_spt f_a (union v t) =
cv_union (from_sptree_sptree_spt f_a v)
(from_sptree_sptree_spt f_a t)
[cv_v2n_custom_thm] Theorem
⊢ Num (v2n_custom acc v) = cv_v2n_custom (Num acc) (from_list b2c v)
[every_empty_snd] Theorem
⊢ ∀ys. EVERY ((λt. isEmpty t) ∘ SND) ys ⇔ every_empty_snd ys
[every_empty_snd_def] Theorem
⊢ (every_empty_snd [] ⇔ T) ∧
∀xs x n.
every_empty_snd ((n,x)::xs) ⇔
if isEmpty x then every_empty_snd xs else F
[every_empty_snd_ind] Theorem
⊢ ∀P. P [] ∧ (∀n x xs. (isEmpty x ⇒ P xs) ⇒ P ((n,x)::xs)) ⇒ ∀v. P v
[from_sptree_spt_def] Theorem
⊢ from_sptree_sptree_spt f0 LN = Num 0 ∧
from_sptree_sptree_spt f0 ⦕ 0 ↦ v0 ⦖ = Pair (Num 1) (f0 v0) ∧
from_sptree_sptree_spt f0 (BN v0 v1) =
Pair (Num 2)
(Pair (from_sptree_sptree_spt f0 v0)
(from_sptree_sptree_spt f0 v1)) ∧
from_sptree_sptree_spt f0 (BS v0 v1 v2) =
Pair (Num 3)
(Pair (from_sptree_sptree_spt f0 v0)
(Pair (f0 v1) (from_sptree_sptree_spt f0 v2)))
[from_sptree_to_sptree_spt_thm] Theorem
⊢ from_to f0 t0 ⇒
from_to (from_sptree_sptree_spt f0) (to_sptree_spt t0)
[from_to_fmap] Theorem
⊢ from_to f0 t0 ⇒ from_to (from_fmap f0) (to_fmap t0)
[genlist_compute] Theorem
⊢ (∀i f. genlist i f 0 = []) ∧
(∀i f n.
genlist i f (NUMERAL (BIT1 n)) =
f i::genlist (i + 1) f (NUMERAL (BIT1 n) − 1)) ∧
∀i f n.
genlist i f (NUMERAL (BIT2 n)) =
f i::genlist (i + 1) f (NUMERAL (BIT1 n))
[genlist_eq_GENLIST] Theorem
⊢ GENLIST = genlist 0
[map_spt_left_def] Theorem
⊢ map_spt_left [] = [] ∧
∀xs x i. map_spt_left ((i,x)::xs) = (i,spt_left x)::map_spt_left xs
[map_spt_left_ind] Theorem
⊢ ∀P. P [] ∧ (∀i x xs. P xs ⇒ P ((i,x)::xs)) ⇒ ∀v. P v
[map_spt_right_def] Theorem
⊢ map_spt_right [] = [] ∧
∀xs x i.
map_spt_right ((i,x)::xs) = (i,spt_right x)::map_spt_right xs
[map_spt_right_ind] Theorem
⊢ ∀P. P [] ∧ (∀i x xs. P xs ⇒ P ((i,x)::xs)) ⇒ ∀v. P v
[map_spt_right_left] Theorem
⊢ MAP (λ(i,t). (i,spt_right t)) ys = map_spt_right ys ∧
MAP (λ(i,t). (i,spt_left t)) ys = map_spt_left ys
[o_THM] Theorem
⊢ ∀f g x. (f ∘ g) x = f (g x)
[replicate_acc_def] Theorem
⊢ ∀x n acc.
replicate_acc n x acc =
if n = 0 then acc else replicate_acc (n − 1) x (x::acc)
[replicate_acc_ind] Theorem
⊢ ∀P. (∀n x acc. (n ≠ 0 ⇒ P (n − 1) x (x::acc)) ⇒ P n x acc) ⇒
∀v v1 v2. P v v1 v2
[spt_centers_pre_cases] Theorem
⊢ ∀a0 a1.
spt_centers_pre a0 a1 ⇔
∀v0 v1.
a1 = v0::v1 ⇒
∀v0' v1'.
v0 = (v0',v1') ⇒
∀v. v = spt_center v1' ⇒
(v = NONE ⇒ spt_centers_pre (a0 + v0') v1) ∧
∀v0''. v = SOME v0'' ⇒ spt_centers_pre (a0 + v0') v1
[spt_centers_pre_ind] Theorem
⊢ ∀spt_centers_pre'.
(∀i v.
(∀v0 v1.
v = v0::v1 ⇒
∀v0' v1'.
v0 = (v0',v1') ⇒
∀v. v = spt_center v1' ⇒
(v = NONE ⇒ spt_centers_pre' (i + v0') v1) ∧
∀v0''. v = SOME v0'' ⇒ spt_centers_pre' (i + v0') v1) ⇒
spt_centers_pre' i v) ⇒
∀a0 a1. spt_centers_pre a0 a1 ⇒ spt_centers_pre' a0 a1
[spt_centers_pre_rules] Theorem
⊢ ∀i v.
(∀v0 v1.
v = v0::v1 ⇒
∀v0' v1'.
v0 = (v0',v1') ⇒
∀v. v = spt_center v1' ⇒
(v = NONE ⇒ spt_centers_pre (i + v0') v1) ∧
∀v0''. v = SOME v0'' ⇒ spt_centers_pre (i + v0') v1) ⇒
spt_centers_pre i v
[spt_centers_pre_strongind] Theorem
⊢ ∀spt_centers_pre'.
(∀i v.
(∀v0 v1.
v = v0::v1 ⇒
∀v0' v1'.
v0 = (v0',v1') ⇒
∀v. v = spt_center v1' ⇒
(v = NONE ⇒
spt_centers_pre (i + v0') v1 ∧
spt_centers_pre' (i + v0') v1) ∧
∀v0''.
v = SOME v0'' ⇒
spt_centers_pre (i + v0') v1 ∧
spt_centers_pre' (i + v0') v1) ⇒
spt_centers_pre' i v) ⇒
∀a0 a1. spt_centers_pre a0 a1 ⇒ spt_centers_pre' a0 a1
[toAList_foldi_pre] Theorem
⊢ ∀a0 a1 a2. toAList_foldi_pre a0 a1 a2
[toAList_foldi_pre_cases] Theorem
⊢ ∀a0 a1 a2.
toAList_foldi_pre a0 a1 a2 ⇔
(∀v0 v1.
a2 = BN v0 v1 ⇒
∀v. v = sptree$lrnext a0 ⇒
toAList_foldi_pre (a0 + 2 * v) a1 v0 ∧
toAList_foldi_pre (a0 + v)
(toAList_foldi (a0 + 2 * v) a1 v0) v1) ∧
∀v0 v1 v2.
a2 = BS v0 v1 v2 ⇒
∀v. v = sptree$lrnext a0 ⇒
toAList_foldi_pre (a0 + 2 * v) a1 v0 ∧
toAList_foldi_pre (a0 + v)
((a0,v1)::toAList_foldi (a0 + 2 * v) a1 v0) v2
[toAList_foldi_pre_ind] Theorem
⊢ ∀toAList_foldi_pre'.
(∀i acc v.
(∀v0 v1.
v = BN v0 v1 ⇒
∀v. v = sptree$lrnext i ⇒
toAList_foldi_pre' (i + 2 * v) acc v0 ∧
toAList_foldi_pre' (i + v)
(toAList_foldi (i + 2 * v) acc v0) v1) ∧
(∀v0 v1 v2.
v = BS v0 v1 v2 ⇒
∀v. v = sptree$lrnext i ⇒
toAList_foldi_pre' (i + 2 * v) acc v0 ∧
toAList_foldi_pre' (i + v)
((i,v1)::toAList_foldi (i + 2 * v) acc v0) v2) ⇒
toAList_foldi_pre' i acc v) ⇒
∀a0 a1 a2.
toAList_foldi_pre a0 a1 a2 ⇒ toAList_foldi_pre' a0 a1 a2
[toAList_foldi_pre_rules] Theorem
⊢ ∀i acc v.
(∀v0 v1.
v = BN v0 v1 ⇒
∀v. v = sptree$lrnext i ⇒
toAList_foldi_pre (i + 2 * v) acc v0 ∧
toAList_foldi_pre (i + v)
(toAList_foldi (i + 2 * v) acc v0) v1) ∧
(∀v0 v1 v2.
v = BS v0 v1 v2 ⇒
∀v. v = sptree$lrnext i ⇒
toAList_foldi_pre (i + 2 * v) acc v0 ∧
toAList_foldi_pre (i + v)
((i,v1)::toAList_foldi (i + 2 * v) acc v0) v2) ⇒
toAList_foldi_pre i acc v
[toAList_foldi_pre_strongind] Theorem
⊢ ∀toAList_foldi_pre'.
(∀i acc v.
(∀v0 v1.
v = BN v0 v1 ⇒
∀v. v = sptree$lrnext i ⇒
toAList_foldi_pre (i + 2 * v) acc v0 ∧
toAList_foldi_pre' (i + 2 * v) acc v0 ∧
toAList_foldi_pre (i + v)
(toAList_foldi (i + 2 * v) acc v0) v1 ∧
toAList_foldi_pre' (i + v)
(toAList_foldi (i + 2 * v) acc v0) v1) ∧
(∀v0 v1 v2.
v = BS v0 v1 v2 ⇒
∀v. v = sptree$lrnext i ⇒
toAList_foldi_pre (i + 2 * v) acc v0 ∧
toAList_foldi_pre' (i + 2 * v) acc v0 ∧
toAList_foldi_pre (i + v)
((i,v1)::toAList_foldi (i + 2 * v) acc v0) v2 ∧
toAList_foldi_pre' (i + v)
((i,v1)::toAList_foldi (i + 2 * v) acc v0) v2) ⇒
toAList_foldi_pre' i acc v) ⇒
∀a0 a1 a2.
toAList_foldi_pre a0 a1 a2 ⇒ toAList_foldi_pre' a0 a1 a2
[to_sptree_spt_def] Theorem
⊢ to_sptree_spt t0 v =
if cv_has_shape [SOME 2; NONE] v then
BN (to_sptree_spt t0 (cv_fst (cv_snd v)))
(to_sptree_spt t0 (cv_snd (cv_snd v)))
else if cv_has_shape [SOME 3; NONE; NONE] v then
BS (to_sptree_spt t0 (cv_fst (cv_snd v)))
(t0 (cv_fst (cv_snd (cv_snd v))))
(to_sptree_spt t0 (cv_snd (cv_snd (cv_snd v))))
else if v = Num 0 then LN
else ⦕ 0 ↦ t0 (cv_snd v) ⦖
*)
end
HOL 4, Trindemossen-1