Nuprl Lemma : es-effective-causle
∀es:EO. ∀e,e':E. (e c≤ e' ⇒ es-effective(es;e') ⇒ es-effective(es;e))
Proof
Definitions occuring in Statement :
es-effective: es-effective(es;e),
es-causle: e c≤ e',
es-E: E,
event_ordering: EO,
all: ∀x:A. B[x],
implies: P ⇒ Q
Lemmas :
decidable__equal_Id,
es-loc_wf,
es-effective_wf,
es-causle_wf,
es-E_wf,
event_ordering_wf,
not_wf,
Id_wf,
equal_wf,
es-causle_transitivity
\mforall{}es:EO. \mforall{}e,e':E. (e c\mleq{} e' {}\mRightarrow{} es-effective(es;e') {}\mRightarrow{} es-effective(es;e))
Date html generated:
2015_07_17-AM-09_04_23
Last ObjectModification:
2015_07_16-AM-09_51_38
Home
Index