Step
*
1
1
of Lemma
fps-mul-single-general
.....assertion.....
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. c : bag(X)
6. f : PowerSeries(X;r)
7. Comm(|r|;+r)
8. IsMonoid(|r|;+r;0)
9. b : bag(X)@i
10. x : bag(X)@i
11. b = (c + x) ∈ bag(X)
12. ([p∈bag-partitions(eq;b)|bag-eq(eq;fst(p);c)] = {<c, x>} ∈ bag(bag(X) × bag(X)))
∧ ([p∈bag-partitions(eq;b)|bag-eq(eq;snd(p);x)] = {<c, x>} ∈ bag(bag(X) × bag(X)))
⊢ Σ(p∈[p∈bag-partitions(eq;b)|bag-eq(eq;fst(p);c)]). * (<c> (fst(p))) (f (snd(p))) = (f x) ∈ |r|
BY
{ (D -1 THEN Thin (-1) THEN HypSubst' -1 0 THEN Auto THEN Try ((Fold `power-series` 0 THEN Auto))) }
1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. c : bag(X)
6. f : PowerSeries(X;r)
7. Comm(|r|;+r)
8. IsMonoid(|r|;+r;0)
9. b : bag(X)@i
10. x : bag(X)@i
11. b = (c + x) ∈ bag(X)
12. [p∈bag-partitions(eq;b)|bag-eq(eq;fst(p);c)] = {<c, x>} ∈ bag(bag(X) × bag(X))
⊢ Σ(p∈{<c, x>}). * (<c> (fst(p))) (f (snd(p))) = (f x) ∈ |r|
Latex:
Latex:
.....assertion.....
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. c : bag(X)
6. f : PowerSeries(X;r)
7. Comm(|r|;+r)
8. IsMonoid(|r|;+r;0)
9. b : bag(X)@i
10. x : bag(X)@i
11. b = (c + x)
12. ([p\mmember{}bag-partitions(eq;b)|bag-eq(eq;fst(p);c)] = \{<c, x>\})
\mwedge{} ([p\mmember{}bag-partitions(eq;b)|bag-eq(eq;snd(p);x)] = \{<c, x>\})
\mvdash{} \mSigma{}(p\mmember{}[p\mmember{}bag-partitions(eq;b)|bag-eq(eq;fst(p);c)]). * (<c> (fst(p))) (f (snd(p))) = (f x)
By
Latex:
(D -1 THEN Thin (-1) THEN HypSubst' -1 0 THEN Auto THEN Try ((Fold `power-series` 0 THEN Auto)))
Home
Index