Nuprl Lemma : decidable__exists-es-p-le-pred

{

es:EO

[P:E

]

e:E. ((

e:E. Dec(P e))

Dec(

a:E. (es-p-le-pred(es;P) e a))) }

{ Proof }

Definitions occuring in Statement : es-p-le-pred: es-p-le-pred(es;P), es-E: E, event_ordering: EO, decidable: Dec(P), uall:

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

, all:

x:A. B[x], exists:

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

Q, apply: f a, function: x:A

B[x]
Definitions : all:

x:A. B[x], uall:

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

, implies: P

Q, es-p-le-pred: es-p-le-pred(es;P), and: P

Q, cand: A c

B, alle-at:

e@i.P[e], member: t

T, so_lambda:

x.t[x], so_apply: x[s], existse-le:

e

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

e

e'.P[e]
Lemmas : decidable__existse-le, alle-le_wf, es-locl_wf, not_wf, es-E_wf, Id_wf, es-loc_wf, decidable__and, decidable__alle-le, decidable__implies, decidable__es-locl, decidable__not, decidable_wf, event_ordering_wf

\mforall{}es:EO. \mforall{}[P:E {}\mrightarrow{} \mBbbP{}]. \mforall{}e:E. ((\mforall{}e:E. Dec(P e)) {}\mRightarrow{} Dec(\mexists{}a:E. (es-p-le-pred(es;P) e a))) Date html generated: 2011_08_16-AM-11_03_10 Last ObjectModification: 2011_06_18-AM-09_36_31 Home Index