Nuprl Lemma : es-first-at-exists2

{

es:EO.

i:Id.

[P:{e:E| loc(e) = i}

]
((

e:{e:E| loc(e) = i} . Dec(P[e]))

(

e:E
(

e'

e.e' is first@ i s.t. e'.P[e']) supposing
((

e'

e.

P[e']) and
(loc(e) = i)))) }

{ Proof }

Definitions occuring in Statement : es-first-at: e is first@ i s.t. e.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, decidable: Dec(P), uimplies: b supposing a, uall:

[x:A]. B[x], prop:

, so_apply: x[s], all:

x:A. B[x], not:

A, implies: P

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

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

x:A. B[x], uall:

[x:A]. B[x], prop:

, implies: P

Q, so_apply: x[s], uimplies: b supposing a, not:

A, member: t

T, false: False, so_lambda:

x.t[x], alle-at:

e@i.P[e], and: P

Q, exists:

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

e

e'.P[e], cand: A c

B, alle-le:

e

e'.P[e], decidable: Dec(P), or: P

Q
Lemmas : alle-le_wf, not_wf, Id_wf, es-loc_wf, es-E_wf, decidable__existse-le, decidable_wf, event_ordering_wf, es-le-loc, es-first-at-exists, es-le_transitivity, es-le_wf, es-first-at_wf

\mforall{}es:EO. \mforall{}i:Id. \mforall{}[P:\{e:E| loc(e) = i\} {}\mrightarrow{} \mBbbP{}] ((\mforall{}e:\{e:E| loc(e) = i\} . Dec(P[e])) {}\mRightarrow{} (\mforall{}e:E. (\mexists{}e'\mleq{}e.e' is first@ i s.t. e'.P[e']) supposing ((\mneg{}\mforall{}e'\mleq{}e.\mneg{}P[e']) and (loc(e) = i)))) Date html generated: 2011_08_16-AM-10_50_31 Last ObjectModification: 2011_06_18-AM-09_25_40 Home Index