- canonical_sum_TY_DEF
-
|- ∃rep.
TYPE_DEFINITION
(λa0'.
∀'canonical_sum' .
(∀a0'.
(a0' = ind_type$CONSTR 0 (ARB,ARB) (λn. ind_type$BOTTOM)) ∨
(∃a0 a1 a2.
(a0' =
(λa0 a1 a2.
ind_type$CONSTR (SUC 0) (a0,a1)
(ind_type$FCONS a2 (λn. ind_type$BOTTOM))) a0 a1 a2) ∧
'canonical_sum' a2) ∨
(∃a0 a1.
(a0' =
(λa0 a1.
ind_type$CONSTR (SUC (SUC 0)) (ARB,a0)
(ind_type$FCONS a1 (λn. ind_type$BOTTOM))) a0 a1) ∧
'canonical_sum' a1) ⇒
'canonical_sum' a0') ⇒
'canonical_sum' a0') rep
- canonical_sum_case_def
-
|- (∀v f f1. canonical_sum_CASE Nil_monom v f f1 = v) ∧
(∀a0 a1 a2 v f f1.
canonical_sum_CASE (Cons_monom a0 a1 a2) v f f1 = f a0 a1 a2) ∧
∀a0 a1 v f f1. canonical_sum_CASE (Cons_varlist a0 a1) v f f1 = f1 a0 a1
- canonical_sum_size_def
-
|- (∀f. canonical_sum_size f Nil_monom = 0) ∧
(∀f a0 a1 a2.
canonical_sum_size f (Cons_monom a0 a1 a2) =
1 + (f a0 + (list_size index_size a1 + canonical_sum_size f a2))) ∧
∀f a0 a1.
canonical_sum_size f (Cons_varlist a0 a1) =
1 + (list_size index_size a0 + canonical_sum_size f a1)
- canonical_sum_merge_tupled_primitive_def
-
|- canonical_sum_merge_tupled =
WFREC
(@R.
WF R ∧
(∀l2 c2 t2 t1 l1 c1 sr.
R (sr,Cons_monom c1 l1 t1,t2)
(sr,Cons_monom c1 l1 t1,Cons_monom c2 l2 t2)) ∧
(∀l1 c1 t2 l2 c2 t1 sr.
R (sr,t1,Cons_monom c2 l2 t2)
(sr,Cons_monom c1 l1 t1,Cons_monom c2 l2 t2)) ∧
(∀l2 c2 l1 c1 t2 t1 sr.
R (sr,t1,t2) (sr,Cons_monom c1 l1 t1,Cons_monom c2 l2 t2)) ∧
(∀l2 t2 t1 l1 c1 sr.
R (sr,Cons_monom c1 l1 t1,t2)
(sr,Cons_monom c1 l1 t1,Cons_varlist l2 t2)) ∧
(∀l1 c1 t2 l2 t1 sr.
R (sr,t1,Cons_varlist l2 t2)
(sr,Cons_monom c1 l1 t1,Cons_varlist l2 t2)) ∧
(∀l2 l1 c1 t2 t1 sr.
R (sr,t1,t2) (sr,Cons_monom c1 l1 t1,Cons_varlist l2 t2)) ∧
(∀l2 c2 t2 t1 l1 sr.
R (sr,Cons_varlist l1 t1,t2)
(sr,Cons_varlist l1 t1,Cons_monom c2 l2 t2)) ∧
(∀l1 t2 l2 c2 t1 sr.
R (sr,t1,Cons_monom c2 l2 t2)
(sr,Cons_varlist l1 t1,Cons_monom c2 l2 t2)) ∧
(∀l2 c2 l1 t2 t1 sr.
R (sr,t1,t2) (sr,Cons_varlist l1 t1,Cons_monom c2 l2 t2)) ∧
(∀l2 l1 t2 t1 sr.
R (sr,t1,t2) (sr,Cons_varlist l1 t1,Cons_varlist l2 t2)) ∧
(∀l1 t2 l2 t1 sr.
R (sr,t1,Cons_varlist l2 t2)
(sr,Cons_varlist l1 t1,Cons_varlist l2 t2)) ∧
∀l2 t2 t1 l1 sr.
R (sr,Cons_varlist l1 t1,t2)
(sr,Cons_varlist l1 t1,Cons_varlist l2 t2))
(λcanonical_sum_merge_tupled a.
case a of
(sr,s1,Nil_monom) => I s1
| (sr,Nil_monom,Cons_monom c2 l2 t2) => I (Cons_monom c2 l2 t2)
| (sr,Cons_monom c1 l1 t1,Cons_monom c2 l2 t2) =>
I
(compare (list_compare index_compare l1 l2)
(Cons_monom c1 l1
(canonical_sum_merge_tupled (sr,t1,Cons_monom c2 l2 t2)))
(Cons_monom (SRP sr c1 c2) l1
(canonical_sum_merge_tupled (sr,t1,t2)))
(Cons_monom c2 l2
(canonical_sum_merge_tupled (sr,Cons_monom c1 l1 t1,t2))))
| (sr,Cons_varlist l1'' t1'',Cons_monom c2 l2 t2) =>
I
(compare (list_compare index_compare l1'' l2)
(Cons_varlist l1''
(canonical_sum_merge_tupled
(sr,t1'',Cons_monom c2 l2 t2)))
(Cons_monom (SRP sr (SR1 sr) c2) l1''
(canonical_sum_merge_tupled (sr,t1'',t2)))
(Cons_monom c2 l2
(canonical_sum_merge_tupled
(sr,Cons_varlist l1'' t1'',t2))))
| (sr,Nil_monom,Cons_varlist l2' t2') => I (Cons_varlist l2' t2')
| (sr,Cons_monom c1' l1' t1',Cons_varlist l2' t2') =>
I
(compare (list_compare index_compare l1' l2')
(Cons_monom c1' l1'
(canonical_sum_merge_tupled
(sr,t1',Cons_varlist l2' t2')))
(Cons_monom (SRP sr c1' (SR1 sr)) l1'
(canonical_sum_merge_tupled (sr,t1',t2')))
(Cons_varlist l2'
(canonical_sum_merge_tupled
(sr,Cons_monom c1' l1' t1',t2'))))
| (sr,Cons_varlist l1''' t1''',Cons_varlist l2' t2') =>
I
(compare (list_compare index_compare l1''' l2')
(Cons_varlist l1'''
(canonical_sum_merge_tupled
(sr,t1''',Cons_varlist l2' t2')))
(Cons_monom (SRP sr (SR1 sr) (SR1 sr)) l1'''
(canonical_sum_merge_tupled (sr,t1''',t2')))
(Cons_varlist l2'
(canonical_sum_merge_tupled
(sr,Cons_varlist l1''' t1''',t2')))))
- canonical_sum_merge_curried_def
-
|- ∀x x1 x2.
canonical_sum_merge x x1 x2 = canonical_sum_merge_tupled (x,x1,x2)
- monom_insert_tupled_primitive_def
-
|- monom_insert_tupled =
WFREC
(@R.
WF R ∧
(∀l2 c2 t2 l1 c1 sr. R (sr,c1,l1,t2) (sr,c1,l1,Cons_monom c2 l2 t2)) ∧
∀l2 t2 l1 c1 sr. R (sr,c1,l1,t2) (sr,c1,l1,Cons_varlist l2 t2))
(λmonom_insert_tupled a.
case a of
(sr,c1,l1,Nil_monom) => I (Cons_monom c1 l1 Nil_monom)
| (sr,c1,l1,Cons_monom c2 l2 t2) =>
I
(compare (list_compare index_compare l1 l2)
(Cons_monom c1 l1 (Cons_monom c2 l2 t2))
(Cons_monom (SRP sr c1 c2) l1 t2)
(Cons_monom c2 l2 (monom_insert_tupled (sr,c1,l1,t2))))
| (sr,c1,l1,Cons_varlist l2' t2') =>
I
(compare (list_compare index_compare l1 l2')
(Cons_monom c1 l1 (Cons_varlist l2' t2'))
(Cons_monom (SRP sr c1 (SR1 sr)) l1 t2')
(Cons_varlist l2' (monom_insert_tupled (sr,c1,l1,t2')))))
- monom_insert_curried_def
-
|- ∀x x1 x2 x3. monom_insert x x1 x2 x3 = monom_insert_tupled (x,x1,x2,x3)
- varlist_insert_tupled_primitive_def
-
|- varlist_insert_tupled =
WFREC
(@R.
WF R ∧ (∀l2 c2 t2 l1 sr. R (sr,l1,t2) (sr,l1,Cons_monom c2 l2 t2)) ∧
∀l2 t2 l1 sr. R (sr,l1,t2) (sr,l1,Cons_varlist l2 t2))
(λvarlist_insert_tupled a.
case a of
(sr,l1,Nil_monom) => I (Cons_varlist l1 Nil_monom)
| (sr,l1,Cons_monom c2 l2 t2) =>
I
(compare (list_compare index_compare l1 l2)
(Cons_varlist l1 (Cons_monom c2 l2 t2))
(Cons_monom (SRP sr (SR1 sr) c2) l1 t2)
(Cons_monom c2 l2 (varlist_insert_tupled (sr,l1,t2))))
| (sr,l1,Cons_varlist l2' t2') =>
I
(compare (list_compare index_compare l1 l2')
(Cons_varlist l1 (Cons_varlist l2' t2'))
(Cons_monom (SRP sr (SR1 sr) (SR1 sr)) l1 t2')
(Cons_varlist l2' (varlist_insert_tupled (sr,l1,t2')))))
- varlist_insert_curried_def
-
|- ∀x x1 x2. varlist_insert x x1 x2 = varlist_insert_tupled (x,x1,x2)
- canonical_sum_scalar_def
-
|- (∀sr c0 c l t.
canonical_sum_scalar sr c0 (Cons_monom c l t) =
Cons_monom (SRM sr c0 c) l (canonical_sum_scalar sr c0 t)) ∧
(∀sr c0 l t.
canonical_sum_scalar sr c0 (Cons_varlist l t) =
Cons_monom c0 l (canonical_sum_scalar sr c0 t)) ∧
∀sr c0. canonical_sum_scalar sr c0 Nil_monom = Nil_monom
- canonical_sum_scalar2_def
-
|- (∀sr l0 c l t.
canonical_sum_scalar2 sr l0 (Cons_monom c l t) =
monom_insert sr c (list_merge index_lt l0 l)
(canonical_sum_scalar2 sr l0 t)) ∧
(∀sr l0 l t.
canonical_sum_scalar2 sr l0 (Cons_varlist l t) =
varlist_insert sr (list_merge index_lt l0 l)
(canonical_sum_scalar2 sr l0 t)) ∧
∀sr l0. canonical_sum_scalar2 sr l0 Nil_monom = Nil_monom
- canonical_sum_scalar3_def
-
|- (∀sr c0 l0 c l t.
canonical_sum_scalar3 sr c0 l0 (Cons_monom c l t) =
monom_insert sr (SRM sr c0 c) (list_merge index_lt l0 l)
(canonical_sum_scalar3 sr c0 l0 t)) ∧
(∀sr c0 l0 l t.
canonical_sum_scalar3 sr c0 l0 (Cons_varlist l t) =
monom_insert sr c0 (list_merge index_lt l0 l)
(canonical_sum_scalar3 sr c0 l0 t)) ∧
∀sr c0 l0. canonical_sum_scalar3 sr c0 l0 Nil_monom = Nil_monom
- canonical_sum_prod_def
-
|- (∀sr c1 l1 t1 s2.
canonical_sum_prod sr (Cons_monom c1 l1 t1) s2 =
canonical_sum_merge sr (canonical_sum_scalar3 sr c1 l1 s2)
(canonical_sum_prod sr t1 s2)) ∧
(∀sr l1 t1 s2.
canonical_sum_prod sr (Cons_varlist l1 t1) s2 =
canonical_sum_merge sr (canonical_sum_scalar2 sr l1 s2)
(canonical_sum_prod sr t1 s2)) ∧
∀sr s2. canonical_sum_prod sr Nil_monom s2 = Nil_monom
- canonical_sum_simplify_def
-
|- (∀sr c l t.
canonical_sum_simplify sr (Cons_monom c l t) =
if c = SR0 sr then canonical_sum_simplify sr t
else if c = SR1 sr then Cons_varlist l (canonical_sum_simplify sr t)
else Cons_monom c l (canonical_sum_simplify sr t)) ∧
(∀sr l t.
canonical_sum_simplify sr (Cons_varlist l t) =
Cons_varlist l (canonical_sum_simplify sr t)) ∧
∀sr. canonical_sum_simplify sr Nil_monom = Nil_monom
- ivl_aux_def
-
|- (∀sr vm x. ivl_aux sr vm x [] = varmap_find x vm) ∧
∀sr vm x x' t'.
ivl_aux sr vm x (x'::t') =
SRM sr (varmap_find x vm) (ivl_aux sr vm x' t')
- interp_vl_def
-
|- (∀sr vm. interp_vl sr vm [] = SR1 sr) ∧
∀sr vm x t. interp_vl sr vm (x::t) = ivl_aux sr vm x t
- interp_m_def
-
|- (∀sr vm c. interp_m sr vm c [] = c) ∧
∀sr vm c x t. interp_m sr vm c (x::t) = SRM sr c (ivl_aux sr vm x t)
- ics_aux_def
-
|- (∀sr vm a. ics_aux sr vm a Nil_monom = a) ∧
(∀sr vm a l t.
ics_aux sr vm a (Cons_varlist l t) =
SRP sr a (ics_aux sr vm (interp_vl sr vm l) t)) ∧
∀sr vm a c l t.
ics_aux sr vm a (Cons_monom c l t) =
SRP sr a (ics_aux sr vm (interp_m sr vm c l) t)
- interp_cs_def
-
|- (∀sr vm. interp_cs sr vm Nil_monom = SR0 sr) ∧
(∀sr vm l t.
interp_cs sr vm (Cons_varlist l t) =
ics_aux sr vm (interp_vl sr vm l) t) ∧
∀sr vm c l t.
interp_cs sr vm (Cons_monom c l t) = ics_aux sr vm (interp_m sr vm c l) t
- spolynom_TY_DEF
-
|- ∃rep.
TYPE_DEFINITION
(λa0'.
∀'spolynom' .
(∀a0'.
(∃a.
a0' =
(λa. ind_type$CONSTR 0 (a,ARB) (λn. ind_type$BOTTOM)) a) ∨
(∃a.
a0' =
(λa. ind_type$CONSTR (SUC 0) (ARB,a) (λn. ind_type$BOTTOM))
a) ∨
(∃a0 a1.
(a0' =
(λa0 a1.
ind_type$CONSTR (SUC (SUC 0)) (ARB,ARB)
(ind_type$FCONS a0
(ind_type$FCONS a1 (λn. ind_type$BOTTOM)))) a0
a1) ∧ 'spolynom' a0 ∧ 'spolynom' a1) ∨
(∃a0 a1.
(a0' =
(λa0 a1.
ind_type$CONSTR (SUC (SUC (SUC 0))) (ARB,ARB)
(ind_type$FCONS a0
(ind_type$FCONS a1 (λn. ind_type$BOTTOM)))) a0
a1) ∧ 'spolynom' a0 ∧ 'spolynom' a1) ⇒
'spolynom' a0') ⇒
'spolynom' a0') rep
- spolynom_case_def
-
|- (∀a f f1 f2 f3. spolynom_CASE (SPvar a) f f1 f2 f3 = f a) ∧
(∀a f f1 f2 f3. spolynom_CASE (SPconst a) f f1 f2 f3 = f1 a) ∧
(∀a0 a1 f f1 f2 f3. spolynom_CASE (SPplus a0 a1) f f1 f2 f3 = f2 a0 a1) ∧
∀a0 a1 f f1 f2 f3. spolynom_CASE (SPmult a0 a1) f f1 f2 f3 = f3 a0 a1
- spolynom_size_def
-
|- (∀f a. spolynom_size f (SPvar a) = 1 + index_size a) ∧
(∀f a. spolynom_size f (SPconst a) = 1 + f a) ∧
(∀f a0 a1.
spolynom_size f (SPplus a0 a1) =
1 + (spolynom_size f a0 + spolynom_size f a1)) ∧
∀f a0 a1.
spolynom_size f (SPmult a0 a1) =
1 + (spolynom_size f a0 + spolynom_size f a1)
- spolynom_normalize_def
-
|- (∀sr i. spolynom_normalize sr (SPvar i) = Cons_varlist [i] Nil_monom) ∧
(∀sr c. spolynom_normalize sr (SPconst c) = Cons_monom c [] Nil_monom) ∧
(∀sr l r.
spolynom_normalize sr (SPplus l r) =
canonical_sum_merge sr (spolynom_normalize sr l)
(spolynom_normalize sr r)) ∧
∀sr l r.
spolynom_normalize sr (SPmult l r) =
canonical_sum_prod sr (spolynom_normalize sr l) (spolynom_normalize sr r)
- spolynom_simplify_def
-
|- ∀sr x.
spolynom_simplify sr x =
canonical_sum_simplify sr (spolynom_normalize sr x)
- interp_sp_def
-
|- (∀sr vm c. interp_sp sr vm (SPconst c) = c) ∧
(∀sr vm i. interp_sp sr vm (SPvar i) = varmap_find i vm) ∧
(∀sr vm p1 p2.
interp_sp sr vm (SPplus p1 p2) =
SRP sr (interp_sp sr vm p1) (interp_sp sr vm p2)) ∧
∀sr vm p1 p2.
interp_sp sr vm (SPmult p1 p2) =
SRM sr (interp_sp sr vm p1) (interp_sp sr vm p2)
- datatype_canonical_sum
-
|- DATATYPE (canonical_sum Nil_monom Cons_monom Cons_varlist)
- canonical_sum_11
-
|- (∀a0 a1 a2 a0' a1' a2'.
(Cons_monom a0 a1 a2 = Cons_monom a0' a1' a2') ⇔
(a0 = a0') ∧ (a1 = a1') ∧ (a2 = a2')) ∧
∀a0 a1 a0' a1'.
(Cons_varlist a0 a1 = Cons_varlist a0' a1') ⇔ (a0 = a0') ∧ (a1 = a1')
- canonical_sum_distinct
-
|- (∀a2 a1 a0. Nil_monom ≠ Cons_monom a0 a1 a2) ∧
(∀a1 a0. Nil_monom ≠ Cons_varlist a0 a1) ∧
∀a2 a1' a1 a0' a0. Cons_monom a0 a1 a2 ≠ Cons_varlist a0' a1'
- canonical_sum_case_cong
-
|- ∀M M' v f f1.
(M = M') ∧ ((M' = Nil_monom) ⇒ (v = v')) ∧
(∀a0 a1 a2. (M' = Cons_monom a0 a1 a2) ⇒ (f a0 a1 a2 = f' a0 a1 a2)) ∧
(∀a0 a1. (M' = Cons_varlist a0 a1) ⇒ (f1 a0 a1 = f1' a0 a1)) ⇒
(canonical_sum_CASE M v f f1 = canonical_sum_CASE M' v' f' f1')
- canonical_sum_nchotomy
-
|- ∀cc.
(cc = Nil_monom) ∨ (∃a l c. cc = Cons_monom a l c) ∨
∃l c. cc = Cons_varlist l c
- canonical_sum_Axiom
-
|- ∀f0 f1 f2.
∃fn.
(fn Nil_monom = f0) ∧
(∀a0 a1 a2. fn (Cons_monom a0 a1 a2) = f1 a0 a1 a2 (fn a2)) ∧
∀a0 a1. fn (Cons_varlist a0 a1) = f2 a0 a1 (fn a1)
- canonical_sum_induction
-
|- ∀P.
P Nil_monom ∧ (∀c. P c ⇒ ∀l a. P (Cons_monom a l c)) ∧
(∀c. P c ⇒ ∀l. P (Cons_varlist l c)) ⇒
∀c. P c
- canonical_sum_merge_ind
-
|- ∀P.
(∀sr c1 l1 t1 c2 l2 t2.
P sr t1 t2 ∧ P sr t1 (Cons_monom c2 l2 t2) ∧
P sr (Cons_monom c1 l1 t1) t2 ⇒
P sr (Cons_monom c1 l1 t1) (Cons_monom c2 l2 t2)) ∧
(∀sr c1 l1 t1 l2 t2.
P sr t1 t2 ∧ P sr t1 (Cons_varlist l2 t2) ∧
P sr (Cons_monom c1 l1 t1) t2 ⇒
P sr (Cons_monom c1 l1 t1) (Cons_varlist l2 t2)) ∧
(∀sr l1 t1 c2 l2 t2.
P sr t1 t2 ∧ P sr t1 (Cons_monom c2 l2 t2) ∧
P sr (Cons_varlist l1 t1) t2 ⇒
P sr (Cons_varlist l1 t1) (Cons_monom c2 l2 t2)) ∧
(∀sr l1 t1 l2 t2.
P sr t1 t2 ∧ P sr t1 (Cons_varlist l2 t2) ∧
P sr (Cons_varlist l1 t1) t2 ⇒
P sr (Cons_varlist l1 t1) (Cons_varlist l2 t2)) ∧
(∀sr s1. P sr s1 Nil_monom) ∧
(∀sr v4 v5 v6. P sr Nil_monom (Cons_monom v4 v5 v6)) ∧
(∀sr v7 v8. P sr Nil_monom (Cons_varlist v7 v8)) ⇒
∀v v1 v2. P v v1 v2
- canonical_sum_merge_def
-
|- (∀t2 t1 sr l2 l1 c2 c1.
canonical_sum_merge sr (Cons_monom c1 l1 t1) (Cons_monom c2 l2 t2) =
compare (list_compare index_compare l1 l2)
(Cons_monom c1 l1 (canonical_sum_merge sr t1 (Cons_monom c2 l2 t2)))
(Cons_monom (SRP sr c1 c2) l1 (canonical_sum_merge sr t1 t2))
(Cons_monom c2 l2
(canonical_sum_merge sr (Cons_monom c1 l1 t1) t2))) ∧
(∀t2 t1 sr l2 l1 c1.
canonical_sum_merge sr (Cons_monom c1 l1 t1) (Cons_varlist l2 t2) =
compare (list_compare index_compare l1 l2)
(Cons_monom c1 l1 (canonical_sum_merge sr t1 (Cons_varlist l2 t2)))
(Cons_monom (SRP sr c1 (SR1 sr)) l1 (canonical_sum_merge sr t1 t2))
(Cons_varlist l2 (canonical_sum_merge sr (Cons_monom c1 l1 t1) t2))) ∧
(∀t2 t1 sr l2 l1 c2.
canonical_sum_merge sr (Cons_varlist l1 t1) (Cons_monom c2 l2 t2) =
compare (list_compare index_compare l1 l2)
(Cons_varlist l1 (canonical_sum_merge sr t1 (Cons_monom c2 l2 t2)))
(Cons_monom (SRP sr (SR1 sr) c2) l1 (canonical_sum_merge sr t1 t2))
(Cons_monom c2 l2 (canonical_sum_merge sr (Cons_varlist l1 t1) t2))) ∧
(∀t2 t1 sr l2 l1.
canonical_sum_merge sr (Cons_varlist l1 t1) (Cons_varlist l2 t2) =
compare (list_compare index_compare l1 l2)
(Cons_varlist l1 (canonical_sum_merge sr t1 (Cons_varlist l2 t2)))
(Cons_monom (SRP sr (SR1 sr) (SR1 sr)) l1
(canonical_sum_merge sr t1 t2))
(Cons_varlist l2 (canonical_sum_merge sr (Cons_varlist l1 t1) t2))) ∧
(∀sr s1. canonical_sum_merge sr s1 Nil_monom = s1) ∧
(∀v6 v5 v4 sr.
canonical_sum_merge sr Nil_monom (Cons_monom v4 v5 v6) =
Cons_monom v4 v5 v6) ∧
∀v8 v7 sr.
canonical_sum_merge sr Nil_monom (Cons_varlist v7 v8) =
Cons_varlist v7 v8
- monom_insert_ind
-
|- ∀P.
(∀sr c1 l1 c2 l2 t2. P sr c1 l1 t2 ⇒ P sr c1 l1 (Cons_monom c2 l2 t2)) ∧
(∀sr c1 l1 l2 t2. P sr c1 l1 t2 ⇒ P sr c1 l1 (Cons_varlist l2 t2)) ∧
(∀sr c1 l1. P sr c1 l1 Nil_monom) ⇒
∀v v1 v2 v3. P v v1 v2 v3
- monom_insert_def
-
|- (∀t2 sr l2 l1 c2 c1.
monom_insert sr c1 l1 (Cons_monom c2 l2 t2) =
compare (list_compare index_compare l1 l2)
(Cons_monom c1 l1 (Cons_monom c2 l2 t2))
(Cons_monom (SRP sr c1 c2) l1 t2)
(Cons_monom c2 l2 (monom_insert sr c1 l1 t2))) ∧
(∀t2 sr l2 l1 c1.
monom_insert sr c1 l1 (Cons_varlist l2 t2) =
compare (list_compare index_compare l1 l2)
(Cons_monom c1 l1 (Cons_varlist l2 t2))
(Cons_monom (SRP sr c1 (SR1 sr)) l1 t2)
(Cons_varlist l2 (monom_insert sr c1 l1 t2))) ∧
∀sr l1 c1. monom_insert sr c1 l1 Nil_monom = Cons_monom c1 l1 Nil_monom
- varlist_insert_ind
-
|- ∀P.
(∀sr l1 c2 l2 t2. P sr l1 t2 ⇒ P sr l1 (Cons_monom c2 l2 t2)) ∧
(∀sr l1 l2 t2. P sr l1 t2 ⇒ P sr l1 (Cons_varlist l2 t2)) ∧
(∀sr l1. P sr l1 Nil_monom) ⇒
∀v v1 v2. P v v1 v2
- varlist_insert_def
-
|- (∀t2 sr l2 l1 c2.
varlist_insert sr l1 (Cons_monom c2 l2 t2) =
compare (list_compare index_compare l1 l2)
(Cons_varlist l1 (Cons_monom c2 l2 t2))
(Cons_monom (SRP sr (SR1 sr) c2) l1 t2)
(Cons_monom c2 l2 (varlist_insert sr l1 t2))) ∧
(∀t2 sr l2 l1.
varlist_insert sr l1 (Cons_varlist l2 t2) =
compare (list_compare index_compare l1 l2)
(Cons_varlist l1 (Cons_varlist l2 t2))
(Cons_monom (SRP sr (SR1 sr) (SR1 sr)) l1 t2)
(Cons_varlist l2 (varlist_insert sr l1 t2))) ∧
∀sr l1. varlist_insert sr l1 Nil_monom = Cons_varlist l1 Nil_monom
- ivl_aux_ok
-
|- ∀sr.
is_semi_ring sr ⇒
∀vm v i.
ivl_aux sr vm i v = SRM sr (varmap_find i vm) (interp_vl sr vm v)
- varlist_merge_ok
-
|- ∀sr.
is_semi_ring sr ⇒
∀vm x y.
interp_vl sr vm (list_merge index_lt x y) =
SRM sr (interp_vl sr vm x) (interp_vl sr vm y)
- ics_aux_ok
-
|- ∀sr.
is_semi_ring sr ⇒
∀vm x s. ics_aux sr vm x s = SRP sr x (interp_cs sr vm s)
- interp_m_ok
-
|- ∀sr.
is_semi_ring sr ⇒
∀vm x l. interp_m sr vm x l = SRM sr x (interp_vl sr vm l)
- canonical_sum_merge_ok
-
|- ∀sr.
is_semi_ring sr ⇒
∀vm x y.
interp_cs sr vm (canonical_sum_merge sr x y) =
SRP sr (interp_cs sr vm x) (interp_cs sr vm y)
- monom_insert_ok
-
|- ∀sr.
is_semi_ring sr ⇒
∀vm a l s.
interp_cs sr vm (monom_insert sr a l s) =
SRP sr (SRM sr a (interp_vl sr vm l)) (interp_cs sr vm s)
- varlist_insert_ok
-
|- ∀sr.
is_semi_ring sr ⇒
∀vm l s.
interp_cs sr vm (varlist_insert sr l s) =
SRP sr (interp_vl sr vm l) (interp_cs sr vm s)
- canonical_sum_scalar_ok
-
|- ∀sr.
is_semi_ring sr ⇒
∀vm a s.
interp_cs sr vm (canonical_sum_scalar sr a s) =
SRM sr a (interp_cs sr vm s)
- canonical_sum_scalar2_ok
-
|- ∀sr.
is_semi_ring sr ⇒
∀vm l s.
interp_cs sr vm (canonical_sum_scalar2 sr l s) =
SRM sr (interp_vl sr vm l) (interp_cs sr vm s)
- canonical_sum_scalar3_ok
-
|- ∀sr.
is_semi_ring sr ⇒
∀vm c l s.
interp_cs sr vm (canonical_sum_scalar3 sr c l s) =
SRM sr (SRM sr c (interp_vl sr vm l)) (interp_cs sr vm s)
- canonical_sum_prod_ok
-
|- ∀sr.
is_semi_ring sr ⇒
∀vm x y.
interp_cs sr vm (canonical_sum_prod sr x y) =
SRM sr (interp_cs sr vm x) (interp_cs sr vm y)
- canonical_sum_simplify_ok
-
|- ∀sr.
is_semi_ring sr ⇒
∀vm s. interp_cs sr vm (canonical_sum_simplify sr s) = interp_cs sr vm s
- datatype_spolynom
-
|- DATATYPE (spolynom SPvar SPconst SPplus SPmult)
- spolynom_11
-
|- (∀a a'. (SPvar a = SPvar a') ⇔ (a = a')) ∧
(∀a a'. (SPconst a = SPconst a') ⇔ (a = a')) ∧
(∀a0 a1 a0' a1'.
(SPplus a0 a1 = SPplus a0' a1') ⇔ (a0 = a0') ∧ (a1 = a1')) ∧
∀a0 a1 a0' a1'. (SPmult a0 a1 = SPmult a0' a1') ⇔ (a0 = a0') ∧ (a1 = a1')
- spolynom_distinct
-
|- (∀a' a. SPvar a ≠ SPconst a') ∧ (∀a1 a0 a. SPvar a ≠ SPplus a0 a1) ∧
(∀a1 a0 a. SPvar a ≠ SPmult a0 a1) ∧ (∀a1 a0 a. SPconst a ≠ SPplus a0 a1) ∧
(∀a1 a0 a. SPconst a ≠ SPmult a0 a1) ∧
∀a1' a1 a0' a0. SPplus a0 a1 ≠ SPmult a0' a1'
- spolynom_case_cong
-
|- ∀M M' f f1 f2 f3.
(M = M') ∧ (∀a. (M' = SPvar a) ⇒ (f a = f' a)) ∧
(∀a. (M' = SPconst a) ⇒ (f1 a = f1' a)) ∧
(∀a0 a1. (M' = SPplus a0 a1) ⇒ (f2 a0 a1 = f2' a0 a1)) ∧
(∀a0 a1. (M' = SPmult a0 a1) ⇒ (f3 a0 a1 = f3' a0 a1)) ⇒
(spolynom_CASE M f f1 f2 f3 = spolynom_CASE M' f' f1' f2' f3')
- spolynom_nchotomy
-
|- ∀ss.
(∃i. ss = SPvar i) ∨ (∃a. ss = SPconst a) ∨ (∃s s0. ss = SPplus s s0) ∨
∃s s0. ss = SPmult s s0
- spolynom_Axiom
-
|- ∀f0 f1 f2 f3.
∃fn.
(∀a. fn (SPvar a) = f0 a) ∧ (∀a. fn (SPconst a) = f1 a) ∧
(∀a0 a1. fn (SPplus a0 a1) = f2 a0 a1 (fn a0) (fn a1)) ∧
∀a0 a1. fn (SPmult a0 a1) = f3 a0 a1 (fn a0) (fn a1)
- spolynom_induction
-
|- ∀P.
(∀i. P (SPvar i)) ∧ (∀a. P (SPconst a)) ∧
(∀s s0. P s ∧ P s0 ⇒ P (SPplus s s0)) ∧
(∀s s0. P s ∧ P s0 ⇒ P (SPmult s s0)) ⇒
∀s. P s
- spolynomial_normalize_ok
-
|- ∀sr.
is_semi_ring sr ⇒
∀vm p. interp_cs sr vm (spolynom_normalize sr p) = interp_sp sr vm p
- spolynomial_simplify_ok
-
|- ∀sr.
is_semi_ring sr ⇒
∀vm p. interp_cs sr vm (spolynom_simplify sr p) = interp_sp sr vm p