---

Step * 1 of Lemma fps-mul-single-general


1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. c : bag(X)
6. f : PowerSeries(X;r)
7. Comm(|r|;+r)
8. IsMonoid(|r|;+r;0)
9. b : bag(X)@i
10. x : bag(X)@i
11. b = (c + x) ∈ bag(X)
⊢ Σ(p∈bag-partitions(eq;b)). * (<c> (fst(p))) (f (snd(p))) = (f x) ∈ |r|
BY
{ TACTIC:((InstLemma `bag-partitions-with-one-given` [⌜X⌝;⌜eq⌝;⌜c⌝;⌜x⌝;⌜b⌝]⋅ THENA Auto)
          THEN Assert ⌜Σ(p∈[p∈bag-partitions(eq;b)|bag-eq(eq;fst(p);c)]). * (<c> (fst(p))) (f (snd(p))) = (f x) ∈ |r|⌝⋅
          ) }

1
.....assertion..... 
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. c : bag(X)
6. f : PowerSeries(X;r)
7. Comm(|r|;+r)
8. IsMonoid(|r|;+r;0)
9. b : bag(X)@i
10. x : bag(X)@i
11. b = (c + x) ∈ bag(X)
12. ([p∈bag-partitions(eq;b)|bag-eq(eq;fst(p);c)] = {<c, x>} ∈ bag(bag(X) × bag(X)))
∧ ([p∈bag-partitions(eq;b)|bag-eq(eq;snd(p);x)] = {<c, x>} ∈ bag(bag(X) × bag(X)))
⊢ Σ(p∈[p∈bag-partitions(eq;b)|bag-eq(eq;fst(p);c)]). * (<c> (fst(p))) (f (snd(p))) = (f x) ∈ |r|

2
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. c : bag(X)
6. f : PowerSeries(X;r)
7. Comm(|r|;+r)
8. IsMonoid(|r|;+r;0)
9. b : bag(X)@i
10. x : bag(X)@i
11. b = (c + x) ∈ bag(X)
12. ([p∈bag-partitions(eq;b)|bag-eq(eq;fst(p);c)] = {<c, x>} ∈ bag(bag(X) × bag(X)))
∧ ([p∈bag-partitions(eq;b)|bag-eq(eq;snd(p);x)] = {<c, x>} ∈ bag(bag(X) × bag(X)))
13. Σ(p∈[p∈bag-partitions(eq;b)|bag-eq(eq;fst(p);c)]). * (<c> (fst(p))) (f (snd(p))) = (f x) ∈ |r|
⊢ Σ(p∈bag-partitions(eq;b)). * (<c> (fst(p))) (f (snd(p))) = (f x) ∈ |r|

---

Latex:

---

Latex:

1.  X  :  Type
2.  valueall-type(X)
3.  eq  :  EqDecider(X)
4.  r  :  CRng
5.  c  :  bag(X)
6.  f  :  PowerSeries(X;r)
7.  Comm(|r|;+r)
8.  IsMonoid(|r|;+r;0)
9.  b  :  bag(X)@i
10.  x  :  bag(X)@i
11.  b  =  (c  +  x)
\mvdash{}  \mSigma{}(p\mmember{}bag-partitions(eq;b)).  *  (<c>  (fst(p)))  (f  (snd(p)))  =  (f  x)


By

---

Latex:
TACTIC:((InstLemma  `bag-partitions-with-one-given`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  Assert  \mkleeneopen{}\mSigma{}(p\mmember{}[p\mmember{}bag-partitions(eq;b)|bag-eq(eq;fst(p);c)]).  *  (<c>  (fst(p))) 
                                                                                                                                                (f  (snd(p)))
                                          =  (f  x)\mkleeneclose{}\mcdot{}
                )

---

Home Index