---

Step * of Lemma bfs-rm0-equiv

∀K:RngSig. ∀S:Type. ∀b:basic-formal-sum(K;S). ∀eq:EqDecider(|K|).  (↓bfs-equiv(K;S;bfs-rm0(K;eq;b);b))
BY
{ (Auto
   THEN (InstLemma `bfs-equiv-rel` [⌜K⌝;⌜S⌝]⋅ THENA Auto)
   THEN All (Unfold `basic-formal-sum`)
   THEN (BagInd (-3) THENA Auto)) }

1
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;[]);[])

2
1. K : RngSig
2. S : Type
3. eq : EqDecider(|K|)
4. EquivRel(bag(|K| × S);a,b.bfs-equiv(K;S;a;b))
5. u : |K| × S
6. v : (|K| × S) List
7. ↓bfs-equiv(K;S;bfs-rm0(K;eq;v);v)
⊢ ↓bfs-equiv(K;S;bfs-rm0(K;eq;[u / v]);[u / v])

---

Latex:

---

Latex:
\mforall{}K:RngSig.  \mforall{}S:Type.  \mforall{}b:basic-formal-sum(K;S).  \mforall{}eq:EqDecider(|K|).
    (\mdownarrow{}bfs-equiv(K;S;bfs-rm0(K;eq;b);b))


By

---

Latex:
(Auto
  THEN  (InstLemma  `bfs-equiv-rel`  [\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}S\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  All  (Unfold  `basic-formal-sum`)
  THEN  (BagInd  (-3)  THENA  Auto))

---

Home Index