---

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

.....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)
BY
{ (SubsumeC  ⌜basic-formal-sum(K;S)⌝⋅ THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(SubsumeC    \mkleeneopen{}basic-formal-sum(K;S)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index