Step
*
1
2
1
1
3
2
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)
⊢ ⋃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:(Folds ``tlp hdp`` 0 THEN BLemma `bag-extensionality-no-repeats` THEN Auto) }
1
.....decidable?.....
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. x1 : bag(X) List+ × bag(X) × bag(X)
18. y : bag(X) List+ × bag(X) × bag(X)
⊢ Dec(x1 = y ∈ (bag(X) List+ × bag(X) × bag(X)))
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)
⊢ bag-no-repeats(bag(X) List+ × bag(X) × bag(X);⋃L∈bag-parts'(eq;b;x).bag-map(λp.<L, p>;bag-partitions(eq;hdp(L)
+ bag-rep(||tlp(L)||;x))))
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)
17. bag-no-repeats(bag(X) List+ × bag(X) × bag(X);⋃L∈bag-parts'(eq;b;x).bag-map(λp.<L, p>;bag-partitions(eq;hdp(L)
+ bag-rep(||tlp(L)||;x))))
⊢ bag-no-repeats(bag(X) List+ × bag(X) × bag(X);bag-map(λ2L1L2.<[hdp(fst(L1L2)) + hdp(snd(L1L2)) /
(tlp(fst(L1L2)) @ tlp(snd(L1L2)))]
, hdp(fst(L1L2)) + bag-rep(||tlp(fst(L1L2))||;x)
, hdp(snd(L1L2)) + bag-rep(||tlp(snd(L1L2))||;x)>;
⋃p∈bag-partitions(eq;b).
bag-parts'(eq;fst(p);x) × bag-parts'(eq;snd(p);x)))
4
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. x1 : bag(X) List+ × bag(X) × bag(X)
18. x1 ↓∈ ⋃L∈bag-parts'(eq;b;x).bag-map(λp.<L, p>;bag-partitions(eq;hdp(L) + bag-rep(||tlp(L)||;x)))
⊢ x1 ↓∈ bag-map(λ2L1L2.<[hdp(fst(L1L2)) + hdp(snd(L1L2)) / (tlp(fst(L1L2)) @ tlp(snd(L1L2)))]
, hdp(fst(L1L2)) + bag-rep(||tlp(fst(L1L2))||;x)
, hdp(snd(L1L2)) + bag-rep(||tlp(snd(L1L2))||;x)>;
⋃p∈bag-partitions(eq;b).bag-parts'(eq;fst(p);x) × bag-parts'(eq;snd(p);x))
5
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. x1 : bag(X) List+ × bag(X) × bag(X)
18. x1 ↓∈ bag-map(λ2L1L2.<[hdp(fst(L1L2)) + hdp(snd(L1L2)) / (tlp(fst(L1L2)) @ tlp(snd(L1L2)))]
, hdp(fst(L1L2)) + bag-rep(||tlp(fst(L1L2))||;x)
, hdp(snd(L1L2)) + bag-rep(||tlp(snd(L1L2))||;x)>;
⋃p∈bag-partitions(eq;b).bag-parts'(eq;fst(p);x) × bag-parts'(eq;snd(p);x))
⊢ x1 ↓∈ ⋃L∈bag-parts'(eq;b;x).bag-map(λp.<L, p>;bag-partitions(eq;hdp(L) + bag-rep(||tlp(L)||;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{} \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:(Folds ``tlp hdp`` 0 THEN BLemma `bag-extensionality-no-repeats` THEN Auto)
Home
Index