---

Step * of Lemma implies-bfs-equiv

∀[K:RngSig]. ∀[S:Type].  ∀as,bs:basic-formal-sum(K;S).  (bfs-reduce(K;S;as;bs) ⇒ bfs-equiv(K;S;as;bs))
BY
{ (Auto
   THEN (InstLemma `implies-least-equiv` [⌜basic-formal-sum(K;S)⌝;⌜λas,bs. bfs-reduce(K;S;as;bs)⌝]⋅ THENA Auto)
   THEN RepUR ``rel_implies infix_ap`` -1
   THEN Fold `bfs-equiv` (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[K:RngSig].  \mforall{}[S:Type].
    \mforall{}as,bs:basic-formal-sum(K;S).    (bfs-reduce(K;S;as;bs)  {}\mRightarrow{}  bfs-equiv(K;S;as;bs))


By

---

Latex:
(Auto
  THEN  (InstLemma  `implies-least-equiv`  [\mkleeneopen{}basic-formal-sum(K;S)\mkleeneclose{};\mkleeneopen{}\mlambda{}as,bs.  bfs-reduce(K;S;as;bs)\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  RepUR  ``rel\_implies  infix\_ap``  -1
  THEN  Fold  `bfs-equiv`  (-1)
  THEN  Auto)

---

Home Index