---

Step * of Lemma free-vs-subtype

No Annotations
∀[S,T:Type].  ∀[K:CRng]. (Point(free-vs(K;S)) ⊆r Point(free-vs(K;T))) supposing S ⊆r T
BY
{ (Auto
   THEN (Assert basic-formal-sum(K;S) ⊆r basic-formal-sum(K;T) BY
               (RepUR ``basic-formal-sum`` 0 THEN Auto))
   THEN (D 0 THENA Auto)
   THEN All (RepUR ``free-vs vs-point mk-vs``)
   THEN D -1
   THEN EqTypeCD
   THEN Auto
   THEN InstLemma `bfs-equiv-implies` [⌜S⌝;⌜K⌝;⌜λa,b. bfs-equiv(K;T;a;b)⌝]⋅
   THEN Reduce 0
   THEN Try (Complete (Auto))) }

1
1. S : Type
2. T : Type
3. S ⊆r T
4. K : CRng
5. basic-formal-sum(K;S) ⊆r basic-formal-sum(K;T)
6. x : Base
7. x1 : Base
8. x = x1 ∈ (a,b:basic-formal-sum(K;S)//bfs-equiv(K;S;a;b))
9. x ∈ basic-formal-sum(K;S)
10. x1 ∈ basic-formal-sum(K;S)
11. bfs-equiv(K;S;x;x1)
⊢ ∀x,y:basic-formal-sum(K;S).  (bfs-reduce(K;S;x;y) ⇒ bfs-equiv(K;T;x;y))

2
1. S : Type
2. T : Type
3. S ⊆r T
4. K : CRng
5. basic-formal-sum(K;S) ⊆r basic-formal-sum(K;T)
6. x : Base
7. x1 : Base
8. x = x1 ∈ (a,b:basic-formal-sum(K;S)//bfs-equiv(K;S;a;b))
9. x ∈ basic-formal-sum(K;S)
10. x1 ∈ basic-formal-sum(K;S)
11. bfs-equiv(K;S;x;x1)
⊢ EquivRel(basic-formal-sum(K;S);x,y.bfs-equiv(K;T;x;y))

3
1. S : Type
2. T : Type
3. S ⊆r T
4. K : CRng
5. basic-formal-sum(K;S) ⊆r basic-formal-sum(K;T)
6. x : Base
7. x1 : Base
8. x = x1 ∈ (a,b:basic-formal-sum(K;S)//bfs-equiv(K;S;a;b))
9. x ∈ basic-formal-sum(K;S)
10. x1 ∈ basic-formal-sum(K;S)
11. bfs-equiv(K;S;x;x1)
12. ∀x,y:basic-formal-sum(K;S).  (bfs-equiv(K;S;x;y) ⇒ ((λa,b. bfs-equiv(K;T;a;b)) x y))
⊢ bfs-equiv(K;T;x;x1)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[S,T:Type].    \mforall{}[K:CRng].  (Point(free-vs(K;S))  \msubseteq{}r  Point(free-vs(K;T)))  supposing  S  \msubseteq{}r  T


By

---

Latex:
(Auto
  THEN  (Assert  basic-formal-sum(K;S)  \msubseteq{}r  basic-formal-sum(K;T)  BY
                          (RepUR  ``basic-formal-sum``  0  THEN  Auto))
  THEN  (D  0  THENA  Auto)
  THEN  All  (RepUR  ``free-vs  vs-point  mk-vs``)
  THEN  D  -1
  THEN  EqTypeCD
  THEN  Auto
  THEN  InstLemma  `bfs-equiv-implies`  [\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}\mlambda{}a,b.  bfs-equiv(K;T;a;b)\mkleeneclose{}]\mcdot{}
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto)))

---

Home Index