---

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

.....assertion..... 
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)
⊢ ∃k:|K|. (b = {<k, s>} ∈ Point(free-vs(K;S)))
BY
{ (D 0 With ⌜Σ(p∈b). fst(p)⌝ 
   THEN (RepUR ``vs-point free-vs mk-vs`` 0 THEN Auto)
   THEN Try ((D 0 THEN Reduce 0 THEN Auto))) }

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)
⊢ b = {<Σ(p∈b). fst(p), s>} ∈ formal-sum(K;S)

---

Latex:

---

Latex:
.....assertion..... 
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)
\mvdash{}  \mexists{}k:|K|.  (b  =  \{<k,  s>\})


By

---

Latex:
(D  0  With  \mkleeneopen{}\mSigma{}(p\mmember{}b).  fst(p)\mkleeneclose{} 
  THEN  (RepUR  ``vs-point  free-vs  mk-vs``  0  THEN  Auto)
  THEN  Try  ((D  0  THEN  Reduce  0  THEN  Auto)))

---

Home Index