---

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

.....subterm..... T:t
3: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|)
⊢ bag-partitions(eq;b) = ([p∈bag-partitions(eq;b)|¬bbag-null(fst(p))] + {<{}, b>}) ∈ bag(bag(X) × bag(X))
BY
{ xxx((InstLemma `bag-split` [⌜bag(X) × bag(X)⌝;⌜λ2p.¬bbag-null(fst(p))⌝;⌜bag-partitions(eq;b)⌝]⋅ THENA Auto)
      THEN NthHypEq (-1)
      THEN RepeatFor 2 ((EqCD THEN Auto)))xxx }

1
.....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))

---

Latex:

---

Latex:
.....subterm.....  T:t
3: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]))
\mvdash{}  bag-partitions(eq;b)  =  ([p\mmember{}bag-partitions(eq;b)|\mneg{}\msubb{}bag-null(fst(p))]  +  \{<\{\},  b>\})


By

---

Latex:
xxx((InstLemma  `bag-split`  [\mkleeneopen{}bag(X)  \mtimes{}  bag(X)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}p.\mneg{}\msubb{}bag-null(fst(p))\mkleeneclose{};\mkleeneopen{}bag-partitions(eq;b)\mkleeneclose{}]\mcdot{}
          THENA  Auto
          )
        THEN  NthHypEq  (-1)
        THEN  RepeatFor  2  ((EqCD  THEN  Auto)))xxx

---

Home Index