Definitions
canonical_sumMAP_def
⊢ ∀f af.
canonical_sumMAP f (canonical_sum_CONS af) =
canonical_sum_CONS
(SUM_MAP I
(SUM_MAP (f ## I ## canonical_sumMAP f) (I ## canonical_sumMAP f))
af)
canonical_sumREL_def
⊢ canonical_sumREL =
(λR x y.
∃z. (∀p. p ∈ canonical_sumSET z ⇒ R (FST p) (SND p)) ∧
canonical_sumMAP FST z = x ∧ canonical_sumMAP SND z = y)
canonical_sumSET_def
⊢ ∀af.
canonical_sumSET (canonical_sum_CONS af) =
S ($UNION ∘ BIMG (K ∅) ∘ setL)
(BIMG
(S
($UNION ∘
BIMG
(S ($UNION ∘ BIMG $= ∘ setFST)
(BIMG
(S ($UNION ∘ BIMG (K ∅) ∘ setFST)
(BIMG (K ∅) ∘ setSND)) ∘ setSND)) ∘ setL)
(BIMG (S ($UNION ∘ BIMG (K ∅) ∘ setFST) (BIMG (K ∅) ∘ setSND)) ∘
setR)) ∘ setR) af ∪
BIGUNION
(IMAGE canonical_sumSET
(S ($UNION ∘ BIMG (K ∅) ∘ setL)
(BIMG
(S
($UNION ∘
BIMG
(S ($UNION ∘ BIMG (K ∅) ∘ setFST)
(BIMG
(S ($UNION ∘ BIMG (K ∅) ∘ setFST)
(BIMG $= ∘ setSND)) ∘ setSND)) ∘ setL)
(BIMG
(S ($UNION ∘ BIMG (K ∅) ∘ setFST) (BIMG $= ∘ setSND)) ∘
setR)) ∘ setR) af))
canonical_sum_case_def
⊢ (∀v f f0. canonical_sum_CASE Nil_monom v f f0 = v) ∧
(∀a0 a1 a2 v f f0.
canonical_sum_CASE (Cons_monom a0 a1 a2) v f f0 = f a0 a1 a2) ∧
∀a0 a1 v f f0. canonical_sum_CASE (Cons_varlist a0 a1) v f f0 = f0 a0 a1
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_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 (sr.SRM 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_scalar_def
⊢ (∀sr c0 c l t.
canonical_sum_scalar sr c0 (Cons_monom c l t) =
Cons_monom (sr.SRM 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_simplify_def
⊢ (∀sr c l t.
canonical_sum_simplify sr (Cons_monom c l t) =
if c = sr.SR0 then canonical_sum_simplify sr t
else if c = sr.SR1 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
canonical_sum_size_def
⊢ (∀f0. canonical_sum_size f0 Nil_monom = 0) ∧
(∀f0 a0 a1 a2.
canonical_sum_size f0 (Cons_monom a0 a1 a2) =
1 + (f0 a0 + (list_size index_size a1 + canonical_sum_size f0 a2))) ∧
∀f0 a0 a1.
canonical_sum_size f0 (Cons_varlist a0 a1) =
1 + (list_size index_size a0 + canonical_sum_size f0 a1)
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) =
sr.SRP 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) =
sr.SRP a (ics_aux sr vm (interp_m sr vm c l) t)
interp_cs_def
⊢ (∀sr vm. interp_cs sr vm Nil_monom = sr.SR0) ∧
(∀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
interp_m_def
⊢ (∀sr vm c. interp_m sr vm c [] = c) ∧
∀sr vm c x t. interp_m sr vm c (x::t) = sr.SRM c (ivl_aux sr vm x t)
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) =
sr.SRP (interp_sp sr vm p1) (interp_sp sr vm p2)) ∧
∀sr vm p1 p2.
interp_sp sr vm (SPmult p1 p2) =
sr.SRM (interp_sp sr vm p1) (interp_sp sr vm p2)
interp_vl_def
⊢ (∀sr vm. interp_vl sr vm [] = sr.SR1) ∧
∀sr vm x t. interp_vl sr vm (x::t) = ivl_aux sr vm x t
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') =
sr.SRM (varmap_find x vm) (ivl_aux sr vm x' t')
spolynomMAP_def
⊢ ∀f af.
spolynomMAP f (spolynom_CONS af) =
spolynom_CONS
(SUM_MAP I
(SUM_MAP f
(SUM_MAP (spolynomMAP f ## spolynomMAP f)
(spolynomMAP f ## spolynomMAP f))) af)
spolynomREL_def
⊢ spolynomREL =
(λR x y.
∃z. (∀p. p ∈ spolynomSET z ⇒ R (FST p) (SND p)) ∧
spolynomMAP FST z = x ∧ spolynomMAP SND z = y)
spolynomSET_def
⊢ ∀af.
spolynomSET (spolynom_CONS af) =
S ($UNION ∘ BIMG (K ∅) ∘ setL)
(BIMG
(S ($UNION ∘ BIMG $= ∘ setL)
(BIMG
(S
($UNION ∘
BIMG
(S ($UNION ∘ BIMG (K ∅) ∘ setFST)
(BIMG (K ∅) ∘ setSND)) ∘ setL)
(BIMG
(S ($UNION ∘ BIMG (K ∅) ∘ setFST)
(BIMG (K ∅) ∘ setSND)) ∘ setR)) ∘ setR)) ∘ setR) af ∪
BIGUNION
(IMAGE spolynomSET
(S ($UNION ∘ BIMG (K ∅) ∘ setL)
(BIMG
(S ($UNION ∘ BIMG (K ∅) ∘ setL)
(BIMG
(S
($UNION ∘
BIMG
(S ($UNION ∘ BIMG $= ∘ setFST)
(BIMG $= ∘ setSND)) ∘ setL)
(BIMG
(S ($UNION ∘ BIMG $= ∘ setFST)
(BIMG $= ∘ setSND)) ∘ setR)) ∘ setR)) ∘ setR)
af))
spolynom_case_def
⊢ (∀a0 f f0 f1 f2. spolynom_CASE (SPvar a0) f f0 f1 f2 = f a0) ∧
(∀a0 f f0 f1 f2. spolynom_CASE (SPconst a0) f f0 f1 f2 = f0 a0) ∧
(∀a0 a1 f f0 f1 f2. spolynom_CASE (SPplus a0 a1) f f0 f1 f2 = f1 a0 a1) ∧
∀a0 a1 f f0 f1 f2. spolynom_CASE (SPmult a0 a1) f f0 f1 f2 = f2 a0 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)
spolynom_size_def
⊢ (∀f0 a0. spolynom_size f0 (SPvar a0) = 1 + index_size a0) ∧
(∀f0 a0. spolynom_size f0 (SPconst a0) = 1 + f0 a0) ∧
(∀f0 a0 a1.
spolynom_size f0 (SPplus a0 a1) =
1 + (spolynom_size f0 a0 + spolynom_size f0 a1)) ∧
∀f0 a0 a1.
spolynom_size f0 (SPmult a0 a1) =
1 + (spolynom_size f0 a0 + spolynom_size f0 a1)
Theorems
canonical_sumMAP_ind
⊢ ∀P'.
(∀f. P' f Nil_monom ∧ (∀c. P' f c ⇒ ∀l a. P' f (Cons_monom a l c)) ∧
∀c. P' f c ⇒ ∀l. P' f (Cons_varlist l c)) ⇒
∀f c. P' f c
canonical_sumMAP_thm
⊢ canonical_sumMAP f Nil_monom = Nil_monom ∧
canonical_sumMAP f (Cons_monom a0 a1 a2) =
Cons_monom (f a0) a1 (canonical_sumMAP f a2) ∧
canonical_sumMAP f (Cons_varlist a0 a1) =
Cons_varlist a0 (canonical_sumMAP f a1)
canonical_sumSET_ind
⊢ ∀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_sumSET_thm
⊢ canonical_sumSET Nil_monom = ∅ ∧
canonical_sumSET (Cons_monom a0 a1 a2) = a0 INSERT canonical_sumSET a2 ∧
canonical_sumSET (Cons_varlist a0 a1) = canonical_sumSET a1
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_Axiom
⊢ ∀f0 f1 f2. ∃h.
h Nil_monom = f0 ∧
(∀a0 a1 a2. h (Cons_monom a0 a1 a2) = f1 a0 a1 a2 (h a2)) ∧
∀a0 a1. h (Cons_varlist a0 a1) = f2 a0 a1 (h a1)
canonical_sum_MAP_CONG
⊢ ∀f g x.
(∀a. a ∈ canonical_sumSET x ⇒ f a = g a) ⇒
canonical_sumMAP f x = canonical_sumMAP g x
canonical_sum_MAP_ID
⊢ canonical_sumMAP I = I
canonical_sum_MAP_IMAGE
⊢ ∀f n.
canonical_sumSET (canonical_sumMAP f n) = IMAGE f (canonical_sumSET n)
canonical_sum_MAP_O
⊢ canonical_sumMAP f ∘ canonical_sumMAP g = canonical_sumMAP (f ∘ g)
canonical_sum_bnd
⊢ ∀n. cardleq (canonical_sumSET n) 𝕌(:num)
canonical_sum_case_cong
⊢ ∀M M' v f f0.
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 ⇒ f0 a0 a1 = f0' a0 a1) ⇒
canonical_sum_CASE M v f f0 = canonical_sum_CASE M' v' f' f0'
canonical_sum_case_eq
⊢ canonical_sum_CASE x v f f0 = v' ⇔
x = Nil_monom ∧ v = v' ∨ (∃a l c. x = Cons_monom a l c ∧ f a l c = v') ∨
∃l c. x = Cons_varlist l c ∧ f0 l c = v'
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_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_inh
⊢ ∀a2.
a2 ∈
canonical_sumSET
((λa2. canonical_sum_CONS (INR (INL (flip $, ARB a2)))) a2)
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 (sr.SRP 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 (sr.SRP c1 sr.SR1) 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 (sr.SRP sr.SR1 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 (sr.SRP sr.SR1 sr.SR1) 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
canonical_sum_merge_ind
⊢ ∀P. (∀sr c1 l1 t1 c2 l2 t2.
(list_compare index_compare l1 l2 = EQUAL ⇒ P sr t1 t2) ∧
(list_compare index_compare l1 l2 = GREATER ⇒
P sr (Cons_monom c1 l1 t1) t2) ∧
(list_compare index_compare l1 l2 = LESS ⇒
P sr t1 (Cons_monom c2 l2 t2)) ⇒
P sr (Cons_monom c1 l1 t1) (Cons_monom c2 l2 t2)) ∧
(∀sr c1 l1 t1 l2 t2.
(list_compare index_compare l1 l2 = EQUAL ⇒ P sr t1 t2) ∧
(list_compare index_compare l1 l2 = GREATER ⇒
P sr (Cons_monom c1 l1 t1) t2) ∧
(list_compare index_compare l1 l2 = LESS ⇒
P sr t1 (Cons_varlist l2 t2)) ⇒
P sr (Cons_monom c1 l1 t1) (Cons_varlist l2 t2)) ∧
(∀sr l1 t1 c2 l2 t2.
(list_compare index_compare l1 l2 = EQUAL ⇒ P sr t1 t2) ∧
(list_compare index_compare l1 l2 = GREATER ⇒
P sr (Cons_varlist l1 t1) t2) ∧
(list_compare index_compare l1 l2 = LESS ⇒
P sr t1 (Cons_monom c2 l2 t2)) ⇒
P sr (Cons_varlist l1 t1) (Cons_monom c2 l2 t2)) ∧
(∀sr l1 t1 l2 t2.
(list_compare index_compare l1 l2 = EQUAL ⇒ P sr t1 t2) ∧
(list_compare index_compare l1 l2 = GREATER ⇒
P sr (Cons_varlist l1 t1) t2) ∧
(list_compare index_compare l1 l2 = LESS ⇒
P sr t1 (Cons_varlist l2 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_ok
⊢ ∀sr.
is_semi_ring sr ⇒
∀vm x y.
interp_cs sr vm (canonical_sum_merge sr x y) =
sr.SRP (interp_cs sr vm x) (interp_cs sr vm y)
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_prod_ok
⊢ ∀sr.
is_semi_ring sr ⇒
∀vm x y.
interp_cs sr vm (canonical_sum_prod sr x y) =
sr.SRM (interp_cs sr vm x) (interp_cs sr vm y)
canonical_sum_scalar2_ok
⊢ ∀sr.
is_semi_ring sr ⇒
∀vm l s.
interp_cs sr vm (canonical_sum_scalar2 sr l s) =
sr.SRM (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) =
sr.SRM (sr.SRM c (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) =
sr.SRM a (interp_cs sr vm s)
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
canonical_sum_wit
⊢ ∀a. canonical_sumSET ((λa. canonical_sum_CONS ((K ∘ INL) ARB ARB)) a) ⊆ ∅
datatype_canonical_sum
⊢ DATATYPE (canonical_sum Nil_monom Cons_monom Cons_varlist)
datatype_spolynom
⊢ DATATYPE (spolynom SPvar SPconst SPplus SPmult)
ics_aux_ok
⊢ ∀sr.
is_semi_ring sr ⇒
∀vm x s. ics_aux sr vm x s = sr.SRP x (interp_cs sr vm s)
interp_m_ok
⊢ ∀sr.
is_semi_ring sr ⇒
∀vm x l. interp_m sr vm x l = sr.SRM x (interp_vl sr vm l)
ivl_aux_ok
⊢ ∀sr.
is_semi_ring sr ⇒
∀vm v i.
ivl_aux sr vm i v = sr.SRM (varmap_find i vm) (interp_vl sr vm v)
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 (sr.SRP 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 (sr.SRP c1 sr.SR1) 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
monom_insert_ind
⊢ ∀P. (∀sr c1 l1 c2 l2 t2.
(list_compare index_compare l1 l2 = GREATER ⇒ P sr c1 l1 t2) ⇒
P sr c1 l1 (Cons_monom c2 l2 t2)) ∧
(∀sr c1 l1 l2 t2.
(list_compare index_compare l1 l2 = GREATER ⇒ 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_ok
⊢ ∀sr.
is_semi_ring sr ⇒
∀vm a l s.
interp_cs sr vm (monom_insert sr a l s) =
sr.SRP (sr.SRM a (interp_vl sr vm l)) (interp_cs sr vm s)
spolynomMAP_ind
⊢ ∀P'.
(∀f. (∀i. P' f (SPvar i)) ∧ (∀a. P' f (SPconst a)) ∧
(∀s s0. P' f s ∧ P' f s0 ⇒ P' f (SPplus s s0)) ∧
∀s s0. P' f s ∧ P' f s0 ⇒ P' f (SPmult s s0)) ⇒
∀f s. P' f s
spolynomMAP_thm
⊢ spolynomMAP f (SPvar a0) = SPvar a0 ∧
spolynomMAP f (SPconst a0) = SPconst (f a0) ∧
spolynomMAP f (SPplus a0 a1) =
SPplus (spolynomMAP f a0) (spolynomMAP f a1) ∧
spolynomMAP f (SPmult a0 a1) =
SPmult (spolynomMAP f a0) (spolynomMAP f a1)
spolynomSET_ind
⊢ ∀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
spolynomSET_thm
⊢ spolynomSET (SPvar a0) = ∅ ∧ spolynomSET (SPconst a0) = {a0} ∧
spolynomSET (SPplus a0 a1) = spolynomSET a0 ∪ spolynomSET a1 ∧
spolynomSET (SPmult a0 a1) = spolynomSET a0 ∪ spolynomSET a1
spolynom_11
⊢ (∀a0 a0'. SPvar a0 = SPvar a0' ⇔ a0 = a0') ∧
(∀a0 a0'. SPconst a0 = SPconst a0' ⇔ a0 = a0') ∧
(∀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_Axiom
⊢ ∀f0 f1 f2 f3. ∃h.
(∀a0. h (SPvar a0) = f0 a0) ∧ (∀a0. h (SPconst a0) = f1 a0) ∧
(∀a0 a1. h (SPplus a0 a1) = f2 a0 a1 (h a0) (h a1)) ∧
∀a0 a1. h (SPmult a0 a1) = f3 a0 a1 (h a0) (h a1)
spolynom_MAP_CONG
⊢ ∀f g x.
(∀a. a ∈ spolynomSET x ⇒ f a = g a) ⇒ spolynomMAP f x = spolynomMAP g x
spolynom_MAP_ID
⊢ spolynomMAP I = I
spolynom_MAP_IMAGE
⊢ ∀f n. spolynomSET (spolynomMAP f n) = IMAGE f (spolynomSET n)
spolynom_MAP_O
⊢ spolynomMAP f ∘ spolynomMAP g = spolynomMAP (f ∘ g)
spolynom_bnd
⊢ ∀n. cardleq (spolynomSET n) 𝕌(:num)
spolynom_case_cong
⊢ ∀M M' f f0 f1 f2.
M = M' ∧ (∀a0. M' = SPvar a0 ⇒ f a0 = f' a0) ∧
(∀a0. M' = SPconst a0 ⇒ f0 a0 = f0' a0) ∧
(∀a0 a1. M' = SPplus a0 a1 ⇒ f1 a0 a1 = f1' a0 a1) ∧
(∀a0 a1. M' = SPmult a0 a1 ⇒ f2 a0 a1 = f2' a0 a1) ⇒
spolynom_CASE M f f0 f1 f2 = spolynom_CASE M' f' f0' f1' f2'
spolynom_case_eq
⊢ spolynom_CASE x f f0 f1 f2 = v ⇔
(∃i. x = SPvar i ∧ f i = v) ∨ (∃a. x = SPconst a ∧ f0 a = v) ∨
(∃s s0. x = SPplus s s0 ∧ f1 s s0 = v) ∨
∃s s0. x = SPmult s s0 ∧ f2 s s0 = v
spolynom_distinct
⊢ (∀a0' a0. SPvar a0 ≠ SPconst a0') ∧
(∀a1 a0' a0. SPvar a0 ≠ SPplus a0' a1) ∧
(∀a1 a0' a0. SPvar a0 ≠ SPmult a0' a1) ∧
(∀a1 a0' a0. SPconst a0 ≠ SPplus a0' a1) ∧
(∀a1 a0' a0. SPconst a0 ≠ SPmult a0' a1) ∧
∀a1' a1 a0' a0. SPplus a0 a1 ≠ SPmult a0' 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
spolynom_inh
⊢ ∀a2. a2 ∈ spolynomSET ((λa2. spolynom_CONS (INR (INL a2))) a2)
spolynom_nchotomy
⊢ ∀ss.
(∃i. ss = SPvar i) ∨ (∃a. ss = SPconst a) ∨ (∃s s0. ss = SPplus s s0) ∨
∃s s0. ss = SPmult s s0
spolynom_wit
⊢ ∀a. spolynomSET ((λa. spolynom_CONS ((K ∘ INL) ARB ARB)) a) ⊆ ∅
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
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 (sr.SRP sr.SR1 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 (sr.SRP sr.SR1 sr.SR1) l1 t2)
(Cons_varlist l2 (varlist_insert sr l1 t2))) ∧
∀sr l1. varlist_insert sr l1 Nil_monom = Cons_varlist l1 Nil_monom
varlist_insert_ind
⊢ ∀P. (∀sr l1 c2 l2 t2.
(list_compare index_compare l1 l2 = GREATER ⇒ P sr l1 t2) ⇒
P sr l1 (Cons_monom c2 l2 t2)) ∧
(∀sr l1 l2 t2.
(list_compare index_compare l1 l2 = GREATER ⇒ 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_ok
⊢ ∀sr.
is_semi_ring sr ⇒
∀vm l s.
interp_cs sr vm (varlist_insert sr l s) =
sr.SRP (interp_vl sr vm l) (interp_cs sr vm s)
varlist_merge_ok
⊢ ∀sr.
is_semi_ring sr ⇒
∀vm x y.
interp_vl sr vm (list_merge index_lt x y) =
sr.SRM (interp_vl sr vm x) (interp_vl sr vm y)