Step
*
1
1
1
1
1
of Lemma
fps-compose-mul
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. x : X
6. g : PowerSeries(X;r)
7. f : PowerSeries(X;r)
8. h : PowerSeries(X;r)
9. ∀L:bag(X) List+. (||L|| ≥ 1 )
10. Assoc(|r|;+r)
11. IsMonoid(|r|;+r;0)
12. Comm(|r|;+r)
13. Comm(|r|;*)
14. Assoc(|r|;*)
15. ∀L:bag(X) List+. (Πa ∈ tl(L). f a ∈ |r|)
16. b : bag(X)
17. ∀p:bag(X) List+ × bag(X) List+
(p ↓∈ ⋃p∈bag-partitions(eq;b).bag-parts'(eq;fst(p);x) × bag-parts'(eq;snd(p);x)
⇒ ((((g (hd(fst(p)) + bag-rep(||tl(fst(p))||;x))) * Πa ∈ tl(fst(p)). f a)
*
((h (hd(snd(p)) + bag-rep(||tl(snd(p))||;x))) * Πa ∈ tl(snd(p)). f a))
= (((g (hd(fst(p)) + bag-rep(||tl(fst(p))||;x))) * Πa ∈ tl(fst(p)). f a)
*
((h (hd(snd(p)) + bag-rep(||tl(snd(p))||;x))) * Πa ∈ tl(snd(p)). f a))
∈ |r|))
⊢ ⋃p∈bag-partitions(eq;b).bag-parts'(eq;fst(p);x) × bag-parts'(eq;snd(p);x)
= bag-map(λ2p.snd(p);⋃p∈bag-partitions(eq;b).bag-map(λp1.<p, p1>;bag-parts'(eq;fst(p);x) × bag-parts'(eq;snd(p);x)))
∈ bag(bag(X) List+ × bag(X) List+)
BY
{ (GenConclAtAddr [2;1]
THEN (GenConcl ⌜λ2p.snd(p) = F ∈ ((Top × bag(X) List+ × bag(X) List+) ⟶ (bag(X) List+ × bag(X) List+))⌝⋅ THENA Auto)
) }
1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. x : X
6. g : PowerSeries(X;r)
7. f : PowerSeries(X;r)
8. h : PowerSeries(X;r)
9. ∀L:bag(X) List+. (||L|| ≥ 1 )
10. Assoc(|r|;+r)
11. IsMonoid(|r|;+r;0)
12. Comm(|r|;+r)
13. Comm(|r|;*)
14. Assoc(|r|;*)
15. ∀L:bag(X) List+. (Πa ∈ tl(L). f a ∈ |r|)
16. b : bag(X)
17. ∀p:bag(X) List+ × bag(X) List+
(p ↓∈ ⋃p∈bag-partitions(eq;b).bag-parts'(eq;fst(p);x) × bag-parts'(eq;snd(p);x)
⇒ ((((g (hd(fst(p)) + bag-rep(||tl(fst(p))||;x))) * Πa ∈ tl(fst(p)). f a)
*
((h (hd(snd(p)) + bag-rep(||tl(snd(p))||;x))) * Πa ∈ tl(snd(p)). f a))
= (((g (hd(fst(p)) + bag-rep(||tl(fst(p))||;x))) * Πa ∈ tl(fst(p)). f a)
*
((h (hd(snd(p)) + bag-rep(||tl(snd(p))||;x))) * Πa ∈ tl(snd(p)). f a))
∈ |r|))
18. v : bag(bag(X) × bag(X))
19. bag-partitions(eq;b) = v ∈ bag(bag(X) × bag(X))
20. F : (Top × bag(X) List+ × bag(X) List+) ⟶ (bag(X) List+ × bag(X) List+)
21. λ2p.snd(p) = F ∈ ((Top × bag(X) List+ × bag(X) List+) ⟶ (bag(X) List+ × bag(X) List+))
⊢ ⋃p∈v.bag-parts'(eq;fst(p);x) × bag-parts'(eq;snd(p);x)
= bag-map(F;⋃p∈v.bag-map(λp1.<p, p1>;bag-parts'(eq;fst(p);x) × bag-parts'(eq;snd(p);x)))
∈ bag(bag(X) List+ × bag(X) List+)
Latex:
Latex:
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. x : X
6. g : PowerSeries(X;r)
7. f : PowerSeries(X;r)
8. h : PowerSeries(X;r)
9. \mforall{}L:bag(X) List\msupplus{}. (||L|| \mgeq{} 1 )
10. Assoc(|r|;+r)
11. IsMonoid(|r|;+r;0)
12. Comm(|r|;+r)
13. Comm(|r|;*)
14. Assoc(|r|;*)
15. \mforall{}L:bag(X) List\msupplus{}. (\mPi{}a \mmember{} tl(L). f a \mmember{} |r|)
16. b : bag(X)
17. \mforall{}p:bag(X) List\msupplus{} \mtimes{} bag(X) List\msupplus{}
(p \mdownarrow{}\mmember{} \mcup{}p\mmember{}bag-partitions(eq;b).bag-parts'(eq;fst(p);x) \mtimes{} bag-parts'(eq;snd(p);x)
{}\mRightarrow{} ((((g (hd(fst(p)) + bag-rep(||tl(fst(p))||;x))) * \mPi{}a \mmember{} tl(fst(p)). f a)
*
((h (hd(snd(p)) + bag-rep(||tl(snd(p))||;x))) * \mPi{}a \mmember{} tl(snd(p)). f a))
= (((g (hd(fst(p)) + bag-rep(||tl(fst(p))||;x))) * \mPi{}a \mmember{} tl(fst(p)). f a)
*
((h (hd(snd(p)) + bag-rep(||tl(snd(p))||;x))) * \mPi{}a \mmember{} tl(snd(p)). f a))))
\mvdash{} \mcup{}p\mmember{}bag-partitions(eq;b).bag-parts'(eq;fst(p);x) \mtimes{} bag-parts'(eq;snd(p);x)
= bag-map(\mlambda{}\msubtwo{}p.snd(p);\mcup{}p\mmember{}bag-partitions(eq;b).
bag-map(\mlambda{}p1.<p, p1>bag-parts'(eq;fst(p);x) \mtimes{} bag-parts'(eq;snd(p);x)))
By
Latex:
(GenConclAtAddr [2;1] THEN (GenConcl \mkleeneopen{}\mlambda{}\msubtwo{}p.snd(p) = F\mkleeneclose{}\mcdot{} THENA Auto))
Home
Index