Nuprl Lemma : last-transition
∀es:EO. ∀e:E. ∀P:{a:E| loc(a) = loc(e) ∈ Id} ─→ 𝔹.
(∀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 ∈ T
Lemmas :
last-event,
Id_wf,
es-loc_wf,
not_wf,
equal_wf,
bool_wf,
decidable__not,
decidable__equal_bool,
set_wf,
existse-le_wf,
alle-between3_wf,
assert_wf,
es-first_wf2,
alle-le_wf,
es-E_wf,
event_ordering_wf,
es-le-loc,
es-le_wf,
all_wf,
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:
2015_07_17-AM-08_51_05
Last ObjectModification:
2015_01_27-PM-01_20_20
Home
Index