---

Step * of Lemma es-knows-true

∀[poss:EO ─→ ℙ']. ∀[R:PossibleEvent(poss) ─→ PossibleEvent(poss) ─→ ℙ'].
  ((∀e:PossibleEvent(poss). (R e e)) ⇒ (∀[P:PossibleEvent(poss) ─→ ℙ']. ∀e:PossibleEvent(poss). (K(P)@e ⇒ (P e))))
BY
{ (Unfold `es-knows` 0 THEN Auto THEN (Using [`e\'',⌈e⌉] (BackThruSomeHyp THEN Auto))⋅) }

---

Latex:


\mforall{}[poss:EO  {}\mrightarrow{}  \mBbbP{}'].  \mforall{}[R:PossibleEvent(poss)  {}\mrightarrow{}  PossibleEvent(poss)  {}\mrightarrow{}  \mBbbP{}'].
    ((\mforall{}e:PossibleEvent(poss).  (R  e  e))
    {}\mRightarrow{}  (\mforall{}[P:PossibleEvent(poss)  {}\mrightarrow{}  \mBbbP{}'].  \mforall{}e:PossibleEvent(poss).  (K(P)@e  {}\mRightarrow{}  (P  e))))


By

(Unfold  `es-knows`  0  THEN  Auto  THEN  (Using  [`e\mbackslash{}'',\mkleeneopen{}e\mkleeneclose{}]  (BackThruSomeHyp  THEN  Auto))\mcdot{})

---

Home Index