---

Step * 1 of Lemma fps-div-coeff_wf

.....wf..... 
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. f : PowerSeries(X;r)
6. g : PowerSeries(X;r)
7. x : |r|
8. b : bag(X)
9. n : ℕ
10. ∀n:ℕn. ∀b:bag(X).  ((#(b) ≤ n) ⇒ (fps-div-coeff(eq;r;f;g;x;b) ∈ |r|))
11. b1 : bag(X)
12. #(b1) ≤ n
⊢ [p∈bag-partitions(eq;b1)|¬bbag-null(fst(p))] ∈ bag({p:bag(X) × bag(X)| #(snd(p)) < #(b1)} )
BY
{ xxx(MoveToConcl 2 THEN All Thin THEN Auto)xxx }

1
1. X : Type
2. eq : EqDecider(X)
3. b1 : bag(X)
4. valueall-type(X)
⊢ [p∈bag-partitions(eq;b1)|¬bbag-null(fst(p))] ∈ bag({p:bag(X) × bag(X)| #(snd(p)) < #(b1)} )

---

Latex:

---

Latex:
.....wf..... 
1.  X  :  Type
2.  valueall-type(X)
3.  eq  :  EqDecider(X)
4.  r  :  CRng
5.  f  :  PowerSeries(X;r)
6.  g  :  PowerSeries(X;r)
7.  x  :  |r|
8.  b  :  bag(X)
9.  n  :  \mBbbN{}
10.  \mforall{}n:\mBbbN{}n.  \mforall{}b:bag(X).    ((\#(b)  \mleq{}  n)  {}\mRightarrow{}  (fps-div-coeff(eq;r;f;g;x;b)  \mmember{}  |r|))
11.  b1  :  bag(X)
12.  \#(b1)  \mleq{}  n
\mvdash{}  [p\mmember{}bag-partitions(eq;b1)|\mneg{}\msubb{}bag-null(fst(p))]  \mmember{}  bag(\{p:bag(X)  \mtimes{}  bag(X)|  \#(snd(p))  <  \#(b1)\}  )


By

---

Latex:
xxx(MoveToConcl  2  THEN  All  Thin  THEN  Auto)xxx

---

Home Index