Step
*
1
2
1
1
3
2
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)
⊢ (∀x@0:bag(X) List+ × bag(X) × bag(X)
(x@0 ↓∈ ⋃L∈bag-parts'(eq;b;x).bag-map(λp.<L, p>;bag-partitions(eq;hd(L) + bag-rep(||tl(L)||;x)))
⇒ (((* (g (fst(snd(x@0)))) (h (snd(snd(x@0))))) * Πa ∈ tl(fst(x@0)). f a)
= (((g
(hd(fst(let L,b1,b2 = x@0 in
<[(b1|¬x) / firstn(#((b1|x));tl(L))], [(b2|¬x) / nth_tl(#((b1|x));tl(L))]>))
+ bag-rep(||tl(fst(let L,b1,b2 = x@0 in
<[(b1|¬x) / firstn(#((b1|x));tl(L))], [(b2|¬x) / nth_tl(#((b1|x));tl(L))]>))||;x)))
*
Πa ∈ tl(fst(let L,b1,b2 = x@0 in
<[(b1|¬x) / firstn(#((b1|x));tl(L))], [(b2|¬x) / nth_tl(#((b1|x));tl(L))]>)). f a)
*
((h
(hd(snd(let L,b1,b2 = x@0 in
<[(b1|¬x) / firstn(#((b1|x));tl(L))], [(b2|¬x) / nth_tl(#((b1|x));tl(L))]>))
+ bag-rep(||tl(snd(let L,b1,b2 = x@0 in
<[(b1|¬x) / firstn(#((b1|x));tl(L))], [(b2|¬x) / nth_tl(#((b1|x));tl(L))]>))||;x)))
*
Πa ∈ tl(snd(let L,b1,b2 = x@0 in
<[(b1|¬x) / firstn(#((b1|x));tl(L))], [(b2|¬x) / nth_tl(#((b1|x));tl(L))]>)). f a))
∈ |r|)))
∧ (⋃L∈bag-parts'(eq;b;x).bag-map(λp.<L, p>;bag-partitions(eq;hd(L) + bag-rep(||tl(L)||;x)))
= bag-map(λ2L1L2.<[hd(fst(L1L2)) + hd(snd(L1L2)) / (tl(fst(L1L2)) @ tl(snd(L1L2)))]
, hd(fst(L1L2)) + bag-rep(||tl(fst(L1L2))||;x)
, hd(snd(L1L2)) + bag-rep(||tl(snd(L1L2))||;x)>;
⋃p∈bag-partitions(eq;b).bag-parts'(eq;fst(p);x) × bag-parts'(eq;snd(p);x))
∈ bag(bag(X) List+ × bag(X) × bag(X)))
BY
{ TACTIC:D 0 }
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)
⊢ ∀x@0:bag(X) List+ × bag(X) × bag(X)
(x@0 ↓∈ ⋃L∈bag-parts'(eq;b;x).bag-map(λp.<L, p>;bag-partitions(eq;hd(L) + bag-rep(||tl(L)||;x)))
⇒ (((* (g (fst(snd(x@0)))) (h (snd(snd(x@0))))) * Πa ∈ tl(fst(x@0)). f a)
= (((g
(hd(fst(let L,b1,b2 = x@0 in
<[(b1|¬x) / firstn(#((b1|x));tl(L))], [(b2|¬x) / nth_tl(#((b1|x));tl(L))]>))
+ bag-rep(||tl(fst(let L,b1,b2 = x@0 in
<[(b1|¬x) / firstn(#((b1|x));tl(L))], [(b2|¬x) / nth_tl(#((b1|x));tl(L))]>))||;x)))
*
Πa ∈ tl(fst(let L,b1,b2 = x@0 in
<[(b1|¬x) / firstn(#((b1|x));tl(L))], [(b2|¬x) / nth_tl(#((b1|x));tl(L))]>)). f a)
*
((h
(hd(snd(let L,b1,b2 = x@0 in
<[(b1|¬x) / firstn(#((b1|x));tl(L))], [(b2|¬x) / nth_tl(#((b1|x));tl(L))]>))
+ bag-rep(||tl(snd(let L,b1,b2 = x@0 in
<[(b1|¬x) / firstn(#((b1|x));tl(L))], [(b2|¬x) / nth_tl(#((b1|x));tl(L))]>))||;x)))
*
Πa ∈ tl(snd(let L,b1,b2 = x@0 in
<[(b1|¬x) / firstn(#((b1|x));tl(L))], [(b2|¬x) / nth_tl(#((b1|x));tl(L))]>)). f a))
∈ |r|))
2
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)
⊢ ⋃L∈bag-parts'(eq;b;x).bag-map(λp.<L, p>;bag-partitions(eq;hd(L) + bag-rep(||tl(L)||;x)))
= bag-map(λ2L1L2.<[hd(fst(L1L2)) + hd(snd(L1L2)) / (tl(fst(L1L2)) @ tl(snd(L1L2)))]
, hd(fst(L1L2)) + bag-rep(||tl(fst(L1L2))||;x)
, hd(snd(L1L2)) + bag-rep(||tl(snd(L1L2))||;x)>;
⋃p∈bag-partitions(eq;b).bag-parts'(eq;fst(p);x) × bag-parts'(eq;snd(p);x))
∈ bag(bag(X) List+ × bag(X) × bag(X))
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)
\mvdash{} (\mforall{}x@0:bag(X) List\msupplus{} \mtimes{} bag(X) \mtimes{} bag(X)
(x@0 \mdownarrow{}\mmember{} \mcup{}L\mmember{}bag-parts'(eq;b;x).bag-map(\mlambda{}p.<L, p>bag-partitions(eq;hd(L)
+ bag-rep(||tl(L)||;x)))
{}\mRightarrow{} (((* (g (fst(snd(x@0)))) (h (snd(snd(x@0))))) * \mPi{}a \mmember{} tl(fst(x@0)). f a)
= (((g
(hd(fst(let L,b1,b2 = x@0 in
<[(b1|\mneg{}x) / firstn(\#((b1|x));tl(L))], [(b2|\mneg{}x) / nth\_tl(\#((b1|x));tl(L))]>))
+ bag-rep(||tl(fst(let L,b1,b2 = x@0 in
<[(b1|\mneg{}x) / firstn(\#((b1|x));tl(L))], [(b2|\mneg{}x) / nth\_tl(\#((b1|x));tl(L))]>))||;x)))
*
\mPi{}a \mmember{} tl(fst(let L,b1,b2 = x@0 in
<[(b1|\mneg{}x) / firstn(\#((b1|x));tl(L))], [(b2|\mneg{}x) / nth\_tl(\#((b1|x));tl(L))]>)). f a)
*
((h
(hd(snd(let L,b1,b2 = x@0 in
<[(b1|\mneg{}x) / firstn(\#((b1|x));tl(L))], [(b2|\mneg{}x) / nth\_tl(\#((b1|x));tl(L))]>))
+ bag-rep(||tl(snd(let L,b1,b2 = x@0 in
<[(b1|\mneg{}x) / firstn(\#((b1|x));tl(L))], [(b2|\mneg{}x) / nth\_tl(\#((b1|x));tl(L))]>))||;x)))
*
\mPi{}a \mmember{} tl(snd(let L,b1,b2 = x@0 in
<[(b1|\mneg{}x) / firstn(\#((b1|x));tl(L))], [(b2|\mneg{}x) / nth\_tl(\#((b1|x));tl(L))]>)). f a)))))
\mwedge{} (\mcup{}L\mmember{}bag-parts'(eq;b;x).bag-map(\mlambda{}p.<L, p>bag-partitions(eq;hd(L) + bag-rep(||tl(L)||;x)))
= bag-map(\mlambda{}\msubtwo{}L1L2.<[hd(fst(L1L2)) + hd(snd(L1L2)) / (tl(fst(L1L2)) @ tl(snd(L1L2)))]
, hd(fst(L1L2)) + bag-rep(||tl(fst(L1L2))||;x)
, hd(snd(L1L2)) + bag-rep(||tl(snd(L1L2))||;x)>
\mcup{}p\mmember{}bag-partitions(eq;b).bag-parts'(eq;fst(p);x) \mtimes{} bag-parts'(eq;snd(p);x)))
By
Latex:
TACTIC:D 0
Home
Index