---

Step * 1 1 1 1 1 1 1 2 1 of Lemma sub-free-dim-1


1. K : CRng
2. S : Type
3. a : S
4. u : |K| × S
5. v : (|K| × S) List
6. (∀p:|K| × S. (p ↓∈ v ⇒ ((snd(p)) = a ∈ S))) ⇒ (v = {<Σ(p∈v). fst(p), a>} ∈ formal-sum(K;S))
7. ∀p:|K| × S. (p ↓∈ [u / v] ⇒ ((snd(p)) = a ∈ S))
⊢ [u / v] = {<Σ(p∈[u / v]). fst(p), a>} ∈ formal-sum(K;S)
BY
{ ((Assert [u / v] ~ {u} + v BY Computation) THEN RWO "-1" (-2) THEN RWO "-1" 0 THEN Thin (-1)) }

1
1. K : CRng
2. S : Type
3. a : S
4. u : |K| × S
5. v : (|K| × S) List
6. (∀p:|K| × S. (p ↓∈ v ⇒ ((snd(p)) = a ∈ S))) ⇒ (v = {<Σ(p∈v). fst(p), a>} ∈ formal-sum(K;S))
7. ∀p:|K| × S. (p ↓∈ {u} + v ⇒ ((snd(p)) = a ∈ S))
⊢ ({u} + v) = {<Σ(p∈{u} + v). fst(p), a>} ∈ formal-sum(K;S)

---

Latex:

---

Latex:

1.  K  :  CRng
2.  S  :  Type
3.  a  :  S
4.  u  :  |K|  \mtimes{}  S
5.  v  :  (|K|  \mtimes{}  S)  List
6.  (\mforall{}p:|K|  \mtimes{}  S.  (p  \mdownarrow{}\mmember{}  v  {}\mRightarrow{}  ((snd(p))  =  a)))  {}\mRightarrow{}  (v  =  \{<\mSigma{}(p\mmember{}v).  fst(p),  a>\})
7.  \mforall{}p:|K|  \mtimes{}  S.  (p  \mdownarrow{}\mmember{}  [u  /  v]  {}\mRightarrow{}  ((snd(p))  =  a))
\mvdash{}  [u  /  v]  =  \{<\mSigma{}(p\mmember{}[u  /  v]).  fst(p),  a>\}


By

---

Latex:
((Assert  [u  /  v]  \msim{}  \{u\}  +  v  BY  Computation)  THEN  RWO  "-1"  (-2)  THEN  RWO  "-1"  0  THEN  Thin  (-1))

---

Home Index