Nuprl Lemma : eo-forward-ble

eo:EO. ∀e:E. ∀a,b:E.  (a ≤loc a ≤loc b)


Proof




Definitions occuring in Statement :  eo-forward: eo.e es-ble: e ≤loc e' es-E: E event_ordering: EO all: x:A. B[x] sqequal: t
Lemmas :  eo-forward-wf subtype_base_sq bool_wf bool_subtype_base iff_imp_equal_bool es-ble_wf eo-forward-E-subtype eo-forward-le es-le_wf assert-es-ble assert_wf iff_wf es-E_wf event_ordering_wf
\mforall{}eo:EO.  \mforall{}e:E.  \mforall{}a,b:E.    (a  \mleq{}loc  b  \msim{}  a  \mleq{}loc  b)



Date html generated: 2015_07_17-PM-00_03_39
Last ObjectModification: 2015_01_28-AM-00_32_27

Home Index