---

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


1. K : CRng
2. S : Type
3. b : bag(|K| × S)
4. a : S
5. ∀p:|K| × S. (p ↓∈ b ⇒ ((snd(p)) = a ∈ S))
⊢ b = {<Σ(p∈b). fst(p), a>} ∈ formal-sum(K;S)
BY
{ (BagInd 3 THEN Try (QuickAuto)) }

1
1. K : CRng
2. S : Type
3. a : S
⊢ (∀p:|K| × S. (p ↓∈ [] ⇒ ((snd(p)) = a ∈ S))) ⇒ ([] = {<Σ(p∈[]). fst(p), a>} ∈ formal-sum(K;S))

2
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))
⊢ (∀p:|K| × S. (p ↓∈ [u / v] ⇒ ((snd(p)) = a ∈ S))) ⇒ ([u / v] = {<Σ(p∈[u / v]). fst(p), a>} ∈ formal-sum(K;S))

3
.....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) ∈ ℙ

---

Latex:

---

Latex:

1.  K  :  CRng
2.  S  :  Type
3.  b  :  bag(|K|  \mtimes{}  S)
4.  a  :  S
5.  \mforall{}p:|K|  \mtimes{}  S.  (p  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  ((snd(p))  =  a))
\mvdash{}  b  =  \{<\mSigma{}(p\mmember{}b).  fst(p),  a>\}


By

---

Latex:
(BagInd  3  THEN  Try  (QuickAuto))

---

Home Index