### Nuprl 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))`

Proof

Definitions occuring in Statement :  es-knows: `K(P)@e` possible-event: `PossibleEvent(poss)` event_ordering: `EO` equiv_rel: `EquivRel(T;x,y.E[x; y])` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` prop: `ℙ` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` apply: `f a` lambda: `λx.A[x]` function: `x:A ─→ B[x]`
Lemmas :  all_wf possible-event_wf not_wf equiv_rel_wf event_ordering_wf
\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))

Date html generated: 2015_07_17-AM-08_52_09
Last ObjectModification: 2015_01_27-PM-01_17_46

Home Index