---

Step * 1 of Lemma mvp-add_wf

.....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))
BY
{ xxx(All (Unfold `fps-support`)⋅ THEN Auto THEN RepUR ``fps-add fps-coeff`` 0)xxx }

1
1. r : CRng
2. s : bag(Atom)
3. p1 : {f:PowerSeries(r)| ∀[b:bag(Atom)]. f[b] = 0 ∈ |r| supposing ¬sub-bag(Atom;b;s)} 
4. s1 : bag(Atom)
5. q1 : {f:PowerSeries(r)| ∀[b:bag(Atom)]. f[b] = 0 ∈ |r| supposing ¬sub-bag(Atom;b;s1)} 
6. b : bag(Atom)
7. ¬sub-bag(Atom;b;bag-lub(AtomDeq;s;s1))
⊢ (+r (p1 b) (q1 b)) = 0 ∈ |r|

---

Latex:

---

Latex:
.....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)\} 
\mvdash{}  fps-support(r;(p1+q1);bag-lub(AtomDeq;s;s1))


By

---

Latex:
xxx(All  (Unfold  `fps-support`)\mcdot{}  THEN  Auto  THEN  RepUR  ``fps-add  fps-coeff``  0)xxx

---

Home Index