Step
*
1
2
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)
⊢ Σ(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
{ TACTIC:(InstLemma `bag-summation-reindex` [⌜|r|⌝;⌜+r⌝;⌜0⌝;⌜{L:bag(X) List+| ¬x ↓∈ hd(L)} × {L:bag(X) List+|
¬x ↓∈ hd(L)} ⌝;
⌜{L:bag(X) List+| ¬x ↓∈ hd(L)} × bag(X) × bag(X)⌝;⌜λ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)>⌝;
⌜λ2Lp.let L,b1,b2 = Lp in
<[(b1|¬x) / firstn(#((b1|x));tl(L))], [(b2|¬x) / nth_tl(#((b1|x));tl(L))]>⌝]⋅
THENA (Auto
THEN (MemTypeCD
THEN Auto
THEN Reduce 0
THEN TACTIC:((D 0 THENM BagMemberD (-1))
THEN Auto
THEN D (-2)
THEN DSetVars
THEN Reduce (-1)
THEN ((RepeatFor 2 (D -1) THEN Auto)
ORELSE ((RW assert_pushdownC (-1) THENA Auto) THEN D -1 THEN 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. ∀[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|
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{} \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:
TACTIC:(InstLemma `bag-summation-reindex` [\mkleeneopen{}|r|\mkleeneclose{};\mkleeneopen{}+r\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};
\mkleeneopen{}\{L:bag(X) List\msupplus{}| \mneg{}x \mdownarrow{}\mmember{} hd(L)\} \mtimes{} \{L:bag(X) List\msupplus{}| \mneg{}x \mdownarrow{}\mmember{} hd(L)\} \mkleeneclose{};\mkleeneopen{}\{L:bag(X) List\msupplus{}|
\mneg{}x \mdownarrow{}\mmember{} hd(L)\}
\mtimes{} bag(X)
\mtimes{} bag(X)\mkleeneclose{};
\mkleeneopen{}\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)>\mkleeneclose{}; \mkleeneopen{}\mlambda{}\msubtwo{}Lp.let L,b1,b2 = Lp in
<[(b1|\mneg{}x) / firstn(\#((b1|x));tl(L))]
, [(b2|\mneg{}x) / nth\_tl(\#((b1|x));tl(L))]
>\mkleeneclose{}]\mcdot{}
THENA (Auto
THEN (MemTypeCD
THEN Auto
THEN Reduce 0
THEN TACTIC:((D 0 THENM BagMemberD (-1))
THEN Auto
THEN D (-2)
THEN DSetVars
THEN Reduce (-1)
THEN ((RepeatFor 2 (D -1) THEN Auto)
ORELSE ((RW assert\_pushdownC (-1) THENA Auto) THEN D -1 THEN Auto)
)))\mcdot{}
)
)\mcdot{}
Home
Index