### Nuprl Lemma : last-event

`∀es:EO. ∀e:E.`
`  ∀[P:{a:E| loc(a) = loc(e) ∈ Id}  ─→ ℙ]`
`    ((∀a:{a:E| loc(a) = loc(e) ∈ Id} . Dec(P[a]))`
`    `` (∀e'≤e.¬P[e'] ∨ (∃e':E. (e' ≤loc e  c∧ (P[e'] ∧ (∀e'':E. ((e' <loc e'') `` e'' ≤loc e  `` (¬P[e'']))))))))`

Proof

Definitions occuring in Statement :  alle-le: `∀e≤e'.P[e]` es-le: `e ≤loc e' ` es-locl: `(e <loc e')` es-loc: `loc(e)` es-E: `E` event_ordering: `EO` Id: `Id` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` cand: `A c∧ B` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` implies: `P `` Q` or: `P ∨ Q` and: `P ∧ Q` set: `{x:A| B[x]} ` function: `x:A ─→ B[x]` equal: `s = t ∈ T`
Lemmas :  previous-event-exists decidable__existse-le Id_wf es-loc_wf equal_wf all_wf es-E_wf decidable_wf event_ordering_wf alle-le_wf not_wf exists_wf es-le_wf es-le-loc es-locl_wf
\mforall{}es:EO.  \mforall{}e:E.
\mforall{}[P:\{a:E|  loc(a)  =  loc(e)\}    {}\mrightarrow{}  \mBbbP{}]
((\mforall{}a:\{a:E|  loc(a)  =  loc(e)\}  .  Dec(P[a]))
{}\mRightarrow{}  (\mforall{}e'\mleq{}e.\mneg{}P[e']
\mvee{}  (\mexists{}e':E.  (e'  \mleq{}loc  e    c\mwedge{}  (P[e']  \mwedge{}  (\mforall{}e'':E.  ((e'  <loc  e'')  {}\mRightarrow{}  e''  \mleq{}loc  e    {}\mRightarrow{}  (\mneg{}P[e'']))))))))

Date html generated: 2015_07_17-AM-08_50_45
Last ObjectModification: 2015_01_27-PM-01_20_03

Home Index