---

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

.....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)
BY
{ (RepUR ``neg-bfs zero-bfs`` 0 THEN (RWO  "bag-map-map" 0 THENA Auto) THEN RepUR ``compose`` 0 THEN EqCDA) }

1
.....subterm..... T:t
1: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)
⊢ (λx.<-K 0, x>) = (λs.<0, s>) ∈ (S ⟶ (|K| × S))

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  K  :  Rng
2.  S  :  Type
3.  fs  :  basic-formal-sum(K;S)
4.  b  :  bag(|K|  \mtimes{}  S)
5.  ss  :  bag(S)
6.  fs  =  ((b  +  -(b))  +  0  *  ss)
\mvdash{}  -(0  *  ss)  =  0  *  ss


By

---

Latex:
(RepUR  ``neg-bfs  zero-bfs``  0
  THEN  (RWO    "bag-map-map"  0  THENA  Auto)
  THEN  RepUR  ``compose``  0
  THEN  EqCDA)

---

Home Index