---

Step * 1 1 1 1 1 1 1 3 1 of Lemma sub-free-dim-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
BY
{ Auto }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
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{}  formal-sum(K;S)  \mmember{}  Type


By

---

Latex:
Auto

---

Home Index