---

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


1. S : Type
2. K : CRng
3. x : basic-formal-sum(K;S)
4. k : |K|
5. b : bag(|K| × S)
6. ss : bag(S)
7. x = ((b + -(b)) + 0 * ss) ∈ bag(|K| × S)
8. x1 : |K| × S
⊢ ((λx.let k',s = let k,s = x in <-K k, s> in <k * k', s>) x1)
= ((λx.let k,s = let k',s = x in <k * k', s> in <-K k, s>) x1)
∈ (|K| × S)
BY
{ ((D -1 THEN Reduce 0) THEN EqCDA THEN Auto) }

---

Latex:

---

Latex:

1.  S  :  Type
2.  K  :  CRng
3.  x  :  basic-formal-sum(K;S)
4.  k  :  |K|
5.  b  :  bag(|K|  \mtimes{}  S)
6.  ss  :  bag(S)
7.  x  =  ((b  +  -(b))  +  0  *  ss)
8.  x1  :  |K|  \mtimes{}  S
\mvdash{}  ((\mlambda{}x.let  k',s  =  let  k,s  =  x  in  <-K  k,  s>  in  <k  *  k',  s>)  x1)
=  ((\mlambda{}x.let  k,s  =  let  k',s  =  x  in  <k  *  k',  s>  in  <-K  k,  s>)  x1)


By

---

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

---

Home Index