---

Step * of Lemma bfs-equiv-implies2

∀[S:Type]. ∀[K:RngSig].
  ∀x,y:basic-formal-sum(K;S).
    (bfs-equiv(K;S;x;y)
    ⇒ {∀[P:basic-formal-sum(K;S) ⟶ ℙ]
          ((∀x,y:basic-formal-sum(K;S).  (bfs-reduce(K;S;x;y) ⇒ (P[x] ⇐⇒ P[y]))) ⇒ P[x] ⇒ P[y])})
BY
{ (Auto
   THEN (InstLemma `least-equiv-induction2` [⌜basic-formal-sum(K;S)⌝;⌜λas,bs. bfs-reduce(K;S;as;bs)⌝]⋅ THENA Auto)
   THEN Unfold `infix_ap` -1
   THEN Fold `bfs-equiv` (-1)
   THEN Reduce -1
   THEN FHyp (-1) [-2]
   THEN Auto) }

---

Latex:

---

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


By

---

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

---

Home Index