Step
*
1
2
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. ∀[f:({L:bag(X) List+| ¬x ↓∈ hd(L)} × {L:bag(X) List+| ¬x ↓∈ hd(L)} ) ⟶ |r|]
∀[b:bag({L:bag(X) List+| ¬x ↓∈ hd(L)} × {L:bag(X) List+| ¬x ↓∈ hd(L)} )]
(Σ(x∈b). f[x]
= Σ(x@0∈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)>;b)). f[let L,b1,b2 = x@0 in
<[(b1|¬x) / firstn(#((b1|x));tl(L))], [(b2|¬x) / nth_tl(#((b1|x));tl(L))]>]
∈ |r|)
supposing ∀x@0:{L:bag(X) List+| ¬x ↓∈ hd(L)} × {L:bag(X) List+| ¬x ↓∈ hd(L)}
(x@0
= let L,b1,b2 = <[hd(fst(x@0)) + hd(snd(x@0)) / (tl(fst(x@0)) @ tl(snd(x@0)))]
, hd(fst(x@0)) + bag-rep(||tl(fst(x@0))||;x)
, hd(snd(x@0)) + bag-rep(||tl(snd(x@0))||;x)> in
<[(b1|¬x) / firstn(#((b1|x));tl(L))], [(b2|¬x) / nth_tl(#((b1|x));tl(L))]>
∈ ({L:bag(X) List+| ¬x ↓∈ hd(L)} × {L:bag(X) List+| ¬x ↓∈ hd(L)} ))
⊢ Σ(p∈⋃L∈bag-parts'(eq;b;x).bag-map(λp.<L, p>;bag-partitions(eq;hd(L) + bag-rep(||tl(L)||;x)))). (* (g (fst(snd(p))))
(h (snd(snd(p)))))
*
Πa ∈ tl(fst(p)). f a
= Σ(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)
∈ |r|
BY
{ (RW (AddrC [3] (HypC (-1))) 0⋅
THEN Try (Complete (Auto))
THEN Thin (-1)
THEN Try ((Using [`T',bag(X) List+ × bag(X) × bag(X)] MemCD⋅ THEN Complete (Auto)))
THEN Try (BackThruSomeHyp)) }
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)
⊢ Σ(p∈⋃L∈bag-parts'(eq;b;x).bag-map(λp.<L, p>;bag-partitions(eq;hd(L) + bag-rep(||tl(L)||;x)))). (* (g (fst(snd(p))))
(h (snd(snd(p)))))
*
Πa ∈ tl(fst(p)). f a
= Σ(p∈⋃L∈bag-parts'(eq;b;x).bag-map(λp.<L, p>;bag-partitions(eq;hd(L) + bag-rep(||tl(L)||;x)))). (* (g (fst(snd(p))))
(h (snd(snd(p)))))
*
Πa ∈ tl(fst(p)). 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)
⊢ ∀x@0:{L:bag(X) List+| ¬x ↓∈ hd(L)} × {L:bag(X) List+| ¬x ↓∈ hd(L)}
(x@0
= let L,b1,b2 = <[hd(fst(x@0)) + hd(snd(x@0)) / (tl(fst(x@0)) @ tl(snd(x@0)))]
, hd(fst(x@0)) + bag-rep(||tl(fst(x@0))||;x)
, hd(snd(x@0)) + bag-rep(||tl(snd(x@0))||;x)> in
<[(b1|¬x) / firstn(#((b1|x));tl(L))], [(b2|¬x) / nth_tl(#((b1|x));tl(L))]>
∈ ({L:bag(X) List+| ¬x ↓∈ hd(L)} × {L:bag(X) List+| ¬x ↓∈ hd(L)} ))
3
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)
⊢ Σ(p∈⋃L∈bag-parts'(eq;b;x).bag-map(λp.<L, p>;bag-partitions(eq;hd(L) + bag-rep(||tl(L)||;x)))). (* (g (fst(snd(p))))
(h (snd(snd(p)))))
*
Πa ∈ tl(fst(p)). f a
= Σ(x@0∈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)))
((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|
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{}[f:(\{L:bag(X) List\msupplus{}| \mneg{}x \mdownarrow{}\mmember{} hd(L)\} \mtimes{} \{L:bag(X) List\msupplus{}| \mneg{}x \mdownarrow{}\mmember{} hd(L)\} ) {}\mrightarrow{} |r|]
\mforall{}[b:bag(\{L:bag(X) List\msupplus{}| \mneg{}x \mdownarrow{}\mmember{} hd(L)\} \mtimes{} \{L:bag(X) List\msupplus{}| \mneg{}x \mdownarrow{}\mmember{} hd(L)\} )]
(\mSigma{}(x\mmember{}b). f[x]
= \mSigma{}(x@0\mmember{}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)>b)). f[let L,b1,b2 = \000Cx@0 in
<[(b1|\mneg{}x) / firstn(\#((b1|x));tl(L))], [(b2|\mneg{}x) / nth\_tl(\#((b1|x));tl(L))]>])
supposing \mforall{}x@0:\{L:bag(X) List\msupplus{}| \mneg{}x \mdownarrow{}\mmember{} hd(L)\} \mtimes{} \{L:bag(X) List\msupplus{}| \mneg{}x \mdownarrow{}\mmember{} hd(L)\}
(x@0
= let L,b1,b2 = <[hd(fst(x@0)) + hd(snd(x@0)) / (tl(fst(x@0)) @ tl(snd(x@0)))]
, hd(fst(x@0)) + bag-rep(||tl(fst(x@0))||;x)
, hd(snd(x@0)) + bag-rep(||tl(snd(x@0))||;x)> in
<[(b1|\mneg{}x) / firstn(\#((b1|x));tl(L))], [(b2|\mneg{}x) / nth\_tl(\#((b1|x));tl(L))]>)
\mvdash{} \mSigma{}(p\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))))
(* (g (fst(snd(p)))) (h (snd(snd(p))))) * \mPi{}a \mmember{} tl(fst(p)). f a
= \mSigma{}(p\mmember{}\mcup{}p\mmember{}bag-partitions(eq;b).bag-parts'(eq;fst(p);x) \mtimes{} bag-parts'(eq;snd(p);x))
((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)
By
Latex:
(RW (AddrC [3] (HypC (-1))) 0\mcdot{}
THEN Try (Complete (Auto))
THEN Thin (-1)
THEN Try ((Using [`T',bag(X) List\msupplus{} \mtimes{} bag(X) \mtimes{} bag(X)] MemCD\mcdot{} THEN Complete (Auto)))
THEN Try (BackThruSomeHyp))
Home
Index