---

Step * 1 1 2 1 1 of Lemma fps-div-coeff-property

.....subterm..... T:t
2:n
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. (g[{}] * x) = 1 ∈ |r|
9. Comm(|r|;+r)
10. Assoc(|r|;+r)
11. b : bag(X)
12. ∀[f:(bag(X) × bag(X)) ⟶ |r|]. ∀[b,c:bag(bag(X) × bag(X))].
      (Σ(x∈b + c). f[x] = (Σ(x∈b). f[x] +r Σ(x∈c). f[x]) ∈ |r|)
13. bag-partitions(eq;b)
= ([x∈bag-partitions(eq;b)|¬bbag-null(fst(x))] + [x∈bag-partitions(eq;b)|¬b¬bbag-null(fst(x))])
∈ bag(bag(X) × bag(X))
⊢ {<{}, b>} = [x∈bag-partitions(eq;b)|¬b¬bbag-null(fst(x))] ∈ bag(bag(X) × bag(X))
BY
{ xxx(MoveToConcl 2 THEN All Thin THEN Auto)xxx }

1
1. X : Type
2. eq : EqDecider(X)
3. b : bag(X)
4. valueall-type(X)
⊢ {<{}, b>} = [x∈bag-partitions(eq;b)|¬b¬bbag-null(fst(x))] ∈ bag(bag(X) × bag(X))

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
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.  (g[\{\}]  *  x)  =  1
9.  Comm(|r|;+r)
10.  Assoc(|r|;+r)
11.  b  :  bag(X)
12.  \mforall{}[f:(bag(X)  \mtimes{}  bag(X))  {}\mrightarrow{}  |r|].  \mforall{}[b,c:bag(bag(X)  \mtimes{}  bag(X))].
            (\mSigma{}(x\mmember{}b  +  c).  f[x]  =  (\mSigma{}(x\mmember{}b).  f[x]  +r  \mSigma{}(x\mmember{}c).  f[x]))
13.  bag-partitions(eq;b)
=  ([x\mmember{}bag-partitions(eq;b)|\mneg{}\msubb{}bag-null(fst(x))]  +  [x\mmember{}bag-partitions(eq;b)|\mneg{}\msubb{}\mneg{}\msubb{}bag-null(fst(x))])
\mvdash{}  \{<\{\},  b>\}  =  [x\mmember{}bag-partitions(eq;b)|\mneg{}\msubb{}\mneg{}\msubb{}bag-null(fst(x))]


By

---

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

---

Home Index