Step * 1 1 1 of Lemma mvp-add_wf


1. CRng
2. 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. bag(Atom)
9. ¬sub-bag(Atom;b;bag-lub(AtomDeq;s;s1))
⊢ (+r 0) 0 ∈ |r|
BY
(All Thin⋅ THEN THEN THEN RepeatFor (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