---

Step * 1 1 1 of Lemma mvp-add_wf


1. r : CRng
2. s : bag(Atom)
3. p1 : PowerSeries(r)
4. ∀[b:bag(Atom)]. (p1 b) = 0 ∈ |r| supposing ¬sub-bag(Atom;b;s)
5. s1 : bag(Atom)
6. q1 : PowerSeries(r)
7. ∀[b:bag(Atom)]. (q1 b) = 0 ∈ |r| supposing ¬sub-bag(Atom;b;s1)
8. b : bag(Atom)
9. ¬sub-bag(Atom;b;bag-lub(AtomDeq;s;s1))
⊢ (+r 0 0) = 0 ∈ |r|
BY
{ (All Thin⋅ THEN D 1 THEN D 1 THEN RepeatFor 2 (D 2) THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  s  :  bag(Atom)
3.  p1  :  PowerSeries(r)
4.  \mforall{}[b:bag(Atom)].  (p1  b)  =  0  supposing  \mneg{}sub-bag(Atom;b;s)
5.  s1  :  bag(Atom)
6.  q1  :  PowerSeries(r)
7.  \mforall{}[b:bag(Atom)].  (q1  b)  =  0  supposing  \mneg{}sub-bag(Atom;b;s1)
8.  b  :  bag(Atom)
9.  \mneg{}sub-bag(Atom;b;bag-lub(AtomDeq;s;s1))
\mvdash{}  (+r  0  0)  =  0


By

---

Latex:
(All  Thin\mcdot{}  THEN  D  1  THEN  D  1  THEN  RepeatFor  2  (D  2)  THEN  Auto)

---

Home Index