---

Step * 1 1 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 : basic-formal-sum(K;S)
9. y : basic-formal-sum(K;S)
10. bfs-reduce(K;S;x;y)
⊢ (λa,b. bfs-equiv(K;T;a;b)) x y
BY
{ Reduce 0 }

1
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 : basic-formal-sum(K;S)
9. y : basic-formal-sum(K;S)
10. bfs-reduce(K;S;x;y)
⊢ bfs-equiv(K;T;x;y)

---

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.  x  :  basic-formal-sum(K;S)
9.  y  :  basic-formal-sum(K;S)
10.  bfs-reduce(K;S;x;y)
\mvdash{}  (\mlambda{}a,b.  bfs-equiv(K;T;a;b))  x  y


By

---

Latex:
Reduce  0

---

Home Index