---

Step * of Lemma es-knows_wf

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

---

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)].
    (K(P)@e  \mmember{}  \mBbbP{}')


By

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

---

Home Index