Definitions
cv_finite_map_FUPDATE_LIST_def
⊢ ∀cv_f cv_v.
cv_finite_map_FUPDATE_LIST cv_f cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_ispair (cv_fst cv_v))
(cv_finite_map_FUPDATE_LIST
(cv_st_set cv_f (cv_fst (cv_fst cv_v)) (cv_snd (cv_fst cv_v)))
(cv_snd cv_v)) (Num 0)) cv_f
cv_mk_Branch_def
⊢ ∀cv_c cv_v cv_t2.
cv_mk_Branch cv_c cv_v cv_t2 =
cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 1) (cv_fst cv_v))
(Pair (Num 2)
(Pair cv_c
(Pair
(Pair (Num 2)
(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_t2)))
(Pair (Num 2)
(Pair cv_c (Pair (Pair (Num 1) (cv_snd cv_v)) cv_t2)))) cv_t2
cv_st_card_def_primitive
⊢ cv_st_card =
WFREC
(@R. WF R ∧
(∀cv_v.
cv$c2b (cv_ispair cv_v) ∧ cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ⇒
R (cv_fst (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)) ⇒
R (cv_snd (cv_snd (cv_snd cv_v))) cv_v)
(λcv_st_card a.
I
(cv_if (cv_ispair a)
(cv_if (cv_lt (Num 1) (cv_fst a))
(cv_add (cv_st_card (cv_fst (cv_snd (cv_snd a))))
(cv_st_card (cv_snd (cv_snd (cv_snd a))))) (Num 1))
(Num 0)))
cv_st_del_def
⊢ ∀cv_t cv_v.
cv_st_del cv_t cv_v =
cv_if (cv_ispair cv_v)
(cv_st_del_cons cv_t (cv_fst cv_v) (cv_snd cv_v))
(cv_st_del_nil cv_t)
cv_st_del_nil_def_primitive
⊢ cv_st_del_nil =
WFREC
(@R. WF R ∧
∀cv_v.
cv$c2b (cv_ispair cv_v) ∧ cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ⇒
R (cv_snd (cv_snd (cv_snd cv_v))) cv_v)
(λcv_st_del_nil a.
I
(cv_if (cv_ispair a)
(cv_if (cv_lt (Num 1) (cv_fst a))
(Pair (Num 2)
(Pair (cv_fst (cv_snd a))
(Pair (cv_fst (cv_snd (cv_snd a)))
(cv_st_del_nil (cv_snd (cv_snd (cv_snd a)))))))
(Num 0)) (Num 0)))
cv_st_get_def
⊢ (∀cv_t cv_v.
cv_st_get cv_t cv_v =
cv_if (cv_ispair cv_v)
(cv_st_get_cons cv_t (cv_fst cv_v) (cv_snd cv_v))
(cv_st_get_nil cv_t)) ∧
∀cv_v cv_x cv_xs.
cv_st_get_cons cv_v cv_x cv_xs =
cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 1) (cv_fst cv_v))
(cv_if (cv_lt cv_x (cv_fst (cv_snd cv_v))) (Num 0)
(cv_if (cv_lt (cv_fst (cv_snd cv_v)) cv_x)
(cv_st_get_cons (cv_snd (cv_snd (cv_snd cv_v))) cv_x cv_xs)
(cv_st_get (cv_fst (cv_snd (cv_snd cv_v))) cv_xs))) (Num 0))
(Num 0)
cv_st_get_nil_def
⊢ ∀cv_v.
cv_st_get_nil cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 1) (cv_fst cv_v))
(cv_st_get_nil (cv_snd (cv_snd (cv_snd cv_v))))
(Pair (Num 1) (cv_snd cv_v))) (Num 0)
cv_st_set_def
⊢ ∀cv_t cv_v cv_y.
cv_st_set cv_t cv_v cv_y =
cv_if (cv_ispair cv_v)
(cv_st_set_cons cv_t (cv_fst cv_v) (cv_snd cv_v) cv_y)
(cv_st_set_nil cv_t cv_y)
cv_st_to_list_def
⊢ ∀cv_t. cv_st_to_list cv_t = cv_st_lex_acc cv_t (Num 0) (Num 0)
⊢ ∀m. fmap_to_sorted_list m =
@l. ALOOKUP l = FLOOKUP m ∧ SORTED string_lt (MAP FST l)
from_cv_string_fmap_str_trie_def
⊢ (∀f0. from_cv_string_fmap_str_trie f0 Nothing = Num 0) ∧
(∀f0 v0. from_cv_string_fmap_str_trie f0 (Just v0) = Pair (Num 1) (f0 v0)) ∧
∀f0 v0 v1 v2.
from_cv_string_fmap_str_trie f0 (Branch v0 v1 v2) =
Pair (Num 2)
(Pair (from_char v0)
(Pair (from_cv_string_fmap_str_trie f0 v1)
(from_cv_string_fmap_str_trie f0 v2)))
⊢ ∀f m.
from_string_fmap f m =
from_cv_string_fmap_str_trie f (st_sets Nothing (fmap_to_alist m))
⊢ (∀c t2. mk_Branch c Nothing t2 = t2) ∧
(∀c x t2. mk_Branch c (Just x) t2 = Branch c (Just x) t2) ∧
∀c a b d t2. mk_Branch c (Branch a b d) t2 = Branch c (Branch a b d) t2
⊢ st_card Nothing = 0 ∧ (∀x. st_card (Just x) = 1) ∧
∀c t1 t2. st_card (Branch c t1 t2) = st_card t1 + st_card t2
⊢ (∀x xs. st_del_cons Nothing x xs = Nothing) ∧
(∀z x xs. st_del_cons (Just z) x xs = Just z) ∧
∀c subtrie rest x xs.
st_del_cons (Branch c subtrie rest) x xs =
if char_gt c x then Branch c subtrie rest
else if char_lt c x then Branch c subtrie (st_del_cons rest x xs)
else
mk_Branch c
(case xs of
"" => st_del_nil subtrie
| STRING x xs => st_del_cons subtrie x xs) rest
⊢ (∀t. st_del t "" = st_del_nil t) ∧
∀t x xs. st_del t (STRING x xs) = st_del_cons t x xs
st_del_nil_def_primitive
⊢ st_del_nil =
WFREC (@R. WF R ∧ ∀y x rest. R rest (Branch x y rest))
(λst_del_nil a.
case a of
Nothing => I Nothing
| Just v4 => I Nothing
| Branch x y rest => I (Branch x y (st_del_nil rest)))
⊢ st_flat Nothing = [] ∧ (∀a. st_flat (Just a) = [("",a)]) ∧
∀c t1 t2.
st_flat (Branch c t1 t2) =
MAP (λ(k,v). (STRING c k,v)) (st_flat t1) ⧺ st_flat t2
⊢ (∀v0 v1 rest. st_get_nil (Branch v0 v1 rest) = st_get_nil rest) ∧
(∀x. st_get_nil (Just x) = SOME x) ∧ st_get_nil Nothing = NONE
⊢ (∀y. st_make "" y = Just y) ∧
∀x xs y. st_make (STRING x xs) y = Branch x (st_make xs y) Nothing
⊢ (∀x xs y. st_set_cons Nothing x xs y = Branch x (st_make xs y) Nothing) ∧
(∀z x xs y.
st_set_cons (Just z) x xs y = Branch x (st_make xs y) (Just z)) ∧
∀c subtrie rest x xs y.
st_set_cons (Branch c subtrie rest) x xs y =
if char_gt c x then Branch x (st_make xs y) (Branch c subtrie rest)
else if char_lt c x then Branch c subtrie (st_set_cons rest x xs y)
else
Branch c
(case xs of
"" => st_set_nil subtrie y
| STRING x xs => st_set_cons subtrie x xs y) rest
⊢ (∀t y. st_set t "" y = st_set_nil t y) ∧
∀t x xs y. st_set t (STRING x xs) y = st_set_cons t x xs y
⊢ (st_sorted Nothing ⇔ T) ∧ (∀x. st_sorted (Just x) ⇔ T) ∧
∀c t1 t2.
st_sorted (Branch c t1 t2) ⇔
t1 ≠ Nothing ∧ st_sorted t1 ∧ st_sorted t2 ∧
∀c' t1' t2'. t2 = Branch c' t1' t2' ⇒ char_lt c c'
⊢ ∀t. st_to_list t = st_lex_acc t "" []
str_trie_TY_DEF
⊢ ∃rep.
TYPE_DEFINITION
(λa0'.
∀ $var$('str_trie').
(∀a0'.
a0' = ind_type$CONSTR 0 (ARB,ARB) (λn. ind_type$BOTTOM) ∨
(∃a. a0' =
(λa.
ind_type$CONSTR (SUC 0) (a,ARB) (λn. ind_type$BOTTOM))
a) ∨
(∃a0 a1 a2.
a0' =
(λa0 a1 a2.
ind_type$CONSTR (SUC (SUC 0)) (ARB,a0)
(ind_type$FCONS a1
(ind_type$FCONS a2 (λn. ind_type$BOTTOM)))) a0 a1
a2 ∧ $var$('str_trie') a1 ∧ $var$('str_trie') a2) ⇒
$var$('str_trie') a0') ⇒
$var$('str_trie') a0') rep
str_trie_case_def
⊢ (∀v f f1. str_trie_CASE Nothing v f f1 = v) ∧
(∀a v f f1. str_trie_CASE (Just a) v f f1 = f a) ∧
∀a0 a1 a2 v f f1. str_trie_CASE (Branch a0 a1 a2) v f f1 = f1 a0 a1 a2
str_trie_size_def
⊢ (∀f. str_trie_size f Nothing = 0) ∧
(∀f a. str_trie_size f (Just a) = 1 + f a) ∧
∀f a0 a1 a2.
str_trie_size f (Branch a0 a1 a2) =
1 + (char_size a0 + (str_trie_size f a1 + str_trie_size f a2))
to_str_trie_curried_def
⊢ ∀x x0. to_str_trie x x0 = to_str_trie_tupled (x,x0)
to_str_trie_tupled_primitive_def
⊢ to_str_trie_tupled =
WFREC
(@R. WF R ∧
(∀t0 v.
cv_has_shape [SOME 2; NONE; NONE] v ⇒
R (t0,cv_fst (cv_snd (cv_snd v))) (t0,v)) ∧
∀t0 v.
cv_has_shape [SOME 2; NONE; NONE] v ⇒
R (t0,cv_snd (cv_snd (cv_snd v))) (t0,v))
(λto_str_trie_tupled a.
case a of
(t0,v) =>
I
(if cv_has_shape [SOME 2; NONE; NONE] v then
Branch (to_char (cv_fst (cv_snd v)))
(to_str_trie_tupled (t0,cv_fst (cv_snd (cv_snd v))))
(to_str_trie_tupled (t0,cv_snd (cv_snd (cv_snd v))))
else if v = Num 0 then Nothing
else Just (t0 (cv_snd v))))
⊢ ∀t m. to_string_fmap t m = alist_to_fmap (st_flat (to_str_trie t m))
Theorems
⊢ st_sorted t ⇒ ALOOKUP (st_flat t) n = st_get t n
⊢ (∀t. st_sorted t ⇒ ∀k. ALOOKUP (st_lex t) k = st_get t k) ∧
∀t. st_sorted t ⇒
∀k. ALOOKUP (st_branches t) k = if k = "" then NONE else st_get t k
⊢ ∀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
⊢ LENGTH (fmap_to_sorted_list m) = FCARD m
⊢ (∀t. st_sorted t ⇒ SORTED string_lt (MAP FST (st_lex t))) ∧
∀t. st_sorted t ⇒ SORTED string_lt (MAP FST (st_branches t))
cv_finite_map_FUPDATE_LIST_thm
⊢ FUPDATE_LIST_pre f v ⇒
from_string_fmap f_b (f |++ v) =
cv_finite_map_FUPDATE_LIST (from_string_fmap f_b f)
(from_list (from_pair (from_list from_char) f_b) v)
cv_mk_Branch_thm
⊢ from_cv_string_fmap_str_trie f_a (mk_Branch c v t2) =
cv_mk_Branch (from_char c) (from_cv_string_fmap_str_trie f_a v)
(from_cv_string_fmap_str_trie f_a t2)
cv_rep_cv_string_fmap_str_trie_datatype
⊢ (cv_rep p cv (from_cv_string_fmap_str_trie f_a) x ∧
cv_rep Nothing_pre Nothing_cv f_b f0 ∧
(∀v0. cv_rep (Just_pre v0) (Just_cv (f_a v0)) f_b (f1 v0)) ∧
(∀v0 v1 v2.
cv_rep (Branch_pre v0 v1 v2)
(Branch_cv (from_char v0) (from_cv_string_fmap_str_trie f_a v1)
(from_cv_string_fmap_str_trie f_a v2)) f_b (f2 v0 v1 v2)) ⇒
cv_rep
(p ∧ (x = Nothing ⇒ Nothing_pre) ∧ (∀v0. x = Just v0 ⇒ Just_pre v0) ∧
∀v0 v1 v2. x = Branch v0 v1 v2 ⇒ Branch_pre v0 v1 v2)
(cv_if (cv_ispair cv)
(cv_if (cv_lt (Num 1) (cv_fst cv))
(Branch_cv (cv_fst (cv_snd cv)) (cv_fst (cv_snd (cv_snd cv)))
(cv_snd (cv_snd (cv_snd cv)))) (Just_cv (cv_snd cv)))
Nothing_cv) f_b (str_trie_CASE x f0 f1 f2)) ∧
from_cv_string_fmap_str_trie f0 Nothing = Num 0 ∧
from_cv_string_fmap_str_trie f0 (Just v0) = Pair (Num 1) (f0 v0) ∧
from_cv_string_fmap_str_trie f0 (Branch v0 v1 v2) =
Pair (Num 2)
(Pair (from_char v0)
(Pair (from_cv_string_fmap_str_trie f0 v1)
(from_cv_string_fmap_str_trie f0 v2)))
⊢ from_string_fmap f (m \\ k) =
cv_st_del (from_string_fmap f m) (from_list from_char k)
⊢ Num (FCARD m) = cv_st_card (from_string_fmap f m)
⊢ from_string_fmap f FEMPTY = Num 0
⊢ from_string_fmap f (FINTER m1 m2) =
cv_st_inter (from_string_fmap f m1) (from_string_fmap g m2)
⊢ from_option f (FLOOKUP m n) =
cv_st_get (from_string_fmap f m) (from_list from_char n)
⊢ from_string_fmap f (FMINUS m1 m2) =
cv_st_minus (from_string_fmap f m1) (from_string_fmap g m2)
⊢ from_string_fmap f (m1 ⊌ m2) =
cv_st_union (from_string_fmap f m1) (from_string_fmap f m2)
⊢ from_string_fmap f m⟨k ↦ v⟩ =
cv_st_set (from_string_fmap f m) (from_list from_char k) (f v)
⊢ from_to f_a t_a ⇒
cv_rep T
(cv_st_submap (from_string_fmap f_a m1) (from_string_fmap f_a m2)) b2c
(m1 ⊑ m2)
⊢ from_list (from_pair (from_list from_char) f) (fmap_to_sorted_list m) =
cv_st_to_list (from_string_fmap f m)
cv_st_card_def
⊢ ∀cv_v.
cv_st_card cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 1) (cv_fst cv_v))
(cv_add (cv_st_card (cv_fst (cv_snd (cv_snd cv_v))))
(cv_st_card (cv_snd (cv_snd (cv_snd cv_v))))) (Num 1)) (Num 0)
cv_st_card_ind
⊢ ∀P. (∀cv_v.
(cv$c2b (cv_ispair cv_v) ∧ cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ⇒
P (cv_fst (cv_snd (cv_snd cv_v)))) ∧
(cv$c2b (cv_ispair cv_v) ∧ cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ⇒
P (cv_snd (cv_snd (cv_snd cv_v)))) ⇒
P cv_v) ⇒
∀v. P v
cv_st_card_thm
⊢ Num (st_card v) = cv_st_card (from_cv_string_fmap_str_trie f_a v)
cv_st_del_cons_def
⊢ ∀cv_xs cv_x cv_v.
cv_st_del_cons cv_v cv_x cv_xs =
cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 1) (cv_fst cv_v))
(cv_if (cv_lt cv_x (cv_fst (cv_snd cv_v)))
(Pair (Num 2)
(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_lt (cv_fst (cv_snd cv_v)) cv_x)
(Pair (Num 2)
(Pair (cv_fst (cv_snd cv_v))
(Pair (cv_fst (cv_snd (cv_snd cv_v)))
(cv_st_del_cons (cv_snd (cv_snd (cv_snd cv_v)))
cv_x cv_xs))))
(cv_mk_Branch (cv_fst (cv_snd cv_v))
(cv_if (cv_ispair cv_xs)
(cv_st_del_cons (cv_fst (cv_snd (cv_snd cv_v)))
(cv_fst cv_xs) (cv_snd cv_xs))
(cv_st_del_nil (cv_fst (cv_snd (cv_snd cv_v)))))
(cv_snd (cv_snd (cv_snd cv_v))))))
(Pair (Num 1) (cv_snd cv_v))) (Num 0)
cv_st_del_cons_ind
⊢ ∀P. (∀cv_v cv_x cv_xs.
(cv$c2b (cv_ispair cv_v) ∧ cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt cv_x (cv_fst (cv_snd cv_v))) ∧
cv$c2b (cv_lt (cv_fst (cv_snd cv_v)) cv_x) ⇒
P (cv_snd (cv_snd (cv_snd cv_v))) cv_x cv_xs) ∧
(cv$c2b (cv_ispair cv_v) ∧ cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt cv_x (cv_fst (cv_snd cv_v))) ∧
¬cv$c2b (cv_lt (cv_fst (cv_snd cv_v)) cv_x) ∧
cv$c2b (cv_ispair cv_xs) ⇒
P (cv_fst (cv_snd (cv_snd cv_v))) (cv_fst cv_xs) (cv_snd cv_xs)) ⇒
P cv_v cv_x cv_xs) ⇒
∀v v1 v2. P v v1 v2
cv_st_del_cons_thm
⊢ from_cv_string_fmap_str_trie f_a (st_del_cons v x xs) =
cv_st_del_cons (from_cv_string_fmap_str_trie f_a v) (from_char x)
(from_list from_char xs)
cv_st_del_nil_def
⊢ ∀cv_v.
cv_st_del_nil cv_v =
cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 1) (cv_fst cv_v))
(Pair (Num 2)
(Pair (cv_fst (cv_snd cv_v))
(Pair (cv_fst (cv_snd (cv_snd cv_v)))
(cv_st_del_nil (cv_snd (cv_snd (cv_snd cv_v)))))))
(Num 0)) (Num 0)
cv_st_del_nil_ind
⊢ ∀P. (∀cv_v.
(cv$c2b (cv_ispair cv_v) ∧ cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ⇒
P (cv_snd (cv_snd (cv_snd cv_v)))) ⇒
P cv_v) ⇒
∀v. P v
cv_st_del_nil_thm
⊢ from_cv_string_fmap_str_trie f_a (st_del_nil v) =
cv_st_del_nil (from_cv_string_fmap_str_trie f_a v)
cv_st_del_thm
⊢ from_cv_string_fmap_str_trie f_a (st_del t v) =
cv_st_del (from_cv_string_fmap_str_trie f_a t) (from_list from_char v)
cv_st_get_nil_thm
⊢ from_option f_a (st_get_nil v) =
cv_st_get_nil (from_cv_string_fmap_str_trie f_a v)
cv_st_get_thm
⊢ from_option f_a (st_get t v) =
cv_st_get (from_cv_string_fmap_str_trie f_a t) (from_list from_char v) ∧
from_option f_a (st_get_cons v x xs) =
cv_st_get_cons (from_cv_string_fmap_str_trie f_a v) (from_char x)
(from_list from_char xs)
cv_st_inter_def
⊢ ∀cv_v0 cv_v.
cv_st_inter 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_ispair (cv_snd cv0))
(cv_if (cv_lt (Num 1) (cv_fst (cv_snd cv0)))
(cv_if
(cv_lt (cv_fst (cv_snd (cv_fst cv0)))
(cv_fst (cv_snd (cv_snd cv0))))
(cv_st_inter
(cv_snd (cv_snd (cv_snd (cv_fst cv0))))
(Pair (Num 2)
(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))))))))
(cv_if
(cv_lt (cv_fst (cv_snd (cv_snd cv0)))
(cv_fst (cv_snd (cv_fst cv0))))
(cv_st_inter
(Pair (Num 2)
(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 (cv_snd (cv_snd (cv_snd cv0)))))
(cv_mk_Branch (cv_fst (cv_snd (cv_fst cv0)))
(cv_st_inter
(cv_fst (cv_snd (cv_snd (cv_fst cv0))))
(cv_fst (cv_snd (cv_snd (cv_snd cv0)))))
(cv_st_inter
(cv_snd (cv_snd (cv_snd (cv_fst cv0))))
(cv_snd (cv_snd (cv_snd (cv_snd cv0))))))))
(cv_st_inter (cv_snd (cv_snd (cv_snd (cv_fst cv0))))
(Pair (Num 1) (cv_snd (cv_snd cv0))))) (Num 0))
(cv_if (cv_ispair (cv_snd cv0))
(cv_if (cv_lt (Num 1) (cv_fst (cv_snd cv0)))
(cv_st_inter (Pair (Num 1) (cv_snd (cv_fst cv0)))
(cv_snd (cv_snd (cv_snd (cv_snd cv0)))))
(Pair (Num 1) (cv_snd (cv_fst cv0)))) (Num 0)))
(Num 0)) (Num 0))
cv_st_inter_ind
⊢ ∀P. (∀cv_v0 cv_v.
(∀cv0.
cv0 = Pair cv_v0 cv_v ∧ cv$c2b (cv_ispair cv0) ∧
cv$c2b (cv_ispair (cv_fst cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_fst cv0))) ∧
cv$c2b (cv_ispair (cv_snd cv0)) ∧
¬cv$c2b (cv_lt (Num 1) (cv_fst (cv_snd cv0))) ⇒
P (cv_snd (cv_snd (cv_snd (cv_fst cv0))))
(Pair (Num 1) (cv_snd (cv_snd cv0)))) ∧
(∀cv0.
cv0 = Pair cv_v0 cv_v ∧ cv$c2b (cv_ispair cv0) ∧
cv$c2b (cv_ispair (cv_fst cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_fst cv0))) ∧
cv$c2b (cv_ispair (cv_snd cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_snd cv0))) ∧
cv$c2b
(cv_lt (cv_fst (cv_snd (cv_fst cv0)))
(cv_fst (cv_snd (cv_snd cv0)))) ⇒
P (cv_snd (cv_snd (cv_snd (cv_fst cv0))))
(Pair (Num 2)
(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)))))))) ∧
(∀cv0.
cv0 = Pair cv_v0 cv_v ∧ cv$c2b (cv_ispair cv0) ∧
cv$c2b (cv_ispair (cv_fst cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_fst cv0))) ∧
cv$c2b (cv_ispair (cv_snd cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_snd cv0))) ∧
¬cv$c2b
(cv_lt (cv_fst (cv_snd (cv_fst cv0)))
(cv_fst (cv_snd (cv_snd cv0)))) ∧
cv$c2b
(cv_lt (cv_fst (cv_snd (cv_snd cv0)))
(cv_fst (cv_snd (cv_fst cv0)))) ⇒
P
(Pair (Num 2)
(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 (cv_snd (cv_snd (cv_snd cv0))))) ∧
(∀cv0.
cv0 = Pair cv_v0 cv_v ∧ cv$c2b (cv_ispair cv0) ∧
cv$c2b (cv_ispair (cv_fst cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_fst cv0))) ∧
cv$c2b (cv_ispair (cv_snd cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_snd cv0))) ∧
¬cv$c2b
(cv_lt (cv_fst (cv_snd (cv_fst cv0)))
(cv_fst (cv_snd (cv_snd cv0)))) ∧
¬cv$c2b
(cv_lt (cv_fst (cv_snd (cv_snd cv0)))
(cv_fst (cv_snd (cv_fst cv0)))) ⇒
P (cv_fst (cv_snd (cv_snd (cv_fst cv0))))
(cv_fst (cv_snd (cv_snd (cv_snd cv0))))) ∧
(∀cv0.
cv0 = Pair cv_v0 cv_v ∧ cv$c2b (cv_ispair cv0) ∧
cv$c2b (cv_ispair (cv_fst cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_fst cv0))) ∧
cv$c2b (cv_ispair (cv_snd cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_snd cv0))) ∧
¬cv$c2b
(cv_lt (cv_fst (cv_snd (cv_fst cv0)))
(cv_fst (cv_snd (cv_snd cv0)))) ∧
¬cv$c2b
(cv_lt (cv_fst (cv_snd (cv_snd cv0)))
(cv_fst (cv_snd (cv_fst cv0)))) ⇒
P (cv_snd (cv_snd (cv_snd (cv_fst cv0))))
(cv_snd (cv_snd (cv_snd (cv_snd cv0))))) ∧
(∀cv0.
cv0 = Pair cv_v0 cv_v ∧ cv$c2b (cv_ispair cv0) ∧
cv$c2b (cv_ispair (cv_fst cv0)) ∧
¬cv$c2b (cv_lt (Num 1) (cv_fst (cv_fst cv0))) ∧
cv$c2b (cv_ispair (cv_snd cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_snd cv0))) ⇒
P (Pair (Num 1) (cv_snd (cv_fst cv0)))
(cv_snd (cv_snd (cv_snd (cv_snd cv0))))) ⇒
P cv_v0 cv_v) ⇒
∀v v1. P v v1
cv_st_inter_thm
⊢ from_cv_string_fmap_str_trie f_a (st_inter v0 v) =
cv_st_inter (from_cv_string_fmap_str_trie f_a v0)
(from_cv_string_fmap_str_trie f_b v)
cv_st_lex_acc_def
⊢ (∀cv_t cv_rp cv_acc.
cv_st_lex_acc cv_t cv_rp cv_acc =
(let
cv0 = cv_st_get_nil cv_t
in
cv_if (cv_ispair cv0)
(Pair (Pair (cv_REVERSE cv_rp) (cv_snd cv0))
(cv_st_branches_acc cv_t cv_rp cv_acc))
(cv_st_branches_acc cv_t cv_rp cv_acc))) ∧
∀cv_v cv_rp cv_acc.
cv_st_branches_acc cv_v cv_rp cv_acc =
cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 1) (cv_fst cv_v))
(cv_st_lex_acc (cv_fst (cv_snd (cv_snd cv_v)))
(Pair (cv_fst (cv_snd cv_v)) cv_rp)
(cv_st_branches_acc (cv_snd (cv_snd (cv_snd cv_v))) cv_rp
cv_acc)) cv_acc) cv_acc
cv_st_lex_acc_ind
⊢ ∀P0 P1.
(∀cv_t cv_rp cv_acc.
(∀cv0.
cv0 = cv_st_get_nil cv_t ∧ cv$c2b (cv_ispair cv0) ⇒
P1 cv_t cv_rp cv_acc) ∧
(∀cv0.
cv0 = cv_st_get_nil cv_t ∧ ¬cv$c2b (cv_ispair cv0) ⇒
P1 cv_t cv_rp cv_acc) ⇒
P0 cv_t cv_rp cv_acc) ∧
(∀cv_v cv_rp cv_acc.
(cv$c2b (cv_ispair cv_v) ∧ cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ⇒
P0 (cv_fst (cv_snd (cv_snd cv_v)))
(Pair (cv_fst (cv_snd cv_v)) cv_rp)
(cv_st_branches_acc (cv_snd (cv_snd (cv_snd cv_v))) cv_rp cv_acc)) ∧
(cv$c2b (cv_ispair cv_v) ∧ cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ⇒
P1 (cv_snd (cv_snd (cv_snd cv_v))) cv_rp cv_acc) ⇒
P1 cv_v cv_rp cv_acc) ⇒
(∀v0 v1 v2. P0 v0 v1 v2) ∧ ∀v0 v1 v2. P1 v0 v1 v2
cv_st_lex_acc_thm
⊢ (st_lex_acc_pre t rp acc ⇒
from_list (from_pair (from_list from_char) f_a) (st_lex_acc t rp acc) =
cv_st_lex_acc (from_cv_string_fmap_str_trie f_a t)
(from_list from_char rp)
(from_list (from_pair (from_list from_char) f_a) acc)) ∧
(st_branches_acc_pre v rp acc ⇒
from_list (from_pair (from_list from_char) f_a)
(st_branches_acc v rp acc) =
cv_st_branches_acc (from_cv_string_fmap_str_trie f_a v)
(from_list from_char rp)
(from_list (from_pair (from_list from_char) f_a) acc))
cv_st_make_def
⊢ ∀cv_y cv_v.
cv_st_make cv_v cv_y =
cv_if (cv_ispair cv_v)
(Pair (Num 2)
(Pair (cv_fst cv_v) (Pair (cv_st_make (cv_snd cv_v) cv_y) (Num 0))))
(Pair (Num 1) cv_y)
cv_st_make_ind
⊢ ∀P. (∀cv_v cv_y.
(cv$c2b (cv_ispair cv_v) ⇒ P (cv_snd cv_v) cv_y) ⇒ P cv_v cv_y) ⇒
∀v v1. P v v1
cv_st_make_thm
⊢ from_cv_string_fmap_str_trie f_a (st_make v y) =
cv_st_make (from_list from_char v) (f_a y)
cv_st_minus_def
⊢ ∀cv_v0 cv_v.
cv_st_minus 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_ispair (cv_snd cv0))
(cv_if (cv_lt (Num 1) (cv_fst (cv_snd cv0)))
(cv_if
(cv_lt (cv_fst (cv_snd (cv_fst cv0)))
(cv_fst (cv_snd (cv_snd cv0))))
(Pair (Num 2)
(Pair (cv_fst (cv_snd (cv_fst cv0)))
(Pair (cv_fst (cv_snd (cv_snd (cv_fst cv0))))
(cv_st_minus
(cv_snd (cv_snd (cv_snd (cv_fst cv0))))
(Pair (Num 2)
(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)))))))))))
(cv_if
(cv_lt (cv_fst (cv_snd (cv_snd cv0)))
(cv_fst (cv_snd (cv_fst cv0))))
(cv_st_minus
(Pair (Num 2)
(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 (cv_snd (cv_snd (cv_snd cv0)))))
(cv_mk_Branch (cv_fst (cv_snd (cv_fst cv0)))
(cv_st_minus
(cv_fst (cv_snd (cv_snd (cv_fst cv0))))
(cv_fst (cv_snd (cv_snd (cv_snd cv0)))))
(cv_st_minus
(cv_snd (cv_snd (cv_snd (cv_fst cv0))))
(cv_snd (cv_snd (cv_snd (cv_snd cv0))))))))
(Pair (Num 2)
(Pair (cv_fst (cv_snd (cv_fst cv0)))
(Pair (cv_fst (cv_snd (cv_snd (cv_fst cv0))))
(cv_st_minus
(cv_snd (cv_snd (cv_snd (cv_fst cv0))))
(Pair (Num 1) (cv_snd (cv_snd cv0))))))))
(Pair (Num 2)
(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_if (cv_ispair (cv_snd cv0))
(cv_if (cv_lt (Num 1) (cv_fst (cv_snd cv0)))
(cv_st_minus (Pair (Num 1) (cv_snd (cv_fst cv0)))
(cv_snd (cv_snd (cv_snd (cv_snd cv0))))) (Num 0))
(Pair (Num 1) (cv_snd (cv_fst cv0))))) (Num 0)) (Num 0))
cv_st_minus_ind
⊢ ∀P. (∀cv_v0 cv_v.
(∀cv0.
cv0 = Pair cv_v0 cv_v ∧ cv$c2b (cv_ispair cv0) ∧
cv$c2b (cv_ispair (cv_fst cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_fst cv0))) ∧
cv$c2b (cv_ispair (cv_snd cv0)) ∧
¬cv$c2b (cv_lt (Num 1) (cv_fst (cv_snd cv0))) ⇒
P (cv_snd (cv_snd (cv_snd (cv_fst cv0))))
(Pair (Num 1) (cv_snd (cv_snd cv0)))) ∧
(∀cv0.
cv0 = Pair cv_v0 cv_v ∧ cv$c2b (cv_ispair cv0) ∧
cv$c2b (cv_ispair (cv_fst cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_fst cv0))) ∧
cv$c2b (cv_ispair (cv_snd cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_snd cv0))) ∧
cv$c2b
(cv_lt (cv_fst (cv_snd (cv_fst cv0)))
(cv_fst (cv_snd (cv_snd cv0)))) ⇒
P (cv_snd (cv_snd (cv_snd (cv_fst cv0))))
(Pair (Num 2)
(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)))))))) ∧
(∀cv0.
cv0 = Pair cv_v0 cv_v ∧ cv$c2b (cv_ispair cv0) ∧
cv$c2b (cv_ispair (cv_fst cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_fst cv0))) ∧
cv$c2b (cv_ispair (cv_snd cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_snd cv0))) ∧
¬cv$c2b
(cv_lt (cv_fst (cv_snd (cv_fst cv0)))
(cv_fst (cv_snd (cv_snd cv0)))) ∧
cv$c2b
(cv_lt (cv_fst (cv_snd (cv_snd cv0)))
(cv_fst (cv_snd (cv_fst cv0)))) ⇒
P
(Pair (Num 2)
(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 (cv_snd (cv_snd (cv_snd cv0))))) ∧
(∀cv0.
cv0 = Pair cv_v0 cv_v ∧ cv$c2b (cv_ispair cv0) ∧
cv$c2b (cv_ispair (cv_fst cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_fst cv0))) ∧
cv$c2b (cv_ispair (cv_snd cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_snd cv0))) ∧
¬cv$c2b
(cv_lt (cv_fst (cv_snd (cv_fst cv0)))
(cv_fst (cv_snd (cv_snd cv0)))) ∧
¬cv$c2b
(cv_lt (cv_fst (cv_snd (cv_snd cv0)))
(cv_fst (cv_snd (cv_fst cv0)))) ⇒
P (cv_fst (cv_snd (cv_snd (cv_fst cv0))))
(cv_fst (cv_snd (cv_snd (cv_snd cv0))))) ∧
(∀cv0.
cv0 = Pair cv_v0 cv_v ∧ cv$c2b (cv_ispair cv0) ∧
cv$c2b (cv_ispair (cv_fst cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_fst cv0))) ∧
cv$c2b (cv_ispair (cv_snd cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_snd cv0))) ∧
¬cv$c2b
(cv_lt (cv_fst (cv_snd (cv_fst cv0)))
(cv_fst (cv_snd (cv_snd cv0)))) ∧
¬cv$c2b
(cv_lt (cv_fst (cv_snd (cv_snd cv0)))
(cv_fst (cv_snd (cv_fst cv0)))) ⇒
P (cv_snd (cv_snd (cv_snd (cv_fst cv0))))
(cv_snd (cv_snd (cv_snd (cv_snd cv0))))) ∧
(∀cv0.
cv0 = Pair cv_v0 cv_v ∧ cv$c2b (cv_ispair cv0) ∧
cv$c2b (cv_ispair (cv_fst cv0)) ∧
¬cv$c2b (cv_lt (Num 1) (cv_fst (cv_fst cv0))) ∧
cv$c2b (cv_ispair (cv_snd cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_snd cv0))) ⇒
P (Pair (Num 1) (cv_snd (cv_fst cv0)))
(cv_snd (cv_snd (cv_snd (cv_snd cv0))))) ⇒
P cv_v0 cv_v) ⇒
∀v v1. P v v1
cv_st_minus_thm
⊢ from_cv_string_fmap_str_trie f_a (st_minus v0 v) =
cv_st_minus (from_cv_string_fmap_str_trie f_a v0)
(from_cv_string_fmap_str_trie f_b v)
cv_st_set_cons_def
⊢ ∀cv_y cv_xs cv_x cv_v.
cv_st_set_cons cv_v cv_x cv_xs cv_y =
cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 1) (cv_fst cv_v))
(cv_if (cv_lt cv_x (cv_fst (cv_snd cv_v)))
(Pair (Num 2)
(Pair cv_x
(Pair (cv_st_make cv_xs cv_y)
(Pair (Num 2)
(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_lt (cv_fst (cv_snd cv_v)) cv_x)
(Pair (Num 2)
(Pair (cv_fst (cv_snd cv_v))
(Pair (cv_fst (cv_snd (cv_snd cv_v)))
(cv_st_set_cons (cv_snd (cv_snd (cv_snd cv_v)))
cv_x cv_xs cv_y))))
(Pair (Num 2)
(Pair (cv_fst (cv_snd cv_v))
(Pair
(cv_if (cv_ispair cv_xs)
(cv_st_set_cons (cv_fst (cv_snd (cv_snd cv_v)))
(cv_fst cv_xs) (cv_snd cv_xs) cv_y)
(cv_st_set_nil (cv_fst (cv_snd (cv_snd cv_v)))
cv_y)) (cv_snd (cv_snd (cv_snd cv_v))))))))
(Pair (Num 2)
(Pair cv_x
(Pair (cv_st_make cv_xs cv_y) (Pair (Num 1) (cv_snd cv_v))))))
(Pair (Num 2) (Pair cv_x (Pair (cv_st_make cv_xs cv_y) (Num 0))))
cv_st_set_cons_ind
⊢ ∀P. (∀cv_v cv_x cv_xs cv_y.
(cv$c2b (cv_ispair cv_v) ∧ cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt cv_x (cv_fst (cv_snd cv_v))) ∧
cv$c2b (cv_lt (cv_fst (cv_snd cv_v)) cv_x) ⇒
P (cv_snd (cv_snd (cv_snd cv_v))) cv_x cv_xs cv_y) ∧
(cv$c2b (cv_ispair cv_v) ∧ cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ∧
¬cv$c2b (cv_lt cv_x (cv_fst (cv_snd cv_v))) ∧
¬cv$c2b (cv_lt (cv_fst (cv_snd cv_v)) cv_x) ∧
cv$c2b (cv_ispair cv_xs) ⇒
P (cv_fst (cv_snd (cv_snd cv_v))) (cv_fst cv_xs) (cv_snd cv_xs)
cv_y) ⇒
P cv_v cv_x cv_xs cv_y) ⇒
∀v v1 v2 v3. P v v1 v2 v3
cv_st_set_cons_thm
⊢ from_cv_string_fmap_str_trie f_a (st_set_cons v x xs y) =
cv_st_set_cons (from_cv_string_fmap_str_trie f_a v) (from_char x)
(from_list from_char xs) (f_a y)
cv_st_set_nil_def
⊢ ∀cv_y cv_v.
cv_st_set_nil cv_v cv_y =
cv_if (cv_ispair cv_v)
(cv_if (cv_lt (Num 1) (cv_fst cv_v))
(Pair (Num 2)
(Pair (cv_fst (cv_snd cv_v))
(Pair (cv_fst (cv_snd (cv_snd cv_v)))
(cv_st_set_nil (cv_snd (cv_snd (cv_snd cv_v))) cv_y))))
(Pair (Num 1) cv_y)) (Pair (Num 1) cv_y)
cv_st_set_nil_ind
⊢ ∀P. (∀cv_v cv_y.
(cv$c2b (cv_ispair cv_v) ∧ cv$c2b (cv_lt (Num 1) (cv_fst cv_v)) ⇒
P (cv_snd (cv_snd (cv_snd cv_v))) cv_y) ⇒
P cv_v cv_y) ⇒
∀v v1. P v v1
cv_st_set_nil_thm
⊢ from_cv_string_fmap_str_trie f_a (st_set_nil v y) =
cv_st_set_nil (from_cv_string_fmap_str_trie f_a v) (f_a y)
cv_st_set_thm
⊢ from_cv_string_fmap_str_trie f_a (st_set t v y) =
cv_st_set (from_cv_string_fmap_str_trie f_a t) (from_list from_char v)
(f_a y)
cv_st_submap_def
⊢ ∀cv_v0 cv_v.
cv_st_submap 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_ispair (cv_snd cv0))
(cv_if (cv_lt (Num 1) (cv_fst (cv_snd cv0)))
(cv_if
(cv_lt (cv_fst (cv_snd (cv_fst cv0)))
(cv_fst (cv_snd (cv_snd cv0)))) (Num 0)
(cv_if
(cv_lt (cv_fst (cv_snd (cv_snd cv0)))
(cv_fst (cv_snd (cv_fst cv0))))
(cv_st_submap
(Pair (Num 2)
(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 (cv_snd (cv_snd (cv_snd cv0)))))
(cv_if
(cv_st_submap
(cv_fst (cv_snd (cv_snd (cv_fst cv0))))
(cv_fst (cv_snd (cv_snd (cv_snd cv0)))))
(cv_st_submap
(cv_snd (cv_snd (cv_snd (cv_fst cv0))))
(cv_snd (cv_snd (cv_snd (cv_snd cv0)))))
(Num 0)))) (Num 0)) (Num 0))
(cv_if (cv_ispair (cv_snd cv0))
(cv_if (cv_lt (Num 1) (cv_fst (cv_snd cv0)))
(cv_st_submap (Pair (Num 1) (cv_snd (cv_fst cv0)))
(cv_snd (cv_snd (cv_snd (cv_snd cv0)))))
(cv_eq (cv_snd (cv_fst cv0)) (cv_snd (cv_snd cv0))))
(Num 0))) (Num 1)) (Num 0))
cv_st_submap_ind
⊢ ∀P. (∀cv_v0 cv_v.
(∀cv0.
cv0 = Pair cv_v0 cv_v ∧ cv$c2b (cv_ispair cv0) ∧
cv$c2b (cv_ispair (cv_fst cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_fst cv0))) ∧
cv$c2b (cv_ispair (cv_snd cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_snd cv0))) ∧
¬cv$c2b
(cv_lt (cv_fst (cv_snd (cv_fst cv0)))
(cv_fst (cv_snd (cv_snd cv0)))) ∧
cv$c2b
(cv_lt (cv_fst (cv_snd (cv_snd cv0)))
(cv_fst (cv_snd (cv_fst cv0)))) ⇒
P
(Pair (Num 2)
(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 (cv_snd (cv_snd (cv_snd cv0))))) ∧
(∀cv0.
cv0 = Pair cv_v0 cv_v ∧ cv$c2b (cv_ispair cv0) ∧
cv$c2b (cv_ispair (cv_fst cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_fst cv0))) ∧
cv$c2b (cv_ispair (cv_snd cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_snd cv0))) ∧
¬cv$c2b
(cv_lt (cv_fst (cv_snd (cv_fst cv0)))
(cv_fst (cv_snd (cv_snd cv0)))) ∧
¬cv$c2b
(cv_lt (cv_fst (cv_snd (cv_snd cv0)))
(cv_fst (cv_snd (cv_fst cv0)))) ⇒
P (cv_fst (cv_snd (cv_snd (cv_fst cv0))))
(cv_fst (cv_snd (cv_snd (cv_snd cv0))))) ∧
(∀cv0.
cv0 = Pair cv_v0 cv_v ∧ cv$c2b (cv_ispair cv0) ∧
cv$c2b (cv_ispair (cv_fst cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_fst cv0))) ∧
cv$c2b (cv_ispair (cv_snd cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_snd cv0))) ∧
¬cv$c2b
(cv_lt (cv_fst (cv_snd (cv_fst cv0)))
(cv_fst (cv_snd (cv_snd cv0)))) ∧
¬cv$c2b
(cv_lt (cv_fst (cv_snd (cv_snd cv0)))
(cv_fst (cv_snd (cv_fst cv0)))) ∧
cv$c2b
(cv_st_submap (cv_fst (cv_snd (cv_snd (cv_fst cv0))))
(cv_fst (cv_snd (cv_snd (cv_snd cv0))))) ⇒
P (cv_snd (cv_snd (cv_snd (cv_fst cv0))))
(cv_snd (cv_snd (cv_snd (cv_snd cv0))))) ∧
(∀cv0.
cv0 = Pair cv_v0 cv_v ∧ cv$c2b (cv_ispair cv0) ∧
cv$c2b (cv_ispair (cv_fst cv0)) ∧
¬cv$c2b (cv_lt (Num 1) (cv_fst (cv_fst cv0))) ∧
cv$c2b (cv_ispair (cv_snd cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_snd cv0))) ⇒
P (Pair (Num 1) (cv_snd (cv_fst cv0)))
(cv_snd (cv_snd (cv_snd (cv_snd cv0))))) ⇒
P cv_v0 cv_v) ⇒
∀v v1. P v v1
cv_st_submap_thm
[oracles: DISK_THM] [axioms: ] [from_to f_a t_a]
⊢ b2c (st_submap v0 v) =
cv_st_submap (from_cv_string_fmap_str_trie f_a v0)
(from_cv_string_fmap_str_trie f_a v)
cv_st_to_list_thm
⊢ from_list (from_pair (from_list from_char) f_a) (st_to_list t) =
cv_st_to_list (from_cv_string_fmap_str_trie f_a t)
cv_st_union_def
⊢ ∀cv_v0 cv_v.
cv_st_union 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_ispair (cv_snd cv0))
(cv_if (cv_lt (Num 1) (cv_fst (cv_snd cv0)))
(cv_if
(cv_lt (cv_fst (cv_snd (cv_fst cv0)))
(cv_fst (cv_snd (cv_snd cv0))))
(Pair (Num 2)
(Pair (cv_fst (cv_snd (cv_fst cv0)))
(Pair (cv_fst (cv_snd (cv_snd (cv_fst cv0))))
(cv_st_union
(cv_snd (cv_snd (cv_snd (cv_fst cv0))))
(Pair (Num 2)
(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)))))))))))
(cv_if
(cv_lt (cv_fst (cv_snd (cv_snd cv0)))
(cv_fst (cv_snd (cv_fst cv0))))
(Pair (Num 2)
(Pair (cv_fst (cv_snd (cv_snd cv0)))
(Pair
(cv_fst (cv_snd (cv_snd (cv_snd cv0))))
(cv_st_union
(Pair (Num 2)
(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
(cv_snd (cv_snd (cv_snd cv0))))))))
(Pair (Num 2)
(Pair (cv_fst (cv_snd (cv_fst cv0)))
(Pair
(cv_st_union
(cv_fst
(cv_snd (cv_snd (cv_fst cv0))))
(cv_fst
(cv_snd (cv_snd (cv_snd cv0)))))
(cv_st_union
(cv_snd
(cv_snd (cv_snd (cv_fst cv0))))
(cv_snd
(cv_snd (cv_snd (cv_snd cv0))))))))))
(Pair (Num 2)
(Pair (cv_fst (cv_snd (cv_fst cv0)))
(Pair (cv_fst (cv_snd (cv_snd (cv_fst cv0))))
(cv_st_union
(cv_snd (cv_snd (cv_snd (cv_fst cv0))))
(Pair (Num 1) (cv_snd (cv_snd cv0))))))))
(Pair (Num 2)
(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_if (cv_ispair (cv_snd cv0))
(cv_if (cv_lt (Num 1) (cv_fst (cv_snd cv0)))
(Pair (Num 2)
(Pair (cv_fst (cv_snd (cv_snd cv0)))
(Pair (cv_fst (cv_snd (cv_snd (cv_snd cv0))))
(cv_st_union
(Pair (Num 1) (cv_snd (cv_fst cv0)))
(cv_snd (cv_snd (cv_snd (cv_snd cv0))))))))
(Pair (Num 1) (cv_snd (cv_fst cv0))))
(Pair (Num 1) (cv_snd (cv_fst cv0))))) (cv_snd cv0))
(Num 0))
cv_st_union_ind
⊢ ∀P. (∀cv_v0 cv_v.
(∀cv0.
cv0 = Pair cv_v0 cv_v ∧ cv$c2b (cv_ispair cv0) ∧
cv$c2b (cv_ispair (cv_fst cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_fst cv0))) ∧
cv$c2b (cv_ispair (cv_snd cv0)) ∧
¬cv$c2b (cv_lt (Num 1) (cv_fst (cv_snd cv0))) ⇒
P (cv_snd (cv_snd (cv_snd (cv_fst cv0))))
(Pair (Num 1) (cv_snd (cv_snd cv0)))) ∧
(∀cv0.
cv0 = Pair cv_v0 cv_v ∧ cv$c2b (cv_ispair cv0) ∧
cv$c2b (cv_ispair (cv_fst cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_fst cv0))) ∧
cv$c2b (cv_ispair (cv_snd cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_snd cv0))) ∧
cv$c2b
(cv_lt (cv_fst (cv_snd (cv_fst cv0)))
(cv_fst (cv_snd (cv_snd cv0)))) ⇒
P (cv_snd (cv_snd (cv_snd (cv_fst cv0))))
(Pair (Num 2)
(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)))))))) ∧
(∀cv0.
cv0 = Pair cv_v0 cv_v ∧ cv$c2b (cv_ispair cv0) ∧
cv$c2b (cv_ispair (cv_fst cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_fst cv0))) ∧
cv$c2b (cv_ispair (cv_snd cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_snd cv0))) ∧
¬cv$c2b
(cv_lt (cv_fst (cv_snd (cv_fst cv0)))
(cv_fst (cv_snd (cv_snd cv0)))) ∧
cv$c2b
(cv_lt (cv_fst (cv_snd (cv_snd cv0)))
(cv_fst (cv_snd (cv_fst cv0)))) ⇒
P
(Pair (Num 2)
(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 (cv_snd (cv_snd (cv_snd cv0))))) ∧
(∀cv0.
cv0 = Pair cv_v0 cv_v ∧ cv$c2b (cv_ispair cv0) ∧
cv$c2b (cv_ispair (cv_fst cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_fst cv0))) ∧
cv$c2b (cv_ispair (cv_snd cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_snd cv0))) ∧
¬cv$c2b
(cv_lt (cv_fst (cv_snd (cv_fst cv0)))
(cv_fst (cv_snd (cv_snd cv0)))) ∧
¬cv$c2b
(cv_lt (cv_fst (cv_snd (cv_snd cv0)))
(cv_fst (cv_snd (cv_fst cv0)))) ⇒
P (cv_fst (cv_snd (cv_snd (cv_fst cv0))))
(cv_fst (cv_snd (cv_snd (cv_snd cv0))))) ∧
(∀cv0.
cv0 = Pair cv_v0 cv_v ∧ cv$c2b (cv_ispair cv0) ∧
cv$c2b (cv_ispair (cv_fst cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_fst cv0))) ∧
cv$c2b (cv_ispair (cv_snd cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_snd cv0))) ∧
¬cv$c2b
(cv_lt (cv_fst (cv_snd (cv_fst cv0)))
(cv_fst (cv_snd (cv_snd cv0)))) ∧
¬cv$c2b
(cv_lt (cv_fst (cv_snd (cv_snd cv0)))
(cv_fst (cv_snd (cv_fst cv0)))) ⇒
P (cv_snd (cv_snd (cv_snd (cv_fst cv0))))
(cv_snd (cv_snd (cv_snd (cv_snd cv0))))) ∧
(∀cv0.
cv0 = Pair cv_v0 cv_v ∧ cv$c2b (cv_ispair cv0) ∧
cv$c2b (cv_ispair (cv_fst cv0)) ∧
¬cv$c2b (cv_lt (Num 1) (cv_fst (cv_fst cv0))) ∧
cv$c2b (cv_ispair (cv_snd cv0)) ∧
cv$c2b (cv_lt (Num 1) (cv_fst (cv_snd cv0))) ⇒
P (Pair (Num 1) (cv_snd (cv_fst cv0)))
(cv_snd (cv_snd (cv_snd (cv_snd cv0))))) ⇒
P cv_v0 cv_v) ⇒
∀v v1. P v v1
cv_st_union_thm
⊢ from_cv_string_fmap_str_trie f_a (st_union v0 v) =
cv_st_union (from_cv_string_fmap_str_trie f_a v0)
(from_cv_string_fmap_str_trie f_a v)
datatype_str_trie
⊢ DATATYPE (str_trie Nothing Just Branch)
⊢ ALOOKUP l = FLOOKUP m ∧ SORTED string_lt (MAP FST l) ⇒
fmap_to_sorted_list m = l
⊢ ALOOKUP (fmap_to_sorted_list m) = FLOOKUP m ∧
SORTED string_lt (MAP FST (fmap_to_sorted_list m))
from_str_trie_def
⊢ from_cv_string_fmap_str_trie f0 Nothing = Num 0 ∧
from_cv_string_fmap_str_trie f0 (Just v0) = Pair (Num 1) (f0 v0) ∧
from_cv_string_fmap_str_trie f0 (Branch v0 v1 v2) =
Pair (Num 2)
(Pair (from_char v0)
(Pair (from_cv_string_fmap_str_trie f0 v1)
(from_cv_string_fmap_str_trie f0 v2)))
from_to_str_trie_thm
⊢ from_to f0 t0 ⇒
from_to (from_cv_string_fmap_str_trie f0) (to_str_trie t0)
⊢ from_to f0 t0 ⇒ from_to (from_string_fmap f0) (to_string_fmap t0)
⊢ mk_Branch c t1 t2 = if t1 = Nothing then t2 else Branch c t1 t2
⊢ ∀xs. st_del Nothing xs = Nothing
⊢ ∀t x xs c rest. st_sorted t ⇒ st_del_cons t x xs ≠ Branch c Nothing rest
⊢ (∀y x rest. st_del_nil (Branch x y rest) = Branch x y (st_del_nil rest)) ∧
st_del_nil Nothing = Nothing ∧ ∀v. st_del_nil (Just v) = Nothing
⊢ ∀P. (∀x y rest. P rest ⇒ P (Branch x y rest)) ∧ P Nothing ∧
(∀v. P (Just v)) ⇒
∀v. P v
⊢ st_sorted t ⇒
st_del (st_set t n x) m =
if m = n then st_del t m else st_set (st_del t m) n x
⊢ st_sorted t ⇒
st_del (st_sets t xs) n =
st_sets (st_del t n) (FILTER (λ(k,v). k ≠ n) xs)
⊢ ∀xs. st_get Nothing xs = NONE
⊢ ∀c t1 t2 x xs.
st_get_cons (mk_Branch c t1 t2) x xs =
if t1 = Nothing then st_get_cons t2 x xs
else st_get_cons (Branch c t1 t2) x xs
⊢ ∀t h rest.
st_sorted t ⇒
(∀c' t1' t2'. t = Branch c' t1' t2' ⇒ char_lt h c') ⇒
st_get_cons t h rest = NONE
⊢ ∀t x xs h rest.
st_sorted t ⇒
st_get_cons (st_del_cons t x xs) h rest =
if h = x ∧ rest = xs then NONE else st_get_cons t h rest
⊢ ∀t x xs. st_get_cons (st_del_nil t) x xs = st_get_cons t x xs
⊢ ∀t x xs y h rest.
st_sorted t ⇒
st_get_cons (st_set_cons t x xs y) h rest =
if h = x ∧ rest = xs then SOME y else st_get_cons t h rest
⊢ ∀t y x xs. st_get_cons (st_set_nil t y) x xs = st_get_cons t x xs
⊢ (∀t. st_get t "" = st_get_nil t) ∧
(∀xs x t. st_get t (STRING x xs) = st_get_cons t x xs) ∧
(∀xs x. st_get_cons Nothing x xs = NONE) ∧
(∀xs x v0. st_get_cons (Just v0) x xs = NONE) ∧
∀xs x subtrie rest c.
st_get_cons (Branch c subtrie rest) x xs =
if char_gt c x then NONE
else if char_lt c x then st_get_cons rest x xs
else st_get subtrie xs
⊢ ∀P0 P1.
(∀t. P0 t "") ∧ (∀t x xs. P1 t x xs ⇒ P0 t (STRING x xs)) ∧
(∀x xs. P1 Nothing x xs) ∧ (∀v0 x xs. P1 (Just v0) x xs) ∧
(∀c subtrie rest x xs.
(¬char_gt c x ∧ ¬char_lt c x ⇒ P0 subtrie xs) ∧
(¬char_gt c x ∧ char_lt c x ⇒ P1 rest x xs) ⇒
P1 (Branch c subtrie rest) x xs) ⇒
(∀v0 v1. P0 v0 v1) ∧ ∀v0 v1 v2. P1 v0 v1 v2
⊢ ∀c t1 t2. st_get_nil (mk_Branch c t1 t2) = st_get_nil t2
⊢ ∀t x xs. st_get_nil (st_del_cons t x xs) = st_get_nil t
⊢ ∀t. st_get_nil (st_del_nil t) = NONE
⊢ ∀t u.
st_get_nil (st_inter t u) =
case st_get_nil u of NONE => NONE | SOME v => st_get_nil t
⊢ ∀xs y. st_get_nil (st_make xs y) = if xs = "" then SOME y else NONE
⊢ ∀t u.
st_get_nil (st_minus t u) =
case st_get_nil u of NONE => st_get_nil t | SOME v => NONE
⊢ ∀t x xs y. st_get_nil (st_set_cons t x xs y) = st_get_nil t
⊢ ∀t y. st_get_nil (st_set_nil t y) = SOME y
⊢ ∀t u.
st_get_nil (st_union t u) =
case st_get_nil t of NONE => st_get_nil u | SOME r => SOME r
⊢ ∀t k n.
st_sorted t ⇒
st_get (st_del t k) n = if n = k then NONE else st_get t n
⊢ ∀t1 t2 n.
st_sorted t1 ∧ st_sorted t2 ⇒
st_get (st_inter t1 t2) n =
case st_get t2 n of NONE => NONE | SOME v => st_get t1 n
⊢ ∀xs y n. st_get (st_make xs y) n = if n = xs then SOME y else NONE
⊢ ∀t1 t2 n.
st_sorted t1 ∧ st_sorted t2 ⇒
st_get (st_minus t1 t2) n =
case st_get t2 n of NONE => st_get t1 n | SOME v => NONE
⊢ ∀t k v n.
st_sorted t ⇒
st_get (st_set t k v) n = if n = k then SOME v else st_get t n
⊢ st_sorted t ⇒
st_get (st_sets t xs) n =
case ALOOKUP xs n of NONE => st_get t n | SOME v1 => SOME v1
⊢ ∀t1 t2 n.
st_sorted t1 ∧ st_sorted t2 ⇒
st_get (st_union t1 t2) n =
case st_get t1 n of NONE => st_get t2 n | SOME r => SOME r
⊢ (∀t. st_inter Nothing t = Nothing) ∧
(∀v2. st_inter (Just v2) Nothing = Nothing) ∧
(∀v5 v4 v3. st_inter (Branch v3 v4 v5) Nothing = Nothing) ∧
(∀y x. st_inter (Just x) (Just y) = Just x) ∧
(∀x t2 t1 c. st_inter (Just x) (Branch c t1 t2) = st_inter (Just x) t2) ∧
(∀x t2 t1 c. st_inter (Branch c t1 t2) (Just x) = st_inter t2 (Just x)) ∧
∀u2 u1 t2 t1 c2 c1.
st_inter (Branch c1 t1 t2) (Branch c2 u1 u2) =
if ORD c1 < ORD c2 then st_inter t2 (Branch c2 u1 u2)
else if ORD c2 < ORD c1 then st_inter (Branch c1 t1 t2) u2
else mk_Branch c1 (st_inter t1 u1) (st_inter t2 u2)
⊢ ∀P. (∀t. P Nothing t) ∧ (∀v2. P (Just v2) Nothing) ∧
(∀v3 v4 v5. P (Branch v3 v4 v5) Nothing) ∧
(∀x y. P (Just x) (Just y)) ∧
(∀x c t1 t2. P (Just x) t2 ⇒ P (Just x) (Branch c t1 t2)) ∧
(∀c t1 t2 x. P t2 (Just x) ⇒ P (Branch c t1 t2) (Just x)) ∧
(∀c1 t1 t2 c2 u1 u2.
(¬(ORD c1 < ORD c2) ∧ ¬(ORD c2 < ORD c1) ⇒ P t1 u1) ∧
(¬(ORD c1 < ORD c2) ∧ ¬(ORD c2 < ORD c1) ⇒ P t2 u2) ∧
(¬(ORD c1 < ORD c2) ∧ ORD c2 < ORD c1 ⇒ P (Branch c1 t1 t2) u2) ∧
(ORD c1 < ORD c2 ⇒ P t2 (Branch c2 u1 u2)) ⇒
P (Branch c1 t1 t2) (Branch c2 u1 u2)) ⇒
∀v v1. P v v1
⊢ (∀t rp acc.
st_lex_acc t rp acc =
case st_get_nil t of
NONE => st_branches_acc t rp acc
| SOME v => (REVERSE rp,v)::st_branches_acc t rp acc) ∧
(∀rp acc. st_branches_acc Nothing rp acc = acc) ∧
(∀x rp acc. st_branches_acc (Just x) rp acc = acc) ∧
∀t2 t1 rp c acc.
st_branches_acc (Branch c t1 t2) rp acc =
st_lex_acc t1 (STRING c rp) (st_branches_acc t2 rp acc)
⊢ ∀P0 P1.
(∀t rp acc.
(∀v. st_get_nil t = SOME v ⇒ P1 t rp acc) ∧
(st_get_nil t = NONE ⇒ P1 t rp acc) ⇒
P0 t rp acc) ∧ (∀rp acc. P1 Nothing rp acc) ∧
(∀x rp acc. P1 (Just x) rp acc) ∧
(∀c t1 t2 rp acc.
P0 t1 (STRING c rp) (st_branches_acc t2 rp acc) ∧ P1 t2 rp acc ⇒
P1 (Branch c t1 t2) rp acc) ⇒
(∀v0 v1 v2. P0 v0 v1 v2) ∧ ∀v0 v1 v2. P1 v0 v1 v2
⊢ (∀t rp acc. st_lex_acc_pre t rp acc) ∧
∀t rp acc. st_branches_acc_pre t rp acc
st_lex_acc_pre_cases
⊢ (∀a0 a1 a2.
st_lex_acc_pre a0 a1 a2 ⇔
∀v. v = st_get_nil a0 ⇒
(v = NONE ⇒ st_branches_acc_pre a0 a1 a2) ∧
∀v0. v = SOME v0 ⇒ st_branches_acc_pre a0 a1 a2) ∧
∀a3 a4 a5.
st_branches_acc_pre a3 a4 a5 ⇔
∀v0 v1 v2.
a3 = Branch v0 v1 v2 ⇒
st_branches_acc_pre v2 a4 a5 ∧
st_lex_acc_pre v1 (STRING v0 a4) (st_branches_acc v2 a4 a5)
st_lex_acc_pre_ind
⊢ ∀st_lex_acc_pre' st_branches_acc_pre'.
(∀t rp acc.
(∀v. v = st_get_nil t ⇒
(v = NONE ⇒ st_branches_acc_pre' t rp acc) ∧
∀v0. v = SOME v0 ⇒ st_branches_acc_pre' t rp acc) ⇒
st_lex_acc_pre' t rp acc) ∧
(∀v rp acc.
(∀v0 v1 v2.
v = Branch v0 v1 v2 ⇒
st_branches_acc_pre' v2 rp acc ∧
st_lex_acc_pre' v1 (STRING v0 rp) (st_branches_acc v2 rp acc)) ⇒
st_branches_acc_pre' v rp acc) ⇒
(∀a0 a1 a2. st_lex_acc_pre a0 a1 a2 ⇒ st_lex_acc_pre' a0 a1 a2) ∧
∀a3 a4 a5. st_branches_acc_pre a3 a4 a5 ⇒ st_branches_acc_pre' a3 a4 a5
st_lex_acc_pre_rules
⊢ (∀t rp acc.
(∀v. v = st_get_nil t ⇒
(v = NONE ⇒ st_branches_acc_pre t rp acc) ∧
∀v0. v = SOME v0 ⇒ st_branches_acc_pre t rp acc) ⇒
st_lex_acc_pre t rp acc) ∧
∀v rp acc.
(∀v0 v1 v2.
v = Branch v0 v1 v2 ⇒
st_branches_acc_pre v2 rp acc ∧
st_lex_acc_pre v1 (STRING v0 rp) (st_branches_acc v2 rp acc)) ⇒
st_branches_acc_pre v rp acc
st_lex_acc_pre_strongind
⊢ ∀st_lex_acc_pre' st_branches_acc_pre'.
(∀t rp acc.
(∀v. v = st_get_nil t ⇒
(v = NONE ⇒
st_branches_acc_pre t rp acc ∧ st_branches_acc_pre' t rp acc) ∧
∀v0.
v = SOME v0 ⇒
st_branches_acc_pre t rp acc ∧ st_branches_acc_pre' t rp acc) ⇒
st_lex_acc_pre' t rp acc) ∧
(∀v rp acc.
(∀v0 v1 v2.
v = Branch v0 v1 v2 ⇒
st_branches_acc_pre v2 rp acc ∧ st_branches_acc_pre' v2 rp acc ∧
st_lex_acc_pre v1 (STRING v0 rp) (st_branches_acc v2 rp acc) ∧
st_lex_acc_pre' v1 (STRING v0 rp) (st_branches_acc v2 rp acc)) ⇒
st_branches_acc_pre' v rp acc) ⇒
(∀a0 a1 a2. st_lex_acc_pre a0 a1 a2 ⇒ st_lex_acc_pre' a0 a1 a2) ∧
∀a3 a4 a5. st_branches_acc_pre a3 a4 a5 ⇒ st_branches_acc_pre' a3 a4 a5
⊢ (∀t. st_lex t =
case st_get_nil t of
NONE => st_branches t
| SOME v => ("",v)::st_branches t) ∧ st_branches Nothing = [] ∧
(∀x. st_branches (Just x) = []) ∧
∀t2 t1 c.
st_branches (Branch c t1 t2) =
MAP (λ(k,v). (STRING c k,v)) (st_lex t1) ⧺ st_branches t2
⊢ ∀P0 P1.
(∀t. (∀v. st_get_nil t = SOME v ⇒ P1 t) ∧ (st_get_nil t = NONE ⇒ P1 t) ⇒
P0 t) ∧ P1 Nothing ∧ (∀x. P1 (Just x)) ∧
(∀c t1 t2. P0 t1 ∧ P1 t2 ⇒ P1 (Branch c t1 t2)) ⇒
(∀v0. P0 v0) ∧ ∀v0. P1 v0
⊢ (∀t. st_minus Nothing t = Nothing) ∧
(∀v2. st_minus (Just v2) Nothing = Just v2) ∧
(∀v5 v4 v3. st_minus (Branch v3 v4 v5) Nothing = Branch v3 v4 v5) ∧
(∀y x. st_minus (Just x) (Just y) = Nothing) ∧
(∀x t2 t1 c. st_minus (Just x) (Branch c t1 t2) = st_minus (Just x) t2) ∧
(∀x t2 t1 c.
st_minus (Branch c t1 t2) (Just x) =
Branch c t1 (st_minus t2 (Just x))) ∧
∀u2 u1 t2 t1 c2 c1.
st_minus (Branch c1 t1 t2) (Branch c2 u1 u2) =
if ORD c1 < ORD c2 then Branch c1 t1 (st_minus t2 (Branch c2 u1 u2))
else if ORD c2 < ORD c1 then st_minus (Branch c1 t1 t2) u2
else mk_Branch c1 (st_minus t1 u1) (st_minus t2 u2)
⊢ ∀P. (∀t. P Nothing t) ∧ (∀v2. P (Just v2) Nothing) ∧
(∀v3 v4 v5. P (Branch v3 v4 v5) Nothing) ∧
(∀x y. P (Just x) (Just y)) ∧
(∀x c t1 t2. P (Just x) t2 ⇒ P (Just x) (Branch c t1 t2)) ∧
(∀c t1 t2 x. P t2 (Just x) ⇒ P (Branch c t1 t2) (Just x)) ∧
(∀c1 t1 t2 c2 u1 u2.
(¬(ORD c1 < ORD c2) ∧ ¬(ORD c2 < ORD c1) ⇒ P t1 u1) ∧
(¬(ORD c1 < ORD c2) ∧ ¬(ORD c2 < ORD c1) ⇒ P t2 u2) ∧
(¬(ORD c1 < ORD c2) ∧ ORD c2 < ORD c1 ⇒ P (Branch c1 t1 t2) u2) ∧
(ORD c1 < ORD c2 ⇒ P t2 (Branch c2 u1 u2)) ⇒
P (Branch c1 t1 t2) (Branch c2 u1 u2)) ⇒
∀v v1. P v v1
⊢ st_set_cons t x xs y ≠ Nothing
⊢ (∀y t rest c.
st_set_nil (Branch c t rest) y = Branch c t (st_set_nil rest y)) ∧
(∀y. st_set_nil Nothing y = Just y) ∧
∀y v2. st_set_nil (Just v2) y = Just y
⊢ ∀P. (∀c t rest y. P rest y ⇒ P (Branch c t rest) y) ∧ (∀y. P Nothing y) ∧
(∀v2 y. P (Just v2) y) ⇒
∀v v1. P v v1
⊢ st_set_nil t y ≠ Nothing
⊢ (∀t. st_sets t [] = t) ∧
∀t s rest a. st_sets t ((s,a)::rest) = st_set (st_sets t rest) s a
⊢ st_sorted t ⇒ ALOOKUP xs = ALOOKUP ys ⇒ st_sets t xs = st_sets t ys
⊢ ∀P. (∀t. P t []) ∧ (∀t s a rest. P t rest ⇒ P t ((s,a)::rest)) ⇒
∀v v1. P v v1
⊢ st_sorted Nothing ∧ st_sorted (Just x)
⊢ st_sorted (mk_Branch c t1 t2) ⇔
st_sorted t1 ∧ st_sorted t2 ∧
(t1 ≠ Nothing ⇒ ∀c' t1' t2'. t2 = Branch c' t1' t2' ⇒ char_lt c c')
⊢ ∀t. st_sorted t ∧ t ≠ Nothing ⇒ ∃k v. st_get t k = SOME v
⊢ ∀t k. st_sorted t ⇒ st_sorted (st_del t k)
⊢ ∀t x xs. st_sorted t ⇒ st_sorted (st_del_cons t x xs)
⊢ ∀t. st_sorted t ⇒ st_sorted (st_del_nil t)
⊢ ∀t1 t2.
st_sorted t1 ∧ st_sorted t2 ∧ (∀n. st_get t1 n = st_get t2 n) ⇒ t1 = t2
⊢ ∀t u. st_sorted t ∧ st_sorted u ⇒ st_sorted (st_inter t u)
⊢ ∀xs y. st_sorted (st_make xs y)
⊢ ∀t u. st_sorted t ∧ st_sorted u ⇒ st_sorted (st_minus t u)
⊢ st_sorted t ⇒ st_sorted (st_set t m x)
⊢ ∀t x xs y. st_sorted t ⇒ st_sorted (st_set_cons t x xs y)
⊢ ∀t y. st_sorted t ⇒ st_sorted (st_set_nil t y)
⊢ st_sorted t ⇒ st_sorted (st_sets t xs)
⊢ ∀t1 t2. st_sorted t1 ∧ st_sorted t2 ⇒ st_sorted (st_union t1 t2)
⊢ (∀u. st_submap Nothing u ⇔ T) ∧ (∀x. st_submap (Just x) Nothing ⇔ F) ∧
(∀t2 t1 c. st_submap (Branch c t1 t2) Nothing ⇔ F) ∧
(∀y x. st_submap (Just x) (Just y) ⇔ x = y) ∧
(∀x u2 u1 c. st_submap (Just x) (Branch c u1 u2) ⇔ st_submap (Just x) u2) ∧
(∀y t2 t1 c. st_submap (Branch c t1 t2) (Just y) ⇔ F) ∧
∀u2 u1 t2 t1 c2 c1.
st_submap (Branch c1 t1 t2) (Branch c2 u1 u2) ⇔
if ORD c1 < ORD c2 then F
else if ORD c2 < ORD c1 then st_submap (Branch c1 t1 t2) u2
else st_submap t1 u1 ∧ st_submap t2 u2
⊢ ∀P. (∀u. P Nothing u) ∧ (∀x. P (Just x) Nothing) ∧
(∀c t1 t2. P (Branch c t1 t2) Nothing) ∧
(∀x y. P (Just x) (Just y)) ∧
(∀x c u1 u2. P (Just x) u2 ⇒ P (Just x) (Branch c u1 u2)) ∧
(∀c t1 t2 y. P (Branch c t1 t2) (Just y)) ∧
(∀c1 t1 t2 c2 u1 u2.
(¬(ORD c1 < ORD c2) ∧ ¬(ORD c2 < ORD c1) ⇒ P t1 u1) ∧
(¬(ORD c1 < ORD c2) ∧ ¬(ORD c2 < ORD c1) ⇒ P t2 u2) ∧
(¬(ORD c1 < ORD c2) ∧ ORD c2 < ORD c1 ⇒ P (Branch c1 t1 t2) u2) ⇒
P (Branch c1 t1 t2) (Branch c2 u1 u2)) ⇒
∀v v1. P v v1
⊢ ∀t u.
st_sorted t ∧ st_sorted u ⇒
(st_submap t u ⇔ ∀k v. st_get t k = SOME v ⇒ st_get u k = SOME v)
⊢ st_to_list t = st_lex t
⊢ ∀t u c t1 t2.
st_union t u = Branch c t1 t2 ⇒
(∃x y. t = Branch c x y) ∨ ∃x y. u = Branch c x y
⊢ (∀t. st_union Nothing t = t) ∧
(∀v2. st_union (Just v2) Nothing = Just v2) ∧
(∀v5 v4 v3. st_union (Branch v3 v4 v5) Nothing = Branch v3 v4 v5) ∧
(∀y x. st_union (Just x) (Just y) = Just x) ∧
(∀x t2 t1 c.
st_union (Just x) (Branch c t1 t2) =
Branch c t1 (st_union (Just x) t2)) ∧
(∀x t2 t1 c.
st_union (Branch c t1 t2) (Just x) =
Branch c t1 (st_union t2 (Just x))) ∧
∀u2 u1 t2 t1 c2 c1.
st_union (Branch c1 t1 t2) (Branch c2 u1 u2) =
if ORD c1 < ORD c2 then Branch c1 t1 (st_union t2 (Branch c2 u1 u2))
else if ORD c2 < ORD c1 then
Branch c2 u1 (st_union (Branch c1 t1 t2) u2)
else Branch c1 (st_union t1 u1) (st_union t2 u2)
⊢ st_union t u = Nothing ⇔ t = Nothing ∧ u = Nothing
⊢ ∀P. (∀t. P Nothing t) ∧ (∀v2. P (Just v2) Nothing) ∧
(∀v3 v4 v5. P (Branch v3 v4 v5) Nothing) ∧
(∀x y. P (Just x) (Just y)) ∧
(∀x c t1 t2. P (Just x) t2 ⇒ P (Just x) (Branch c t1 t2)) ∧
(∀c t1 t2 x. P t2 (Just x) ⇒ P (Branch c t1 t2) (Just x)) ∧
(∀c1 t1 t2 c2 u1 u2.
(¬(ORD c1 < ORD c2) ∧ ¬(ORD c2 < ORD c1) ⇒ P t1 u1) ∧
(¬(ORD c1 < ORD c2) ∧ ¬(ORD c2 < ORD c1) ⇒ P t2 u2) ∧
(¬(ORD c1 < ORD c2) ∧ ORD c2 < ORD c1 ⇒ P (Branch c1 t1 t2) u2) ∧
(ORD c1 < ORD c2 ⇒ P t2 (Branch c2 u1 u2)) ⇒
P (Branch c1 t1 t2) (Branch c2 u1 u2)) ⇒
∀v v1. P v v1
str_trie_11
⊢ (∀a a'. Just a = Just a' ⇔ a = a') ∧
∀a0 a1 a2 a0' a1' a2'.
Branch a0 a1 a2 = Branch a0' a1' a2' ⇔ a0 = a0' ∧ a1 = a1' ∧ a2 = a2'
str_trie_Axiom
⊢ ∀f0 f1 f2. ∃fn.
fn Nothing = f0 ∧ (∀a. fn (Just a) = f1 a) ∧
∀a0 a1 a2. fn (Branch a0 a1 a2) = f2 a0 a1 a2 (fn a1) (fn a2)
str_trie_case_cong
⊢ ∀M M' v f f1.
M = M' ∧ (M' = Nothing ⇒ v = v') ∧ (∀a. M' = Just a ⇒ f a = f' a) ∧
(∀a0 a1 a2. M' = Branch a0 a1 a2 ⇒ f1 a0 a1 a2 = f1' a0 a1 a2) ⇒
str_trie_CASE M v f f1 = str_trie_CASE M' v' f' f1'
str_trie_case_eq
⊢ str_trie_CASE x v f f1 = v' ⇔
x = Nothing ∧ v = v' ∨ (∃a. x = Just a ∧ f a = v') ∨
∃c s s0. x = Branch c s s0 ∧ f1 c s s0 = v'
str_trie_distinct
⊢ (∀a. Nothing ≠ Just a) ∧ (∀a2 a1 a0. Nothing ≠ Branch a0 a1 a2) ∧
∀a2 a1 a0 a. Just a ≠ Branch a0 a1 a2
str_trie_induction
⊢ ∀P. P Nothing ∧ (∀a. P (Just a)) ∧
(∀s s0. P s ∧ P s0 ⇒ ∀c. P (Branch c s s0)) ⇒
∀s. P s
str_trie_nchotomy
⊢ ∀ss. ss = Nothing ∨ (∃a. ss = Just a) ∨ ∃c s s0. ss = Branch c s s0
to_str_trie_def
⊢ to_str_trie t0 v =
if cv_has_shape [SOME 2; NONE; NONE] v then
Branch (to_char (cv_fst (cv_snd v)))
(to_str_trie t0 (cv_fst (cv_snd (cv_snd v))))
(to_str_trie t0 (cv_snd (cv_snd (cv_snd v))))
else if v = Num 0 then Nothing
else Just (t0 (cv_snd v))