Structure cv_stdTheory
signature cv_stdTheory =
sig
type thm = Thm.thm
(* Definitions *)
val FOLDL_lam_lam_pair_CASE_lam_la_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_FUPDATE_LIST_def : 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_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_spts_to_alist_add_pause_def : thm
val cv_spts_to_alist_aux_def : thm
val cv_spts_to_alist_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_toSortedAList_def : thm
val cv_v2n_custom_def : thm
val from_fmap_def : thm
val from_num_fset_def : thm
val from_sptree_sptree_spt_def : thm
val genlist_def : thm
val list_mapi_def : thm
val list_mem_def : thm
val toAList_foldi_def : thm
val to_fmap_def : thm
val to_num_fset_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 FUPDATE_LIST_pre : thm
val FUPDATE_LIST_pre_cases : thm
val FUPDATE_LIST_pre_ind : thm
val FUPDATE_LIST_pre_rules : thm
val FUPDATE_LIST_pre_strongind : thm
val INDEX_OF_pre : 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 count_loop_def : thm
val count_loop_ind : 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_COUNT_LIST : 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_FUPDATE_LIST_thm : 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_count_loop_def : thm
val cv_count_loop_ind : thm
val cv_count_loop_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_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_DOMSUB : 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'_Num : thm
val cv_size'_cv_mk_BN : thm
val cv_size'_cv_mk_BS : 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_left_thm : thm
val cv_spt_right_thm : thm
val cv_spts_to_alist_add_pause_thm : thm
val cv_spts_to_alist_aux_thm : thm
val cv_spts_to_alist_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_toSortedAList_thm : thm
val cv_union_def : thm
val cv_union_ind : thm
val cv_union_thm : thm
val cv_v2n_custom_thm : thm
val fEMPTY_num_cv_rep : thm
val fINSERT_num_cv_rep : thm
val fIN_num_cv_rep : thm
val fUNION_num_cv_rep : thm
val from_sptree_spt_def : thm
val from_sptree_to_sptree_spt_thm : thm
val from_to_fmap : thm
val from_to_num_fset : thm
val fset_ABS_num_cv_rep : thm
val genlist_compute : thm
val genlist_eq_GENLIST : thm
val o_THM : thm
val replicate_acc_def : thm
val replicate_acc_ind : 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
(*
[cv_prim] Parent theory of "cv_std"
[finite_set] 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
[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_FUPDATE_LIST_def] Definition
⊢ ∀cv_f cv_v.
cv_FUPDATE_LIST cv_f cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_ispair (cv_fst cv_v))
(cv_FUPDATE_LIST
(cv_insert (cv_fst (cv_fst cv_v)) (cv_snd (cv_fst cv_v))
cv_f) (cv_snd cv_v)) (Num 0)) cv_f
[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_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_spts_to_alist_add_pause_def] Definition
⊢ ∀cv_j cv_q.
cv_spts_to_alist_add_pause cv_j cv_q =
cv_if (cv_ispair cv_q)
(cv_if (cv_ispair (cv_fst cv_q))
(Pair
(Pair (cv_add (cv_fst (cv_fst cv_q)) cv_j)
(cv_snd (cv_fst cv_q))) (cv_snd cv_q)) (Num 0))
(Pair (Pair cv_j (Num 0)) (Num 0))
[cv_spts_to_alist_aux_def] Definition
⊢ ∀cv_i cv_xs cv_acc_cent cv_acc_right cv_acc_left cv_repeat.
cv_spts_to_alist_aux cv_i cv_xs cv_acc_cent cv_acc_right
cv_acc_left cv_repeat =
cv_if (cv_ispair cv_xs)
(cv_if (cv_ispair (cv_fst cv_xs))
(cv_if (cv_eq (cv_snd (cv_fst cv_xs)) (Num 0))
(cv_spts_to_alist_aux
(cv_add cv_i (cv_fst (cv_fst cv_xs))) (cv_snd cv_xs)
cv_acc_cent
(cv_spts_to_alist_add_pause (cv_fst (cv_fst cv_xs))
cv_acc_right)
(cv_spts_to_alist_add_pause (cv_fst (cv_fst cv_xs))
cv_acc_left) cv_repeat)
(cv_spts_to_alist_aux
(cv_add cv_i (cv_fst (cv_fst cv_xs))) (cv_snd cv_xs)
(cv_APPEND
(let
cv0 = cv_spt_center (cv_snd (cv_fst cv_xs))
in
cv_if (cv_ispair cv0)
(Pair (Pair cv_i (cv_snd cv0)) (Num 0))
(Num 0)) cv_acc_cent)
(Pair
(Pair (cv_fst (cv_fst cv_xs))
(cv_spt_right (cv_snd (cv_fst cv_xs))))
cv_acc_right)
(Pair
(Pair (cv_fst (cv_fst cv_xs))
(cv_spt_left (cv_snd (cv_fst cv_xs))))
cv_acc_left) (Num 1))) (Num 0))
(Pair cv_i
(Pair
(cv_APPEND (cv_REVERSE cv_acc_right)
(cv_REVERSE cv_acc_left)) (Pair cv_acc_cent cv_repeat)))
[cv_spts_to_alist_def] Definition
⊢ ∀cv_i cv_xs cv_acc_cent.
cv_spts_to_alist cv_i cv_xs cv_acc_cent =
(let
cv0 =
cv_spts_to_alist_aux cv_i cv_xs cv_acc_cent (Num 0) (Num 0)
(Num 0)
in
cv_if (cv_ispair cv0)
(cv_if (cv_ispair (cv_snd cv0))
(cv_if (cv_ispair (cv_snd (cv_snd cv0)))
(cv_if (cv_snd (cv_snd (cv_snd cv0)))
(cv_spts_to_alist (cv_fst cv0)
(cv_fst (cv_snd cv0))
(cv_fst (cv_snd (cv_snd cv0))))
(cv_REVERSE (cv_fst (cv_snd (cv_snd cv0)))))
(Num 0)) (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_toSortedAList_def] Definition
⊢ ∀cv_spt.
cv_toSortedAList cv_spt =
cv_spts_to_alist (Num 0) (Pair (Pair (Num 1) cv_spt) (Num 0))
(Num 0)
[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
[from_fmap_def] Definition
⊢ ∀f m.
from_fmap f m =
from_sptree_sptree_spt f (fromAList (fmap_to_alist m))
[from_num_fset_def] Definition
⊢ ∀fs.
from_num_fset fs =
from_sptree_sptree_spt from_unit (list_to_num_set (fset_REP fs))
[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
[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))
[to_num_fset_def] Definition
⊢ ∀cv. to_num_fset cv = fromSet (domain (to_sptree_spt to_unit cv))
[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
[FUPDATE_LIST_pre] Theorem
⊢ ∀f ls. FUPDATE_LIST_pre f ls
[FUPDATE_LIST_pre_cases] Theorem
⊢ ∀a0 a1.
FUPDATE_LIST_pre a0 a1 ⇔
∀v0 v1.
a1 = v0::v1 ⇒
∀v0' v1'.
v0 = (v0',v1') ⇒ FUPDATE_LIST_pre (a0 |+ (v0',v1')) v1
[FUPDATE_LIST_pre_ind] Theorem
⊢ ∀FUPDATE_LIST_pre'.
(∀f v.
(∀v0 v1.
v = v0::v1 ⇒
∀v0' v1'.
v0 = (v0',v1') ⇒ FUPDATE_LIST_pre' (f |+ (v0',v1')) v1) ⇒
FUPDATE_LIST_pre' f v) ⇒
∀a0 a1. FUPDATE_LIST_pre a0 a1 ⇒ FUPDATE_LIST_pre' a0 a1
[FUPDATE_LIST_pre_rules] Theorem
⊢ ∀f v.
(∀v0 v1.
v = v0::v1 ⇒
∀v0' v1'.
v0 = (v0',v1') ⇒ FUPDATE_LIST_pre (f |+ (v0',v1')) v1) ⇒
FUPDATE_LIST_pre f v
[FUPDATE_LIST_pre_strongind] Theorem
⊢ ∀FUPDATE_LIST_pre'.
(∀f v.
(∀v0 v1.
v = v0::v1 ⇒
∀v0' v1'.
v0 = (v0',v1') ⇒
FUPDATE_LIST_pre (f |+ (v0',v1')) v1 ∧
FUPDATE_LIST_pre' (f |+ (v0',v1')) v1) ⇒
FUPDATE_LIST_pre' f v) ⇒
∀a0 a1. FUPDATE_LIST_pre a0 a1 ⇒ FUPDATE_LIST_pre' a0 a1
[INDEX_OF_pre] Theorem
⊢ ∀x y. INDEX_OF_pre x y
[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))
[count_loop_def] Theorem
⊢ ∀n k.
count_loop n k =
if n = 0 then [] else k::count_loop (n − 1) (k + 1)
[count_loop_ind] Theorem
⊢ ∀P. (∀n k. (n ≠ 0 ⇒ P (n − 1) (k + 1)) ⇒ P n k) ⇒ ∀v v1. P v v1
[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_COUNT_LIST] Theorem
⊢ COUNT_LIST n = count_loop n 0
[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_FUPDATE_LIST_thm] Theorem
⊢ FUPDATE_LIST_pre f v ⇒
from_fmap f_b (f |++ v) =
cv_FUPDATE_LIST (from_fmap f_b f) (from_list (from_pair Num 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_count_loop_def] Theorem
⊢ ∀cv_n cv_k.
cv_count_loop cv_n cv_k =
cv_if (cv_lt (Num 0) cv_n)
(Pair cv_k
(cv_count_loop (cv_sub cv_n (Num 1)) (cv_add cv_k (Num 1))))
(Num 0)
[cv_count_loop_ind] Theorem
⊢ ∀P. (∀cv_n cv_k.
(cv$c2b (cv_lt (Num 0) cv_n) ⇒
P (cv_sub cv_n (Num 1)) (cv_add cv_k (Num 1))) ⇒
P cv_n cv_k) ⇒
∀v v1. P v v1
[cv_count_loop_thm] Theorem
⊢ from_list Num (count_loop n k) = cv_count_loop (Num n) (Num k)
[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_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_DOMSUB] Theorem
⊢ from_fmap f (m \\ k) = cv_delete (Num k) (from_fmap f m)
[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_a f_b) x ∧
(∀v0 v1.
cv_rep ($var$(,_pre) v0 v1) ($var$(,_cv) (f_a v0) (f_b v1)) f_c
(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_c (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'_Num] Theorem
⊢ cv_size' (Num m) = Num 0
[cv_size'_cv_mk_BN] Theorem
⊢ cv_size' (cv_mk_BN x y) = cv_add (cv_size' x) (cv_size' y)
[cv_size'_cv_mk_BS] Theorem
⊢ cv_size' (cv_mk_BS x y z) =
cv_add (cv_add (cv_size' x) (cv_size' z)) (Num 1)
[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_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_spts_to_alist_add_pause_thm] Theorem
⊢ from_list (from_pair Num (from_sptree_sptree_spt f_a))
(spts_to_alist_add_pause j q) =
cv_spts_to_alist_add_pause (Num j)
(from_list (from_pair Num (from_sptree_sptree_spt f_a)) q)
[cv_spts_to_alist_aux_thm] Theorem
[oracles: DISK_THM] [axioms: ] [from_to f_a t_a]
⊢ from_pair Num
(from_pair
(from_list (from_pair Num (from_sptree_sptree_spt f_a)))
(from_pair (from_list (from_pair Num f_a)) b2c))
(spts_to_alist_aux i xs acc_cent acc_right acc_left repeat) =
cv_spts_to_alist_aux (Num i)
(from_list (from_pair Num (from_sptree_sptree_spt f_a)) xs)
(from_list (from_pair Num f_a) acc_cent)
(from_list (from_pair Num (from_sptree_sptree_spt f_a)) acc_right)
(from_list (from_pair Num (from_sptree_sptree_spt f_a)) acc_left)
(b2c repeat)
[cv_spts_to_alist_thm] Theorem
[oracles: DISK_THM] [axioms: ] [from_to f_a t_a]
⊢ from_list (from_pair Num f_a) (spts_to_alist i xs acc_cent) =
cv_spts_to_alist (Num i)
(from_list (from_pair Num (from_sptree_sptree_spt f_a)) xs)
(from_list (from_pair Num f_a) acc_cent)
[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_toSortedAList_thm] Theorem
[oracles: DISK_THM] [axioms: ] [from_to f_a t_a]
⊢ from_list (from_pair Num f_a) (toSortedAList spt) =
cv_toSortedAList (from_sptree_sptree_spt f_a spt)
[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)
[fEMPTY_num_cv_rep] Theorem
⊢ from_num_fset fEMPTY = Num 0
[fINSERT_num_cv_rep] Theorem
⊢ from_num_fset (fINSERT e s) =
cv_insert (Num e) (Num 0) (from_num_fset s)
[fIN_num_cv_rep] Theorem
⊢ b2c (fIN e s) = cv_ispair (cv_lookup (Num e) (from_num_fset s))
[fUNION_num_cv_rep] Theorem
⊢ from_num_fset (fUNION s1 s2) =
cv_union (from_num_fset s1) (from_num_fset s2)
[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)
[from_to_num_fset] Theorem
⊢ from_to from_num_fset to_num_fset
[fset_ABS_num_cv_rep] Theorem
⊢ from_num_fset (fset_ABS l) = cv_list_to_num_set (from_list Num l)
[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
[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
[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-2