---

Step * 1 3 of Lemma formal-sum-subtype


1. K : RngSig
2. S : Type
3. T : Type
4. S ⊆r T
5. a : basic-formal-sum(K;S)
6. b : basic-formal-sum(K;S)
7. bfs-equiv(K;S;a;b)
8. ∀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;a;b)
BY
{ (Reduce -1 THEN BHyp -1 THEN Auto) }

---

Latex:

---

Latex:

1.  K  :  RngSig
2.  S  :  Type
3.  T  :  Type
4.  S  \msubseteq{}r  T
5.  a  :  basic-formal-sum(K;S)
6.  b  :  basic-formal-sum(K;S)
7.  bfs-equiv(K;S;a;b)
8.  \mforall{}x,y:basic-formal-sum(K;S).    (bfs-equiv(K;S;x;y)  {}\mRightarrow{}  ((\mlambda{}a,b.  bfs-equiv(K;T;a;b))  x  y))
\mvdash{}  bfs-equiv(K;T;a;b)


By

---

Latex:
(Reduce  -1  THEN  BHyp  -1  THEN  Auto)

---

Home Index