Nuprl Lemma : es-le-before-if-first
∀[es:EO]. ∀[e:E]. ≤loc(e) ~ [e] supposing ↑first(e)
Proof
Definitions occuring in Statement :
es-le-before: ≤loc(e),
es-first: first(e),
es-E: E,
event_ordering: EO,
cons: [a / b],
nil: [],
assert: ↑b,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
sqequal: s ~ t
Lemmas :
es-before-is-nil-if-first,
nil-append,
assert_wf,
es-first_wf2,
es-E_wf,
event_ordering_wf
\mforall{}[es:EO]. \mforall{}[e:E]. \mleq{}loc(e) \msim{} [e] supposing \muparrow{}first(e)
Date html generated:
2015_07_17-AM-08_44_32
Last ObjectModification:
2015_01_27-PM-02_28_47
Home
Index