---

Step * of Lemma es-knows-valid

∀[poss:EO ⟶ ℙ']. ∀[R:PossibleEvent(poss) ⟶ PossibleEvent(poss) ⟶ ℙ']. ∀[P:PossibleEvent(poss) ⟶ ℙ'].
  ((∀e:PossibleEvent(poss). (P e)) ⇒ (∀e:PossibleEvent(poss). K(P)@e))
BY
{ (Unfold `es-knows` 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Unfold  `es-knows`  0  THEN  Auto)

---

Home Index