Definitions
FOLDL_lam_lam_pair_CASE_lam_la_def
⊢ ∀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
⊢ ∀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
⊢ ∀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
⊢ ∀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
⊢ ∀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
⊢ 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
⊢ ∀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
⊢ 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
⊢ ∀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
⊢ ∀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
⊢ ∀cv_v. cv_ISR cv_v = cv_if (cv_lt (Num 0) (cv_fst cv_v)) (Num 1) (Num 0)
cv_LAST_def
⊢ ∀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
⊢ ∀cv_L. cv_LENGTH cv_L = cv_LEN cv_L (Num 0)
cv_LEN_def
⊢ ∀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
⊢ ∀cv_v. cv_NULL cv_v = cv_if (cv_ispair cv_v) (Num 0) (Num 1)
cv_OUTL_def
⊢ ∀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
⊢ ∀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
⊢ ∀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
⊢ ∀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
⊢ ∀cv_n cv_c. cv_REPLICATE cv_n cv_c = cv_replicate_acc cv_n cv_c (Num 0)
cv_REVERSE_def
⊢ ∀cv_L. cv_REVERSE cv_L = cv_REV cv_L (Num 0)
cv_REV_def
⊢ ∀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
⊢ ∀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
⊢ ∀cv_L. cv_SUM cv_L = cv_SUM_ACC cv_L (Num 0)
cv_UNZIP_def_primitive
⊢ 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
⊢ 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_be_bytes_def
⊢ ∀cv_v0 cv_res cv_v.
cv_be_bytes cv_v0 cv_res cv_v =
(let
cv0 = Pair cv_v0 cv_v
in
cv_if (cv_ispair cv0)
(cv_if (cv_lt (Num 0) (cv_fst cv0))
(let
cv1 = cv_sub (cv_fst cv0) (Num 1)
in
cv_if (cv_ispair (cv_snd cv0))
(cv_be_bytes cv1 (Pair (cv_fst (cv_snd cv0)) cv_res)
(cv_snd (cv_snd cv0)))
(cv_be_bytes cv1 (Pair (Num 0) cv_res) (Num 0))) cv_res)
(Num 0))
cv_fromList_def
⊢ ∀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
⊢ ∀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_lcp_def
⊢ ∀cv_ls.
cv_lcp cv_ls =
cv_if (cv_ispair cv_ls)
(cv_if (cv_ispair (cv_snd cv_ls))
(cv_lcp
(Pair (cv_lcp2 (cv_fst cv_ls) (cv_fst (cv_snd cv_ls)))
(cv_snd (cv_snd cv_ls)))) (cv_fst cv_ls)) (Num 0)
cv_list_insert_def
⊢ ∀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
⊢ ∀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
⊢ 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
⊢ ∀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
⊢ 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
⊢ 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
⊢ 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
⊢ ∀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
⊢ ∀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
⊢ 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
⊢ 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_num_of_bytes_def_primitive
⊢ cv_num_of_bytes =
WFREC (@R. WF R ∧ ∀cv_v. cv$c2b (cv_ispair cv_v) ⇒ R (cv_snd cv_v) cv_v)
(λcv_num_of_bytes a.
I
(cv_if (cv_ispair a)
(cv_add (cv_fst a)
(cv_mul (Num 256) (cv_num_of_bytes (cv_snd a)))) (Num 0)))
cv_oEL_def
⊢ ∀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
⊢ ∀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
⊢ ∀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
⊢ (∀v0. cv_right_depth (Num v0) = 0) ∧
∀x y. cv_right_depth (Pair x y) = cv_right_depth y + 1
cv_size'_def_primitive
⊢ 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
⊢ ∀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
⊢ ∀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
⊢ ∀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
⊢ ∀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
⊢ ∀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
⊢ ∀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_toAList_def
⊢ ∀cv_x. cv_toAList cv_x = cv_toAList_foldi (Num 0) (Num 0) cv_x
cv_toList_def
⊢ ∀cv_m. cv_toList cv_m = cv_toListA (Num 0) cv_m
cv_toSortedAList_def
⊢ ∀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
⊢ ∀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
cv_word_of_bytes_be'_def
⊢ ∀cv_bs.
cv_word_of_bytes_be' cv_bs =
cv_mod (cv_num_of_bytes (cv_be_bytes (Num 8) (Num 0) cv_bs))
(Num 18446744073709551616)
cv_word_of_bytes_be_def
⊢ ∀cv_bs.
cv_word_of_bytes_be cv_bs =
cv_mod (cv_num_of_bytes (cv_be_bytes (Num 4) (Num 0) cv_bs))
(Num 4294967296)
cv_word_of_bytes_le'_def
⊢ ∀cv_bs.
cv_word_of_bytes_le' cv_bs =
cv_mod (cv_num_of_bytes cv_bs) (Num 18446744073709551616)
cv_word_of_bytes_le_def
⊢ ∀cv_bs.
cv_word_of_bytes_le cv_bs =
cv_mod (cv_num_of_bytes cv_bs) (Num 4294967296)
cv_word_to_bytes_be'_def
⊢ ∀cv_w.
cv_word_to_bytes_be' cv_w = cv_REVERSE (cv_bytes_of_num (Num 8) cv_w)
cv_word_to_bytes_be_def
⊢ ∀cv_w.
cv_word_to_bytes_be cv_w = cv_REVERSE (cv_bytes_of_num (Num 4) cv_w)
cv_word_to_bytes_le'_def
⊢ ∀cv_w. cv_word_to_bytes_le' cv_w = cv_bytes_of_num (Num 8) cv_w
cv_word_to_bytes_le_def
⊢ ∀cv_w. cv_word_to_bytes_le cv_w = cv_bytes_of_num (Num 4) cv_w
⊢ ∀f m.
from_fmap f m = from_sptree_sptree_spt f (fromAList (fmap_to_alist m))
⊢ ∀fs.
from_num_fset fs =
from_sptree_sptree_spt from_unit (list_to_num_set (fset_REP fs))
from_sptree_sptree_spt_def
⊢ (∀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)))
⊢ (∀i f. genlist i f 0 = []) ∧
∀i f n. genlist i f (SUC n) = f i::genlist (i + 1) f n
⊢ (∀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
⊢ (∀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 = foldi (λk v a. (k,v)::a)
⊢ ∀t m. to_fmap t m = alist_to_fmap (toAList (to_sptree_spt t m))
⊢ ∀cv. to_num_fset cv = fromSet (domain (to_sptree_spt to_unit cv))
to_sptree_spt_curried_def
⊢ ∀x x0. to_sptree_spt x x0 = to_sptree_spt_tupled (x,x0)
to_sptree_spt_tupled_primitive_def
⊢ to_sptree_spt_tupled =
WFREC
(@R. WF R ∧
(∀t0 v.
¬cv_has_shape [SOME 2; NONE] v ∧
cv_has_shape [SOME 3; NONE; NONE] v ⇒
R (t0,cv_fst (cv_snd v)) (t0,v)) ∧
(∀t0 v.
¬cv_has_shape [SOME 2; NONE] v ∧
cv_has_shape [SOME 3; NONE; NONE] v ⇒
R (t0,cv_snd (cv_snd (cv_snd v))) (t0,v)) ∧
(∀t0 v.
cv_has_shape [SOME 2; NONE] v ⇒ R (t0,cv_fst (cv_snd v)) (t0,v)) ∧
∀t0 v.
cv_has_shape [SOME 2; NONE] v ⇒ R (t0,cv_snd (cv_snd v)) (t0,v))
(λto_sptree_spt_tupled a.
case a of
(t0,v) =>
I
(if cv_has_shape [SOME 2; NONE] v then
BN (to_sptree_spt_tupled (t0,cv_fst (cv_snd v)))
(to_sptree_spt_tupled (t0,cv_snd (cv_snd v)))
else if cv_has_shape [SOME 3; NONE; NONE] v then
BS (to_sptree_spt_tupled (t0,cv_fst (cv_snd v)))
(t0 (cv_fst (cv_snd (cv_snd v))))
(to_sptree_spt_tupled (t0,cv_snd (cv_snd (cv_snd v))))
else if v = Num 0 then LN
else ⦕ 0 ↦ t0 (cv_snd v) ⦖))
Theorems
⊢ ∀n xs. EL_pre n xs ⇔ n < LENGTH xs
EL_pre_cases
⊢ ∀a0 a1.
EL_pre a0 a1 ⇔ (a0 = 0 ⇒ a1 ≠ []) ∧ ∀n. a0 = SUC n ⇒ EL_pre n (TL a1)
EL_pre_ind
⊢ ∀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
⊢ ∀v l. (v = 0 ⇒ l ≠ []) ∧ (∀n. v = SUC n ⇒ EL_pre n (TL l)) ⇒ EL_pre v l
EL_pre_strongind
⊢ ∀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
⊢ 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)
⊢ ∀xs. FRONT_pre xs ⇔ xs ≠ []
FRONT_pre_cases
⊢ ∀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
⊢ ∀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
⊢ ∀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
⊢ ∀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
⊢ ∀f ls. FUPDATE_LIST_pre f ls
FUPDATE_LIST_pre_cases
⊢ ∀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
⊢ ∀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
⊢ ∀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
⊢ ∀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_cases
⊢ ∀a0 a1.
INDEX_OF_pre a0 a1 ⇔ ∀v0 v1. a1 = v0::v1 ⇒ a0 ≠ v0 ⇒ INDEX_OF_pre a0 v1
INDEX_OF_pre_ind
⊢ ∀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
⊢ ∀x v.
(∀v0 v1. v = v0::v1 ⇒ x ≠ v0 ⇒ INDEX_OF_pre x v1) ⇒ INDEX_OF_pre x v
INDEX_OF_pre_strongind
⊢ ∀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
⊢ ∀xs. LAST_pre xs ⇔ xs ≠ []
LAST_pre_cases
⊢ ∀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
⊢ ∀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
⊢ ∀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
⊢ ∀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
OUTL_pre_cases
⊢ ∀a0. OUTL_pre a0 ⇔ (∃x. a0 = INL x) ∧ ∀v0. a0 ≠ INR v0
OUTL_pre_ind
⊢ ∀OUTL_pre'.
(∀v. (∃x. v = INL x) ∧ (∀v0. v ≠ INR v0) ⇒ OUTL_pre' v) ⇒
∀a0. OUTL_pre a0 ⇒ OUTL_pre' a0
OUTL_pre_rules
⊢ ∀v. (∃x. v = INL x) ∧ (∀v0. v ≠ INR v0) ⇒ OUTL_pre v
OUTL_pre_strongind
⊢ ∀OUTL_pre'.
(∀v. (∃x. v = INL x) ∧ (∀v0. v ≠ INR v0) ⇒ OUTL_pre' v) ⇒
∀a0. OUTL_pre a0 ⇒ OUTL_pre' a0
OUTR_pre_cases
⊢ ∀a0. OUTR_pre a0 ⇔ (∃x. a0 = INR x) ∧ ∀v0. a0 ≠ INL v0
OUTR_pre_ind
⊢ ∀OUTR_pre'.
(∀v. (∃x. v = INR x) ∧ (∀v0. v ≠ INL v0) ⇒ OUTR_pre' v) ⇒
∀a0. OUTR_pre a0 ⇒ OUTR_pre' a0
OUTR_pre_rules
⊢ ∀v. (∃x. v = INR x) ∧ (∀v0. v ≠ INL v0) ⇒ OUTR_pre v
OUTR_pre_strongind
⊢ ∀OUTR_pre'.
(∀v. (∃x. v = INR x) ∧ (∀v0. v ≠ INL v0) ⇒ OUTR_pre' v) ⇒
∀a0. OUTR_pre a0 ⇒ OUTR_pre' a0
⊢ REPLICATE n c = replicate_acc n c []
⊢ UNZIP ts =
case ts of
[] => ([],[])
| x::xs => (let (t1,t2) = UNZIP xs in (FST x::t1,SND x::t2))
⊢ ∀n k.
count_loop n k = if n = 0 then [] else k::count_loop (n − 1) (k + 1)
⊢ ∀P. (∀n k. (n ≠ 0 ⇒ P (n − 1) (k + 1)) ⇒ P n k) ⇒ ∀v v1. P v v1
cv_ALL_DISTINCT_thm
[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
[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
⊢ ∀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
⊢ ∀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
⊢ from_list f_a (v ⧺ l) = cv_APPEND (from_list f_a v) (from_list f_a l)
⊢ COUNT_LIST n = count_loop n 0
cv_DROP_thm
⊢ from_list f_a (DROP n v) = cv_DROP (Num n) (from_list f_a v)
cv_EL_thm
⊢ EL_pre v l ⇒ f_a l❲v❳ = cv_EL (Num v) (from_list f_a l)
cv_FLAT_def
⊢ ∀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
⊢ ∀P. (∀cv_v. (cv$c2b (cv_ispair cv_v) ⇒ P (cv_snd cv_v)) ⇒ P cv_v) ⇒
∀v. P v
cv_FLAT_thm
⊢ from_list f_a (FLAT v) = cv_FLAT (from_list (from_list f_a) v)
cv_FOLDL_lam_lam_pair_CASE_lam_la_thm
⊢ 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
⊢ ∀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
⊢ ∀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
⊢ FRONT_pre v ⇒ from_list f_a (FRONT v) = cv_FRONT (from_list f_a v)
⊢ f_a (FST v) = cv_fst (from_pair f_a f_b v)
cv_FUPDATE_LIST_thm
⊢ 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)
⊢ v ≠ [] ⇒ f_a (HD v) = cv_fst (from_list f_a v)
cv_INDEX_OF_def
⊢ ∀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
⊢ ∀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
[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
⊢ b2c (ISL v) = cv_ISL (from_sum f_a f_b v)
cv_ISR_thm
⊢ b2c (ISR v) = cv_ISR (from_sum f_a f_b v)
⊢ b2c (IS_NONE v) = cv_sub (Num 1) (cv_ispair (from_option f_a v))
⊢ b2c (IS_SOME v) = cv_ispair (from_option f_a v)
cv_LAST_thm
⊢ LAST_pre v ⇒ f_a (LAST v) = cv_LAST (from_list f_a v)
cv_LENGTH_thm
⊢ Num (LENGTH L) = cv_LENGTH (from_list f_a L)
cv_LEN_thm
⊢ Num (LEN v n) = cv_LEN (from_list f_a v) (Num n)
cv_LUPDATE_def
⊢ ∀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
⊢ ∀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
⊢ from_list f_a v❲n ↦ e❳ = cv_LUPDATE (f_a e) (Num n) (from_list f_a v)
⊢ from_list a (MAP FST l) = cv_map_fst (from_list (from_pair a b) l)
⊢ from_list b (MAP SND l) = cv_map_snd (from_list (from_pair a b) l)
cv_NULL_thm
⊢ b2c (NULL v) = cv_NULL (from_list f_a v)
cv_OUTL_thm
⊢ OUTL_pre v ⇒ f_a (OUTL v) = cv_OUTL (from_sum f_a f_b v)
cv_OUTR_thm
⊢ OUTR_pre v ⇒ f_b (OUTR v) = cv_OUTR (from_sum f_a f_b v)
cv_PAD_LEFT_thm
⊢ 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
⊢ 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
⊢ from_list f_a (REPLICATE n c) = cv_REPLICATE (Num n) (f_a c)
cv_REVERSE_thm
⊢ from_list f_a (REVERSE L) = cv_REVERSE (from_list f_a L)
cv_REV_thm
⊢ from_list f_a (REV v acc) = cv_REV (from_list f_a v) (from_list f_a acc)
⊢ f_b (SND v) = cv_snd (from_pair f_a f_b v)
cv_SNOC_def
⊢ ∀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
⊢ ∀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
⊢ from_list f_a (SNOC x v) = cv_SNOC (f_a x) (from_list f_a v)
cv_SUM_ACC_thm
⊢ Num (SUM_ACC v acc) = cv_SUM_ACC (from_list Num v) (Num acc)
cv_SUM_thm
⊢ Num (SUM L) = cv_SUM (from_list Num L)
cv_TAKE_def
⊢ ∀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
⊢ ∀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
⊢ from_list f_a (TAKE n v) = cv_TAKE (Num n) (from_list f_a v)
⊢ v ≠ NONE ⇒ f_a (THE v) = cv_snd (from_option f_a v)
⊢ from_list f_a (TL v) = cv_snd (from_list f_a v)
cv_UNZIP_def
⊢ ∀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
⊢ ∀P. (∀cv_ts. (cv$c2b (cv_ispair cv_ts) ⇒ P (cv_snd cv_ts)) ⇒ P cv_ts) ⇒
∀v. P v
cv_UNZIP_thm
⊢ 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
⊢ ∀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
⊢ ∀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
⊢ 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
⊢ ∀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
⊢ ∀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
⊢ 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_be_bytes_thm
⊢ from_list from_word (be_bytes v0 res v) =
cv_be_bytes (Num v0) (from_list from_word res) (from_list from_word v)
cv_bytes_of_num_def
⊢ ∀cv_v cv_n.
cv_bytes_of_num cv_v cv_n =
cv_if (cv_lt (Num 0) cv_v)
(let
cv0 = cv_sub cv_v (Num 1)
in
Pair (cv_mod cv_n (Num 256))
(cv_bytes_of_num cv0 (cv_div cv_n (Num 256)))) (Num 0)
cv_bytes_of_num_ind
⊢ ∀P. (∀cv_v cv_n.
(∀cv0.
cv$c2b (cv_lt (Num 0) cv_v) ∧ cv0 = cv_sub cv_v (Num 1) ⇒
P cv0 (cv_div cv_n (Num 256))) ⇒
P cv_v cv_n) ⇒
∀v v1. P v v1
cv_bytes_of_num_thm
⊢ from_list from_word (bytes_of_num v n) = cv_bytes_of_num (Num v) (Num n)
cv_count_loop_def
⊢ ∀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
⊢ ∀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
⊢ from_list Num (count_loop n k) = cv_count_loop (Num n) (Num k)
cv_delete_def
⊢ ∀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
⊢ ∀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
⊢ from_sptree_sptree_spt f_a (delete k v) =
cv_delete (Num k) (from_sptree_sptree_spt f_a v)
cv_difference_def
⊢ ∀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
⊢ ∀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
⊢ 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
⊢ ∀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
⊢ ∀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
[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
⊢ from_sptree_sptree_spt f_a (fromList l) = cv_fromList (from_list f_a l)
cv_insert_def
⊢ ∀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
⊢ ∀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
⊢ 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
⊢ ∀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
⊢ ∀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
⊢ 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
[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_lcp2_def
⊢ ∀cv_ys cv_xs.
cv_lcp2 cv_xs cv_ys =
cv_if (cv_ispair cv_xs)
(cv_if (cv_ispair cv_ys)
(cv_if (cv_eq (cv_fst cv_xs) (cv_fst cv_ys))
(Pair (cv_fst cv_xs) (cv_lcp2 (cv_snd cv_xs) (cv_snd cv_ys)))
(Num 0)) (Num 0)) (Num 0)
cv_lcp2_ind
⊢ ∀P. (∀cv_xs cv_ys.
(cv$c2b (cv_ispair cv_xs) ∧ cv$c2b (cv_ispair cv_ys) ∧
cv$c2b (cv_eq (cv_fst cv_xs) (cv_fst cv_ys)) ⇒
P (cv_snd cv_xs) (cv_snd cv_ys)) ⇒
P cv_xs cv_ys) ⇒
∀v v1. P v v1
cv_lcp2_thm
[oracles: DISK_THM] [axioms: ] [from_to f_a t_a]
⊢ lcp2_pre xs ys ⇒
from_list f_a (lcp2 xs ys) =
cv_lcp2 (from_list f_a xs) (from_list f_a ys)
cv_lcp_thm
[oracles: DISK_THM] [axioms: ] [from_to f_a t_a]
⊢ lcp_pre ls ⇒
from_list f_a (lcp ls) = cv_lcp (from_list (from_list f_a) ls)
cv_list_insert_thm
⊢ 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
[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
⊢ ∀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
⊢ ∀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
⊢ from_sptree_sptree_spt from_unit (list_to_num_set v) =
cv_list_to_num_set (from_list Num v)
cv_lookup_thm
⊢ from_option f_a (lookup k v) =
cv_lookup (Num k) (from_sptree_sptree_spt f_a v)
cv_lrnext_def
⊢ ∀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
⊢ ∀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
⊢ Num (sptree$lrnext n) = cv_lrnext (Num n)
⊢ ∀cv.
cv_map_fst cv =
cv_if (cv_ispair cv)
(Pair (cv_fst (cv_fst cv)) (cv_map_fst (cv_snd cv))) (Num 0)
⊢ ∀P. (∀cv. (cv$c2b (cv_ispair cv) ⇒ P (cv_snd cv)) ⇒ P cv) ⇒ ∀v. P v
⊢ ∀cv.
cv_map_snd cv =
cv_if (cv_ispair cv)
(Pair (cv_snd (cv_fst cv)) (cv_map_snd (cv_snd cv))) (Num 0)
⊢ ∀P. (∀cv. (cv$c2b (cv_ispair cv) ⇒ P (cv_snd cv)) ⇒ P cv) ⇒ ∀v. P v
cv_mk_BN_thm
⊢ 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
⊢ 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
⊢ ∀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
⊢ ∀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
⊢ from_sptree_sptree_spt f_a (mk_wf v) =
cv_mk_wf (from_sptree_sptree_spt f_a v)
cv_nub_def
⊢ ∀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
⊢ ∀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
[oracles: DISK_THM] [axioms: ] [from_to f_a t_a]
⊢ from_list f_a (nub v) = cv_nub (from_list f_a v)
cv_num_of_bytes_def
⊢ ∀cv_v.
cv_num_of_bytes cv_v =
cv_if (cv_ispair cv_v)
(cv_add (cv_fst cv_v)
(cv_mul (Num 256) (cv_num_of_bytes (cv_snd cv_v)))) (Num 0)
cv_num_of_bytes_ind
⊢ ∀P. (∀cv_v. (cv$c2b (cv_ispair cv_v) ⇒ P (cv_snd cv_v)) ⇒ P cv_v) ⇒
∀v. P v
cv_num_of_bytes_thm
⊢ Num (num_of_bytes v) = cv_num_of_bytes (from_list from_word v)
cv_oEL_thm
⊢ from_option f_a (oEL n v) = cv_oEL (Num n) (from_list f_a v)
cv_oHD_thm
⊢ from_option f_a (oHD l) = cv_oHD (from_list f_a l)
⊢ from_fmap f (m \\ k) = cv_delete (Num k) (from_fmap f m)
⊢ from_fmap f FEMPTY = Num 0
⊢ from_option f (FLOOKUP m n) = cv_lookup (Num n) (from_fmap f m)
⊢ from_fmap f (m1 ⊌ m2) = cv_union (from_fmap f m1) (from_fmap f m2)
⊢ from_fmap f m⟨k ↦ v⟩ = cv_insert (Num k) (f v) (from_fmap f m)
⊢ 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
⊢ (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
⊢ (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
⊢ (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
⊢ (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
⊢ (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
⊢ (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
⊢ 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 m) = Num 0
⊢ cv_size' (cv_mk_BN x y) = cv_add (cv_size' x) (cv_size' y)
⊢ cv_size' (cv_mk_BS x y z) =
cv_add (cv_add (cv_size' x) (cv_size' z)) (Num 1)
cv_size'_def
⊢ ∀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
⊢ ∀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
⊢ Num (size v) = cv_size' (from_sptree_sptree_spt f_a v)
cv_spt_center_thm
⊢ from_option f_a (spt_center v) =
cv_spt_center (from_sptree_sptree_spt f_a v)
cv_spt_left_thm
⊢ from_sptree_sptree_spt f_a (spt_left v) =
cv_spt_left (from_sptree_sptree_spt f_a v)
cv_spt_right_thm
⊢ 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
⊢ 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
[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
[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
⊢ ∀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
⊢ ∀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
[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
⊢ ∀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
⊢ ∀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
⊢ 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
⊢ from_list (from_pair Num f_a) (toAList x) =
cv_toAList (from_sptree_sptree_spt f_a x)
cv_toListA_def
⊢ ∀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
⊢ ∀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
⊢ from_list f_a (toListA acc v) =
cv_toListA (from_list f_a acc) (from_sptree_sptree_spt f_a v)
cv_toList_thm
⊢ from_list f_a (toList m) = cv_toList (from_sptree_sptree_spt f_a m)
cv_toSortedAList_thm
[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
⊢ ∀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
⊢ ∀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
⊢ 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
⊢ Num (v2n_custom acc v) = cv_v2n_custom (Num acc) (from_list b2c v)
cv_word_of_bytes_be'_thm
⊢ from_word (word_of_bytes_be bs) =
cv_word_of_bytes_be' (from_list from_word bs)
cv_word_of_bytes_be_thm
⊢ from_word (word_of_bytes_be bs) =
cv_word_of_bytes_be (from_list from_word bs)
cv_word_of_bytes_le'_thm
⊢ from_word (word_of_bytes_le bs) =
cv_word_of_bytes_le' (from_list from_word bs)
cv_word_of_bytes_le_thm
⊢ from_word (word_of_bytes_le bs) =
cv_word_of_bytes_le (from_list from_word bs)
cv_word_to_bytes_be'_thm
⊢ from_list from_word (word_to_bytes_be w) =
cv_word_to_bytes_be' (from_word w)
cv_word_to_bytes_be_thm
⊢ from_list from_word (word_to_bytes_be w) =
cv_word_to_bytes_be (from_word w)
cv_word_to_bytes_le'_thm
⊢ from_list from_word (word_to_bytes_le w) =
cv_word_to_bytes_le' (from_word w)
cv_word_to_bytes_le_thm
⊢ from_list from_word (word_to_bytes_le w) =
cv_word_to_bytes_le (from_word w)
⊢ from_num_fset fEMPTY = Num 0
⊢ from_num_fset (fINSERT e s) = cv_insert (Num e) (Num 0) (from_num_fset s)
⊢ b2c (fIN e s) = cv_ispair (cv_lookup (Num e) (from_num_fset s))
⊢ from_num_fset (fUNION s1 s2) =
cv_union (from_num_fset s1) (from_num_fset s2)
from_sptree_spt_def
⊢ 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
⊢ from_to f0 t0 ⇒ from_to (from_sptree_sptree_spt f0) (to_sptree_spt t0)
⊢ from_to f0 t0 ⇒ from_to (from_fmap f0) (to_fmap t0)
⊢ from_to from_num_fset to_num_fset
⊢ from_num_fset (fset_ABS l) = cv_list_to_num_set (from_list Num l)
genlist_compute
⊢ (∀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))
lcp2_pre_cases
⊢ ∀a0 a1.
lcp2_pre a0 a1 ⇔
∀v0 v1.
a0 = v0::v1 ⇒ ∀v0' v1'. a1 = v0'::v1' ⇒ v0 = v0' ⇒ lcp2_pre v1 v1'
lcp2_pre_ind
⊢ ∀lcp2_pre'.
(∀xs ys.
(∀v0 v1.
xs = v0::v1 ⇒
∀v0' v1'. ys = v0'::v1' ⇒ v0 = v0' ⇒ lcp2_pre' v1 v1') ⇒
lcp2_pre' xs ys) ⇒
∀a0 a1. lcp2_pre a0 a1 ⇒ lcp2_pre' a0 a1
lcp2_pre_rules
⊢ ∀xs ys.
(∀v0 v1.
xs = v0::v1 ⇒ ∀v0' v1'. ys = v0'::v1' ⇒ v0 = v0' ⇒ lcp2_pre v1 v1') ⇒
lcp2_pre xs ys
lcp2_pre_strongind
⊢ ∀lcp2_pre'.
(∀xs ys.
(∀v0 v1.
xs = v0::v1 ⇒
∀v0' v1'.
ys = v0'::v1' ⇒ v0 = v0' ⇒ lcp2_pre v1 v1' ∧ lcp2_pre' v1 v1') ⇒
lcp2_pre' xs ys) ⇒
∀a0 a1. lcp2_pre a0 a1 ⇒ lcp2_pre' a0 a1
lcp_pre_cases
⊢ ∀a0.
lcp_pre a0 ⇔
∀v0 v1.
a0 = v0::v1 ⇒ ∀v0' v1'. v1 = v0'::v1' ⇒ lcp_pre (lcp2 v0 v0'::v1')
lcp_pre_ind
⊢ ∀lcp_pre'.
(∀ls.
(∀v0 v1.
ls = v0::v1 ⇒
∀v0' v1'. v1 = v0'::v1' ⇒ lcp_pre' (lcp2 v0 v0'::v1')) ⇒
lcp_pre' ls) ⇒
∀a0. lcp_pre a0 ⇒ lcp_pre' a0
lcp_pre_rules
⊢ ∀ls.
(∀v0 v1.
ls = v0::v1 ⇒ ∀v0' v1'. v1 = v0'::v1' ⇒ lcp_pre (lcp2 v0 v0'::v1')) ⇒
lcp_pre ls
lcp_pre_strongind
⊢ ∀lcp_pre'.
(∀ls.
(∀v0 v1.
ls = v0::v1 ⇒
∀v0' v1'.
v1 = v0'::v1' ⇒
lcp_pre (lcp2 v0 v0'::v1') ∧ lcp_pre' (lcp2 v0 v0'::v1')) ⇒
lcp_pre' ls) ⇒
∀a0. lcp_pre a0 ⇒ lcp_pre' a0
⊢ ∀f g x. (f ∘ g) x = f (g x)
⊢ ∀x n acc.
replicate_acc n x acc =
if n = 0 then acc else replicate_acc (n − 1) x (x::acc)
⊢ ∀P. (∀n x acc. (n ≠ 0 ⇒ P (n − 1) x (x::acc)) ⇒ P n x acc) ⇒
∀v v1 v2. P v v1 v2
⊢ ∀a0 a1 a2. toAList_foldi_pre a0 a1 a2
toAList_foldi_pre_cases
⊢ ∀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
⊢ ∀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
⊢ ∀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
⊢ ∀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
⊢ 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) ⦖
⊢ 8 ≤ dimindex (:α) ∧ divides 8 (dimindex (:α)) ⇒
word_of_bytes_be bs =
n2w (num_of_bytes (be_bytes (dimindex (:α) DIV 8) [] bs))
⊢ 8 ≤ dimindex (:α) ∧ divides 8 (dimindex (:α)) ⇒
word_of_bytes_le bs = n2w (num_of_bytes bs)
⊢ word_to_bytes_be w = REVERSE (bytes_of_num (dimindex (:α) DIV 8) (w2n w))
⊢ word_to_bytes_le w = bytes_of_num (dimindex (:α) DIV 8) (w2n w)