---

Step * of Lemma mvp-add_wf

∀[r:CRng]. ∀[p,q:mv-polynomial(r)].  (mvp-add(r;p;q) ∈ mv-polynomial(r))
BY
{ (ProveWfLemma THEN MemTypeCD THEN Auto) }

1
.....set predicate..... 
1. r : CRng
2. s : bag(Atom)
3. p1 : {f:PowerSeries(r)| fps-support(r;f;s)} 
4. s1 : bag(Atom)
5. q1 : {f:PowerSeries(r)| fps-support(r;f;s1)} 
⊢ fps-support(r;(p1+q1);bag-lub(AtomDeq;s;s1))

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[p,q:mv-polynomial(r)].    (mvp-add(r;p;q)  \mmember{}  mv-polynomial(r))


By

---

Latex:
(ProveWfLemma  THEN  MemTypeCD  THEN  Auto)

---

Home Index