---

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:

---

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

---

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

---

Home Index