---

Step * 1 of Lemma formal-sum-mul-mul


1. S : Type
2. K : CRng
3. k : |K|
4. b : |K|
5. x : bag(|K| × S)
⊢ bag-map(λx.let k',s = let k',s = x 
                        in <b * k', s> 
             in <k * k', s>;x)
= bag-map(λp.let k',s = p 
             in <(k * b) * k', s>;x)
∈ bag(|K| × S)
BY
{ (EqCDA THEN (FunExt THENA Auto) THEN D -1 THEN Reduce 0 THEN EqCD THEN Auto) }

---

Latex:

---

Latex:

1.  S  :  Type
2.  K  :  CRng
3.  k  :  |K|
4.  b  :  |K|
5.  x  :  bag(|K|  \mtimes{}  S)
\mvdash{}  bag-map(\mlambda{}x.let  k',s  =  let  k',s  =  x 
                                                in  <b  *  k',  s> 
                          in  <k  *  k',  s>x)
=  bag-map(\mlambda{}p.let  k',s  =  p 
                          in  <(k  *  b)  *  k',  s>x)


By

---

Latex:
(EqCDA  THEN  (FunExt  THENA  Auto)  THEN  D  -1  THEN  Reduce  0  THEN  EqCD  THEN  Auto)

---

Home Index