---

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


1. K : CRng
2. S : Type
3. T : Type
4. strong-subtype(T;S)
5. ∀x,y:T.  (x = y ∈ T)
6. s : T
7. x : Point(free-vs(K;S))
8. fs-in-subtype(K;S;T;x)
9. b : basic-formal-sum(K;S)
10. x = b ∈ formal-sum(K;S)
11. bfs-predicate(K;S;p.snd(p) ∈ T;b)
12. k : |K|
13. b = {<k, s>} ∈ Point(free-vs(K;S))
14. k1 : |K|
⊢ bag(|K| × T) ⊆r Point(free-vs(K;S))
BY
{ (RepUR ``free-vs vs-point mk-vs`` 0
   THEN (D 0 THENA Auto)
   THEN SubsumeC  ⌜basic-formal-sum(K;S)⌝⋅
   THEN Auto
   THEN SubsumeC ⌜basic-formal-sum(K;T)⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  K  :  CRng
2.  S  :  Type
3.  T  :  Type
4.  strong-subtype(T;S)
5.  \mforall{}x,y:T.    (x  =  y)
6.  s  :  T
7.  x  :  Point(free-vs(K;S))
8.  fs-in-subtype(K;S;T;x)
9.  b  :  basic-formal-sum(K;S)
10.  x  =  b
11.  bfs-predicate(K;S;p.snd(p)  \mmember{}  T;b)
12.  k  :  |K|
13.  b  =  \{<k,  s>\}
14.  k1  :  |K|
\mvdash{}  bag(|K|  \mtimes{}  T)  \msubseteq{}r  Point(free-vs(K;S))


By

---

Latex:
(RepUR  ``free-vs  vs-point  mk-vs``  0
  THEN  (D  0  THENA  Auto)
  THEN  SubsumeC    \mkleeneopen{}basic-formal-sum(K;S)\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  SubsumeC  \mkleeneopen{}basic-formal-sum(K;T)\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index