---

Step * 1 1 of Lemma mset_sum_assoc

.....antecedent..... 
1. s : DSet
2. as : |s| List
3. bs : |s| List
4. as ≡(|s|) bs
5. v : |s| List
6. v1 : |s| List
7. v ≡(|s|) v1
8. v2 : |s| List
9. v3 : |s| List
10. v2 ≡(|s|) v3
⊢ (as @ v @ v2) ≡(|s|) ((bs @ v1) @ v3)
BY
{ (RWW "4 7 10" 0 THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  s  :  DSet
2.  as  :  |s|  List
3.  bs  :  |s|  List
4.  as  \mequiv{}(|s|)  bs
5.  v  :  |s|  List
6.  v1  :  |s|  List
7.  v  \mequiv{}(|s|)  v1
8.  v2  :  |s|  List
9.  v3  :  |s|  List
10.  v2  \mequiv{}(|s|)  v3
\mvdash{}  (as  @  v  @  v2)  \mequiv{}(|s|)  ((bs  @  v1)  @  v3)


By

---

Latex:
(RWW  "4  7  10"  0  THEN  Auto)

---

Home Index