---

Step * 1 of Lemma fs-in-subtype-subspace


1. K : CRng
2. S : Type
3. T : Type
4. strong-subtype(T;S)
5. T ⊆r S
6. respects-equality(S;T)
7. ∀[a,b:S].  (a = b ∈ T ∈ ℙ)
⊢ fs-in-subtype(K;S;T;0)
BY
{ ((Subst' 0 ~ {} 0 THENA Computation)
   THEN (Assert {} ∈ basic-formal-sum(K;S) BY
               (Unfold `basic-formal-sum` 0 THEN Auto))
   THEN RepUR ``fs-in-subtype fs-predicate`` 0
   THEN D 0
   THEN D 0 With ⌜{}⌝ 
   THEN Try (Complete (Auto))
   THEN RepUR ``bfs-predicate`` 0
   THEN Auto
   THEN BagMemberD (-1)) }

---

Latex:

---

Latex:

1.  K  :  CRng
2.  S  :  Type
3.  T  :  Type
4.  strong-subtype(T;S)
5.  T  \msubseteq{}r  S
6.  respects-equality(S;T)
7.  \mforall{}[a,b:S].    (a  =  b  \mmember{}  \mBbbP{})
\mvdash{}  fs-in-subtype(K;S;T;0)


By

---

Latex:
((Subst'  0  \msim{}  \{\}  0  THENA  Computation)
  THEN  (Assert  \{\}  \mmember{}  basic-formal-sum(K;S)  BY
                          (Unfold  `basic-formal-sum`  0  THEN  Auto))
  THEN  RepUR  ``fs-in-subtype  fs-predicate``  0
  THEN  D  0
  THEN  D  0  With  \mkleeneopen{}\{\}\mkleeneclose{} 
  THEN  Try  (Complete  (Auto))
  THEN  RepUR  ``bfs-predicate``  0
  THEN  Auto
  THEN  BagMemberD  (-1))

---

Home Index