---

Step * of Lemma null-formal-sum-neg

∀K:Rng. ∀[S:Type]. ∀[fs:basic-formal-sum(K;S)].  (null-formal-sum(K;S;fs) ⇒ null-formal-sum(K;S;-(fs)))
BY
{ (Auto
   THEN D -1
   THEN ExRepD
   THEN (RWW  "-1 neg-bfs-append" 0 THENA Auto)
   THEN (D 0 With ⌜-(b)⌝  THEN Auto)
   THEN D 0 With ⌜ss⌝ 
   THEN Auto
   THEN EqCDA) }

1
.....subterm..... T:t
2:n
1. K : Rng
2. S : Type
3. fs : basic-formal-sum(K;S)
4. b : bag(|K| × S)
5. ss : bag(S)
6. fs = ((b + -(b)) + 0 * ss) ∈ bag(|K| × S)
⊢ -(0 * ss) = 0 * ss ∈ bag(|K| × S)

---

Latex:

---

Latex:
\mforall{}K:Rng
    \mforall{}[S:Type].  \mforall{}[fs:basic-formal-sum(K;S)].    (null-formal-sum(K;S;fs)  {}\mRightarrow{}  null-formal-sum(K;S;-(fs)))


By

---

Latex:
(Auto
  THEN  D  -1
  THEN  ExRepD
  THEN  (RWW    "-1  neg-bfs-append"  0  THENA  Auto)
  THEN  (D  0  With  \mkleeneopen{}-(b)\mkleeneclose{}    THEN  Auto)
  THEN  D  0  With  \mkleeneopen{}ss\mkleeneclose{} 
  THEN  Auto
  THEN  EqCDA)

---

Home Index