---

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


1. K : RngSig
2. S : Type
3. fs1 : basic-formal-sum(K;S)
4. fs2 : basic-formal-sum(K;S)
5. b : bag(|K| × S)
6. s1 : bag(S)
7. fs1 = ((b + -(b)) + 0 * s1) ∈ bag(|K| × S)
8. b1 : bag(|K| × S)
9. ss : bag(S)
10. fs2 = ((b1 + -(b1)) + 0 * ss) ∈ bag(|K| × S)
⊢ (fs1 + fs2) = (((b + b1) + -(b + b1)) + 0 * s1 + ss) ∈ bag(|K| × S)
BY
{ (RWO "-4 -1 zero-bfs-append neg-bfs-append" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  K  :  RngSig
2.  S  :  Type
3.  fs1  :  basic-formal-sum(K;S)
4.  fs2  :  basic-formal-sum(K;S)
5.  b  :  bag(|K|  \mtimes{}  S)
6.  s1  :  bag(S)
7.  fs1  =  ((b  +  -(b))  +  0  *  s1)
8.  b1  :  bag(|K|  \mtimes{}  S)
9.  ss  :  bag(S)
10.  fs2  =  ((b1  +  -(b1))  +  0  *  ss)
\mvdash{}  (fs1  +  fs2)  =  (((b  +  b1)  +  -(b  +  b1))  +  0  *  s1  +  ss)


By

---

Latex:
(RWO  "-4  -1  zero-bfs-append  neg-bfs-append"  0  THEN  Auto)

---

Home Index