---

Step * 1 2 of Lemma formal-sum-subtype

.....antecedent..... 
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)
⊢ EquivRel(basic-formal-sum(K;S);x,y.(λa,b. bfs-equiv(K;T;a;b)) x y)
BY
{ (Reduce 0 THEN Unfold `bfs-equiv` 0 THEN (BLemma `least-equiv-is-equiv-1` ⋅ THENA Auto) THEN EAuto 1) }

---

Latex:

---

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


By

---

Latex:
(Reduce  0
  THEN  Unfold  `bfs-equiv`  0
  THEN  (BLemma  `least-equiv-is-equiv-1`  \mcdot{}  THENA  Auto)
  THEN  EAuto  1)

---

Home Index