### Nuprl Lemma : es-knows-stable

`∀[poss:EO ─→ ℙ']. ∀[R:PossibleEvent(poss) ─→ PossibleEvent(poss) ─→ ℙ'].`
`  (Trans(PossibleEvent(poss))(R _1 _2)`
`  `` (∀e1,e2:PossibleEvent(poss).  (e1 ≤ e2 `` (R e1 e2)))`
`  `` (∀[P:PossibleEvent(poss) ─→ ℙ']. ∀e1,e2:PossibleEvent(poss).  (e1 ≤ e2 `` K(P)@e1 `` K(P)@e2)))`

Proof

Definitions occuring in Statement :  poss-le: `e1 ≤ e2` es-knows: `K(P)@e` possible-event: `PossibleEvent(poss)` event_ordering: `EO` trans: `Trans(T;x,y.E[x; y])` uall: `∀[x:A]. B[x]` prop: `ℙ` all: `∀x:A. B[x]` implies: `P `` Q` apply: `f a` function: `x:A ─→ B[x]`
Lemmas :  possible-event_wf all_wf poss-le_wf trans_wf event_ordering_wf
\mforall{}[poss:EO  {}\mrightarrow{}  \mBbbP{}'].  \mforall{}[R:PossibleEvent(poss)  {}\mrightarrow{}  PossibleEvent(poss)  {}\mrightarrow{}  \mBbbP{}'].
(Trans(PossibleEvent(poss))(R  \$_{1}\$  \$_{2}\$)
{}\mRightarrow{}  (\mforall{}e1,e2:PossibleEvent(poss).    (e1  \mleq{}  e2  {}\mRightarrow{}  (R  e1  e2)))
{}\mRightarrow{}  (\mforall{}[P:PossibleEvent(poss)  {}\mrightarrow{}  \mBbbP{}'].  \mforall{}e1,e2:PossibleEvent(poss).    (e1  \mleq{}  e2  {}\mRightarrow{}  K(P)@e1  {}\mRightarrow{}  K(P)@e2)))

Date html generated: 2015_07_17-AM-08_52_27
Last ObjectModification: 2015_01_27-PM-01_16_10

Home Index