---

Step * 1 of Lemma bfs-rm0-equiv


1. K : RngSig
2. S : Type
3. eq : EqDecider(|K|)
4. EquivRel(bag(|K| × S);a,b.bfs-equiv(K;S;a;b))
⊢ ↓bfs-equiv(K;S;bfs-rm0(K;eq;[]);[])
BY
{ (((Subst' bfs-rm0(K;eq;[]) ~ [] 0 THENA Computation) THEN (Subst' [] ~ {} 0 THENA Computation)) THEN Auto) }

---

Latex:

---

Latex:

1.  K  :  RngSig
2.  S  :  Type
3.  eq  :  EqDecider(|K|)
4.  EquivRel(bag(|K|  \mtimes{}  S);a,b.bfs-equiv(K;S;a;b))
\mvdash{}  \mdownarrow{}bfs-equiv(K;S;bfs-rm0(K;eq;[]);[])


By

---

Latex:
(((Subst'  bfs-rm0(K;eq;[])  \msim{}  []  0  THENA  Computation)  THEN  (Subst'  []  \msim{}  \{\}  0  THENA  Computation))
  THEN  Auto
  )

---

Home Index