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