---

Step * of Lemma null-formal-sum-append

∀[K:RngSig]. ∀[S:Type]. ∀[fs1,fs2:basic-formal-sum(K;S)].
  (null-formal-sum(K;S;fs1) ⇒ null-formal-sum(K;S;fs2) ⇒ null-formal-sum(K;S;fs1 + fs2))
BY
{ (Auto THEN D -2 THEN D -1 THEN (D 0 With ⌜b + b1⌝  THENA Auto) THEN ExRepD THEN (D 0 With ⌜s1 + ss⌝  THENA Auto)) }

1
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)

---

Latex:

---

Latex:
\mforall{}[K:RngSig].  \mforall{}[S:Type].  \mforall{}[fs1,fs2:basic-formal-sum(K;S)].
    (null-formal-sum(K;S;fs1)  {}\mRightarrow{}  null-formal-sum(K;S;fs2)  {}\mRightarrow{}  null-formal-sum(K;S;fs1  +  fs2))


By

---

Latex:
(Auto
  THEN  D  -2
  THEN  D  -1
  THEN  (D  0  With  \mkleeneopen{}b  +  b1\mkleeneclose{}    THENA  Auto)
  THEN  ExRepD
  THEN  (D  0  With  \mkleeneopen{}s1  +  ss\mkleeneclose{}    THENA  Auto))

---

Home Index