---

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:


\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

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

---

Home Index