---

Step * of Lemma bfs-equiv-rel

∀K:RngSig. ∀S:Type.  EquivRel(basic-formal-sum(K;S);a,b.bfs-equiv(K;S;a;b))
BY
{ (Unfold `bfs-equiv` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}K:RngSig.  \mforall{}S:Type.    EquivRel(basic-formal-sum(K;S);a,b.bfs-equiv(K;S;a;b))


By

---

Latex:
(Unfold  `bfs-equiv`  0  THEN  Auto)

---

Home Index