Nuprl Lemma : decidable__es-p-le-pred
∀es:EO. ∀[P:E ─→ ℙ]. ((∀e:E. Dec(P e)) ⇒ (∀e,e':E. Dec(es-p-le-pred(es;P) e e')))
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],
implies: P ⇒ Q,
apply: f a,
function: x:A ─→ B[x]
Lemmas :
es-E_wf,
all_wf,
decidable_wf,
event_ordering_wf,
es-le_wf,
alle-le_wf,
Id_wf,
es-loc_wf,
es-locl_wf,
not_wf,
decidable__implies,
decidable__es-locl,
decidable__not,
equal_wf,
decidable__cand,
decidable__es-le,
decidable__alle-le
\mforall{}es:EO. \mforall{}[P:E {}\mrightarrow{} \mBbbP{}]. ((\mforall{}e:E. Dec(P e)) {}\mRightarrow{} (\mforall{}e,e':E. Dec(es-p-le-pred(es;P) e e')))
Date html generated:
2015_07_17-AM-08_58_47
Last ObjectModification:
2015_01_27-PM-01_03_41
Home
Index