---

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

.....wf..... 
1. K : CRng
2. S : Type
3. L : (|K| × S) List
4. b : bag(|K| × S)
5. a : S
6. ∀p:|K| × S. (p ↓∈ L ⇒ ((snd(p)) = a ∈ S))
7. b = L ∈ bag(|K| × S)
8. z : bag(|K| × S)
⊢ z = {<Σ(p∈z). fst(p), a>} ∈ formal-sum(K;S) ∈ ℙ
BY
{ MemCD }

1
.....subterm..... T:t
1:n
1. K : CRng
2. S : Type
3. L : (|K| × S) List
4. b : bag(|K| × S)
5. a : S
6. ∀p:|K| × S. (p ↓∈ L ⇒ ((snd(p)) = a ∈ S))
7. b = L ∈ bag(|K| × S)
8. z : bag(|K| × S)
⊢ formal-sum(K;S) ∈ Type

2
.....subterm..... T:t
2:n
1. K : CRng
2. S : Type
3. L : (|K| × S) List
4. b : bag(|K| × S)
5. a : S
6. ∀p:|K| × S. (p ↓∈ L ⇒ ((snd(p)) = a ∈ S))
7. b = L ∈ bag(|K| × S)
8. z : bag(|K| × S)
⊢ z ∈ formal-sum(K;S)

3
.....subterm..... T:t
3:n
1. K : CRng
2. S : Type
3. L : (|K| × S) List
4. b : bag(|K| × S)
5. a : S
6. ∀p:|K| × S. (p ↓∈ L ⇒ ((snd(p)) = a ∈ S))
7. b = L ∈ bag(|K| × S)
8. z : bag(|K| × S)
⊢ {<Σ(p∈z). fst(p), a>} ∈ formal-sum(K;S)

---

Latex:

---

Latex:
.....wf..... 
1.  K  :  CRng
2.  S  :  Type
3.  L  :  (|K|  \mtimes{}  S)  List
4.  b  :  bag(|K|  \mtimes{}  S)
5.  a  :  S
6.  \mforall{}p:|K|  \mtimes{}  S.  (p  \mdownarrow{}\mmember{}  L  {}\mRightarrow{}  ((snd(p))  =  a))
7.  b  =  L
8.  z  :  bag(|K|  \mtimes{}  S)
\mvdash{}  z  =  \{<\mSigma{}(p\mmember{}z).  fst(p),  a>\}  \mmember{}  \mBbbP{}


By

---

Latex:
MemCD

---

Home Index