Nuprl Lemma : es-locl-iff
∀the_es:EO. ∀e,e':E. ((e <loc e') ⇐⇒ (¬↑first(e')) ∧ ((e = pred(e') ∈ E) ∨ (e <loc pred(e'))))
Proof
Definitions occuring in Statement :
es-locl: (e <loc e'),
es-first: first(e),
es-pred: pred(e),
es-E: E,
event_ordering: EO,
assert: ↑b,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
not: ¬A,
or: P ∨ Q,
and: P ∧ Q,
equal: s = t ∈ T
Lemmas :
es-locl_wf,
not_wf,
assert_wf,
es-first_wf,
es-E_wf,
or_wf,
equal_wf,
es-pred_wf,
Id_wf,
es-loc_wf,
es-loc-pred,
iff_weakening_equal
\mforall{}the$_{es}$:EO. \mforall{}e,e':E. ((e <loc e') \mLeftarrow{}{}\mRightarrow{} (\mneg{}\muparrow{}first(e')) \mwedge{} ((e = pred(e')) \mvee{} (e \000C<loc pred(e'))))
Date html generated:
2015_07_17-AM-08_36_26
Last ObjectModification:
2015_02_04-AM-07_07_35
Home
Index