Nuprl Lemma : iseg-es-le-before
∀es:EO. ∀e',e:E. (e' ≤loc e ⇒ ≤loc(e') ≤ ≤loc(e))
Proof
Definitions occuring in Statement :
es-le-before: ≤loc(e),
es-le: e ≤loc e' ,
es-E: E,
event_ordering: EO,
iseg: l1 ≤ l2,
all: ∀x:A. B[x],
implies: P ⇒ Q
Lemmas :
iseg_weakening,
es-le-before_wf2,
subtype_rel_list,
es-le_wf,
iseg_wf,
es-E_wf,
event_ordering_wf,
es-before-decomp,
member-es-before,
append_wf,
cons_wf,
nil_wf,
equal_wf,
list_wf,
es-before_wf,
length_wf_nat,
nat_wf,
append_assoc
\mforall{}es:EO. \mforall{}e',e:E. (e' \mleq{}loc e {}\mRightarrow{} \mleq{}loc(e') \mleq{} \mleq{}loc(e))
Date html generated:
2015_07_17-AM-08_44_18
Last ObjectModification:
2015_01_27-PM-02_29_13
Home
Index