Nuprl Lemma : last-transition

{

es:EO.

e:E.

P:{a:E| loc(a) = loc(e)}

.
(

e'

e.P[e'] = P[e]

e'

e.(

P[e'] = P[e])

e''

(e',e].P[e''] = P[e]) }

{ Proof }

Definitions occuring in Statement : alle-between3:

e

(e1,e2].P[e], alle-le:

e

e'.P[e], existse-le:

e

e'.P[e], es-loc: loc(e), es-E: E, event_ordering: EO, Id: Id, bool:

, so_apply: x[s], all:

x:A. B[x], not:

A, or: P

Q, and: P

Q, set: {x:A| B[x]} , function: x:A

B[x], equal: s = t
Definitions : all:

x:A. B[x], or: P

Q, so_apply: x[s], and: P

Q, prop:

, cand: A c

B, member: t

T, so_lambda:

x.t[x], guard: {T}, alle-le:

e

e'.P[e], implies: P

Q, exists:

x:A. B[x], existse-le:

e

e'.P[e], alle-between3:

e

(e1,e2].P[e], not:

A, decidable: Dec(P), false: False, es-locl: (e <loc e')
Lemmas : last-event, not_wf, bool_wf, es-loc_wf, Id_wf, decidable__not, decidable__equal_bool, existse-le_wf, alle-between3_wf, es-E_wf, assert_wf, es-first_wf, alle-le_wf, event_ordering_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{} \mBbbB{}. (\mforall{}e'\mleq{}e.P[e'] = P[e] \mvee{} \mexists{}e'\mleq{}e.(\mneg{}P[e'] = P[e]) \mwedge{} \mforall{}e''\mmember{}(e',e].P[e''] = P[e]) Date html generated: 2011_08_16-AM-10_53_16 Last ObjectModification: 2010_09_24-PM-08_58_21 Home Index