Nuprl Lemma : eo-forward-interval

[Info:Type]. ∀[es:EO+(Info)]. ∀[e1,e2,e:E].  ([e1, e2] [e1, e2] ∈ (E List)) supposing (e1 ≤loc e2  and e ≤loc e1 )


Definitions occuring in Statement :  eo-forward: eo.e event-ordering+: EO+(Info) es-interval: [e, e'] es-le: e ≤loc e'  es-E: E list: List uimplies: supposing a uall: [x:A]. B[x] universe: Type equal: t ∈ T
Lemmas :  filter_cons_lemma filter_nil_lemma es-le_wf event-ordering+_subtype es-E_wf event-ordering+_wf filter_append_sq append_wf squash_wf true_wf list_wf es-ble_wf bool_wf eqtt_to_assert assert-es-ble cons_wf nil_wf ite_rw_true member-eo-forward-E es-le_transitivity eo-forward-le2 iff_weakening_equal eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot eo-forward_wf Id_wf es-loc_wf eo-forward-before subtype_rel_list eo-forward-E-subtype es-before_wf event_ordering_wf eo-forward-forward
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[e1,e2,e:E].
    ([e1,  e2]  =  [e1,  e2])  supposing  (e1  \mleq{}loc  e2    and  e  \mleq{}loc  e1  )

Date html generated: 2015_07_17-PM-00_05_59
Last ObjectModification: 2015_02_04-PM-05_38_57

Home Index