Nuprl Lemma : last-decidable
∀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'] ⇐⇒ 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,
decidable: Dec(P),
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
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 :
all_wf,
Id_wf,
es-loc_wf,
decidable_wf,
es-E_wf,
event_ordering_wf,
btrue_wf,
bfalse_wf,
equal_wf,
set_wf,
iff_wf,
bool_wf,
equal-wf-base,
btrue_neq_bfalse,
ppcc-problem,
unit_wf2,
iff_imp_equal_bool,
true_wf,
false_wf,
iff_weakening_equal,
last-transition,
exists_wf,
es-le_wf,
not_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.P[e'] \mLeftarrow{}{}\mRightarrow{} P[e] \mvee{} \mexists{}e'\mleq{}e.(\mneg{}(P[e'] \mLeftarrow{}{}\mRightarrow{} P[e])) \mwedge{} \mforall{}e''\mmember{}(e',e].P[e''] \mLeftarrow{}{}\mRightarrow{} P[e]))
Date html generated:
2015_07_17-AM-08_51_12
Last ObjectModification:
2015_02_04-PM-05_56_25
Home
Index