---

Step * of Lemma es-knows-not

∀[poss:EO ─→ ℙ']. ∀[R:PossibleEvent(poss) ─→ PossibleEvent(poss) ─→ ℙ'].
  (EquivRel(PossibleEvent(poss))(R _1 _2)
  ⇒ (∀[P:PossibleEvent(poss) ─→ ℙ']. ∀e:PossibleEvent(poss). K(λe.(¬K(P)@e))@e supposing ¬K(P)@e))
BY
{ (RepUR ``es-knows`` 0 THEN Auto THEN ParallelOp -3 THEN Auto THEN BackThruSomeHyp THEN D 3 THEN Auto) }

---

Latex:


\mforall{}[poss:EO  {}\mrightarrow{}  \mBbbP{}'].  \mforall{}[R:PossibleEvent(poss)  {}\mrightarrow{}  PossibleEvent(poss)  {}\mrightarrow{}  \mBbbP{}'].
    (EquivRel(PossibleEvent(poss))(R  $_{1}$  $_{2}$)
    {}\mRightarrow{}  (\mforall{}[P:PossibleEvent(poss)  {}\mrightarrow{}  \mBbbP{}'].  \mforall{}e:PossibleEvent(poss).  K(\mlambda{}e.(\mneg{}K(P)@e))@e  supposing  \mneg{}K(P)@e))


By

(RepUR  ``es-knows``  0
  THEN  Auto
  THEN  ParallelOp  -3
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  D  3
  THEN  Auto)

---

Home Index