Nuprl Lemma : es-blocl-iff
∀es:EO. ∀e1,e2:E. (↑es-blocl(es;e1;e2) ⇐⇒ (e1 <loc e2))
Proof
Definitions occuring in Statement :
es-blocl: es-blocl(es;e1;e2),
es-locl: (e <loc e'),
es-E: E,
event_ordering: EO,
assert: ↑b,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q
Lemmas :
assert_wf,
es-blocl_wf,
es-locl_wf,
es-E_wf,
event_ordering_wf,
assert_of_band,
es-locless_wf,
eq_id_wf,
es-loc_wf,
assert-eq-id,
es-locless-property,
bool_wf,
eqtt_to_assert,
Id_wf,
iff_transitivity,
iff_weakening_uiff
\mforall{}es:EO. \mforall{}e1,e2:E. (\muparrow{}es-blocl(es;e1;e2) \mLeftarrow{}{}\mRightarrow{} (e1 <loc e2))
Date html generated:
2015_07_17-AM-08_36_09
Last ObjectModification:
2015_01_27-PM-02_58_34
Home
Index