---

Step * of Lemma es-knows-knows

∀[poss:EO ⟶ ℙ']. ∀[R:PossibleEvent(poss) ⟶ PossibleEvent(poss) ⟶ ℙ'].
  (Trans(PossibleEvent(poss);a,b.R a b)
  ⇒ (∀[P:PossibleEvent(poss) ⟶ ℙ']. ∀e:PossibleEvent(poss). (K(P)@e ⇒ K(λe.K(P)@e)@e)))
BY
{ (RepUR ``es-knows`` 0 THEN Auto THEN BackThruSomeHyp THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[poss:EO  {}\mrightarrow{}  \mBbbP{}'].  \mforall{}[R:PossibleEvent(poss)  {}\mrightarrow{}  PossibleEvent(poss)  {}\mrightarrow{}  \mBbbP{}'].
    (Trans(PossibleEvent(poss);a,b.R  a  b)
    {}\mRightarrow{}  (\mforall{}[P:PossibleEvent(poss)  {}\mrightarrow{}  \mBbbP{}'].  \mforall{}e:PossibleEvent(poss).  (K(P)@e  {}\mRightarrow{}  K(\mlambda{}e.K(P)@e)@e)))


By

---

Latex:
(RepUR  ``es-knows``  0  THEN  Auto  THEN  BackThruSomeHyp  THEN  Auto)

---

Home Index