---

Step * of Lemma bfs-equiv-implies

∀[S:Type]. ∀[K:RngSig]. ∀[E:basic-formal-sum(K;S) ⟶ basic-formal-sum(K;S) ⟶ ℙ].
  ((∀x,y:basic-formal-sum(K;S).  (bfs-reduce(K;S;x;y) ⇒ (E x y)))
  ⇒ EquivRel(basic-formal-sum(K;S);x,y.E x y)
  ⇒ (∀x,y:basic-formal-sum(K;S).  (bfs-equiv(K;S;x;y) ⇒ (E x y))))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN (InstLemma `least-equiv-implies` [⌜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 Trivial) }

---

Latex:

---

Latex:
\mforall{}[S:Type].  \mforall{}[K:RngSig].  \mforall{}[E:basic-formal-sum(K;S)  {}\mrightarrow{}  basic-formal-sum(K;S)  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x,y:basic-formal-sum(K;S).    (bfs-reduce(K;S;x;y)  {}\mRightarrow{}  (E  x  y)))
    {}\mRightarrow{}  EquivRel(basic-formal-sum(K;S);x,y.E  x  y)
    {}\mRightarrow{}  (\mforall{}x,y:basic-formal-sum(K;S).    (bfs-equiv(K;S;x;y)  {}\mRightarrow{}  (E  x  y))))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (InstLemma  `least-equiv-implies`  [\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  Trivial)

---

Home Index