- index_TY_DEF
-
|- ∃rep.
TYPE_DEFINITION
(λa0.
∀'index' .
(∀a0.
(∃a.
(a0 =
(λa.
ind_type$CONSTR 0 ARB
(ind_type$FCONS a (λn. ind_type$BOTTOM))) a) ∧
'index' a) ∨
(∃a.
(a0 =
(λa.
ind_type$CONSTR (SUC 0) ARB
(ind_type$FCONS a (λn. ind_type$BOTTOM))) a) ∧
'index' a) ∨
(a0 =
ind_type$CONSTR (SUC (SUC 0)) ARB (λn. ind_type$BOTTOM)) ⇒
'index' a0) ⇒
'index' a0) rep
- index_case_def
-
|- (∀a f f1 v. index_CASE (Left_idx a) f f1 v = f a) ∧
(∀a f f1 v. index_CASE (Right_idx a) f f1 v = f1 a) ∧
∀f f1 v. index_CASE End_idx f f1 v = v
- index_size_def
-
|- (∀a. index_size (Left_idx a) = 1 + index_size a) ∧
(∀a. index_size (Right_idx a) = 1 + index_size a) ∧
(index_size End_idx = 0)
- index_compare_tupled_primitive_def
-
|- index_compare_tupled =
WFREC
(@R.
WF R ∧ (∀m' n'. R (n',m') (Left_idx n',Left_idx m')) ∧
∀m' n'. R (n',m') (Right_idx n',Right_idx m'))
(λindex_compare_tupled a.
case a of
(Left_idx n',Left_idx m') => I (index_compare_tupled (n',m'))
| (Left_idx n',Right_idx m'') => I LESS
| (Left_idx n',End_idx) => I GREATER
| (Right_idx n'',Left_idx m'''') => I GREATER
| (Right_idx n'',Right_idx m''') =>
I (index_compare_tupled (n'',m'''))
| (Right_idx n'',End_idx) => I GREATER
| (End_idx,Left_idx v12) => I LESS
| (End_idx,Right_idx v13) => I LESS
| (End_idx,End_idx) => I EQUAL)
- index_compare_curried_def
-
|- ∀x x1. index_compare x x1 = index_compare_tupled (x,x1)
- index_lt_def
-
|- ∀i1 i2. index_lt i1 i2 ⇔ (index_compare i1 i2 = LESS)
- varmap_TY_DEF
-
|- ∃rep.
TYPE_DEFINITION
(λa0'.
∀'varmap' .
(∀a0'.
(a0' = ind_type$CONSTR 0 ARB (λn. ind_type$BOTTOM)) ∨
(∃a0 a1 a2.
(a0' =
(λa0 a1 a2.
ind_type$CONSTR (SUC 0) a0
(ind_type$FCONS a1
(ind_type$FCONS a2 (λn. ind_type$BOTTOM)))) a0 a1
a2) ∧ 'varmap' a1 ∧ 'varmap' a2) ⇒
'varmap' a0') ⇒
'varmap' a0') rep
- varmap_case_def
-
|- (∀v f. varmap_CASE Empty_vm v f = v) ∧
∀a0 a1 a2 v f. varmap_CASE (Node_vm a0 a1 a2) v f = f a0 a1 a2
- varmap_size_def
-
|- (∀f. varmap_size f Empty_vm = 0) ∧
∀f a0 a1 a2.
varmap_size f (Node_vm a0 a1 a2) =
1 + (f a0 + (varmap_size f a1 + varmap_size f a2))
- varmap_find_tupled_primitive_def
-
|- varmap_find_tupled =
WFREC
(@R.
WF R ∧ (∀v1 x v2 i1. R (i1,v2) (Right_idx i1,Node_vm x v1 v2)) ∧
∀v2 x v1 i1. R (i1,v1) (Left_idx i1,Node_vm x v1 v2))
(λvarmap_find_tupled a.
case a of
(v3,Empty_vm) => I (@x. T)
| (Left_idx i1',Node_vm x v1 v2) => I (varmap_find_tupled (i1',v1))
| (Right_idx i1,Node_vm x v1 v2) => I (varmap_find_tupled (i1,v2))
| (End_idx,Node_vm x v1 v2) => I x)
- varmap_find_curried_def
-
|- ∀x x1. varmap_find x x1 = varmap_find_tupled (x,x1)
- datatype_index
-
|- DATATYPE (index Left_idx Right_idx End_idx)
- index_11
-
|- (∀a a'. (Left_idx a = Left_idx a') ⇔ (a = a')) ∧
∀a a'. (Right_idx a = Right_idx a') ⇔ (a = a')
- index_distinct
-
|- (∀a' a. Left_idx a ≠ Right_idx a') ∧ (∀a. Left_idx a ≠ End_idx) ∧
∀a. Right_idx a ≠ End_idx
- index_case_cong
-
|- ∀M M' f f1 v.
(M = M') ∧ (∀a. (M' = Left_idx a) ⇒ (f a = f' a)) ∧
(∀a. (M' = Right_idx a) ⇒ (f1 a = f1' a)) ∧ ((M' = End_idx) ⇒ (v = v')) ⇒
(index_CASE M f f1 v = index_CASE M' f' f1' v')
- index_nchotomy
-
|- ∀ii. (∃i. ii = Left_idx i) ∨ (∃i. ii = Right_idx i) ∨ (ii = End_idx)
- index_Axiom
-
|- ∀f0 f1 f2.
∃fn.
(∀a. fn (Left_idx a) = f0 a (fn a)) ∧
(∀a. fn (Right_idx a) = f1 a (fn a)) ∧ (fn End_idx = f2)
- index_induction
-
|- ∀P.
(∀i. P i ⇒ P (Left_idx i)) ∧ (∀i. P i ⇒ P (Right_idx i)) ∧ P End_idx ⇒
∀i. P i
- index_compare_ind
-
|- ∀P.
P End_idx End_idx ∧ (∀v10. P End_idx (Left_idx v10)) ∧
(∀v11. P End_idx (Right_idx v11)) ∧ (∀v2. P (Left_idx v2) End_idx) ∧
(∀v3. P (Right_idx v3) End_idx) ∧
(∀n' m'. P n' m' ⇒ P (Left_idx n') (Left_idx m')) ∧
(∀n' m'. P (Left_idx n') (Right_idx m')) ∧
(∀n' m'. P n' m' ⇒ P (Right_idx n') (Right_idx m')) ∧
(∀n' m'. P (Right_idx n') (Left_idx m')) ⇒
∀v v1. P v v1
- index_compare_def
-
|- (index_compare End_idx End_idx = EQUAL) ∧
(∀v10. index_compare End_idx (Left_idx v10) = LESS) ∧
(∀v11. index_compare End_idx (Right_idx v11) = LESS) ∧
(∀v2. index_compare (Left_idx v2) End_idx = GREATER) ∧
(∀v3. index_compare (Right_idx v3) End_idx = GREATER) ∧
(∀n' m'. index_compare (Left_idx n') (Left_idx m') = index_compare n' m') ∧
(∀n' m'. index_compare (Left_idx n') (Right_idx m') = LESS) ∧
(∀n' m'.
index_compare (Right_idx n') (Right_idx m') = index_compare n' m') ∧
∀n' m'. index_compare (Right_idx n') (Left_idx m') = GREATER
- compare_index_equal
-
|- ∀i1 i2. (index_compare i1 i2 = EQUAL) ⇔ (i1 = i2)
- compare_list_index
-
|- ∀l1 l2. (list_compare index_compare l1 l2 = EQUAL) ⇔ (l1 = l2)
- datatype_varmap
-
|- DATATYPE (varmap Empty_vm Node_vm)
- varmap_11
-
|- ∀a0 a1 a2 a0' a1' a2'.
(Node_vm a0 a1 a2 = Node_vm a0' a1' a2') ⇔
(a0 = a0') ∧ (a1 = a1') ∧ (a2 = a2')
- varmap_distinct
-
|- ∀a2 a1 a0. Empty_vm ≠ Node_vm a0 a1 a2
- varmap_case_cong
-
|- ∀M M' v f.
(M = M') ∧ ((M' = Empty_vm) ⇒ (v = v')) ∧
(∀a0 a1 a2. (M' = Node_vm a0 a1 a2) ⇒ (f a0 a1 a2 = f' a0 a1 a2)) ⇒
(varmap_CASE M v f = varmap_CASE M' v' f')
- varmap_nchotomy
-
|- ∀vv. (vv = Empty_vm) ∨ ∃a v v0. vv = Node_vm a v v0
- varmap_Axiom
-
|- ∀f0 f1.
∃fn.
(fn Empty_vm = f0) ∧
∀a0 a1 a2. fn (Node_vm a0 a1 a2) = f1 a0 a1 a2 (fn a1) (fn a2)
- varmap_induction
-
|- ∀P. P Empty_vm ∧ (∀v v0. P v ∧ P v0 ⇒ ∀a. P (Node_vm a v v0)) ⇒ ∀v. P v
- varmap_find_ind
-
|- ∀P.
(∀x v1 v2. P End_idx (Node_vm x v1 v2)) ∧
(∀i1 x v1 v2. P i1 v2 ⇒ P (Right_idx i1) (Node_vm x v1 v2)) ∧
(∀i1 x v1 v2. P i1 v1 ⇒ P (Left_idx i1) (Node_vm x v1 v2)) ∧
(∀i. P i Empty_vm) ⇒
∀v v1. P v v1
- varmap_find_def
-
|- (∀x v2 v1. varmap_find End_idx (Node_vm x v1 v2) = x) ∧
(∀x v2 v1 i1.
varmap_find (Right_idx i1) (Node_vm x v1 v2) = varmap_find i1 v2) ∧
(∀x v2 v1 i1.
varmap_find (Left_idx i1) (Node_vm x v1 v2) = varmap_find i1 v1) ∧
∀i. varmap_find i Empty_vm = @x. T