Nuprl Lemma : eo-forward-no-prior-classrel

[Info,T:Type]. ∀[X:EClass(T)]. ∀[es:EO+(Info)]. ∀[start:E]. ∀[e:E].
  uiff((no prior to e);(no between start and e)) supposing loc(e) loc(start) ∈ Id


Definitions occuring in Statement :  no-classrel-in-interval: (no between start and e) no-prior-classrel: (no prior to e) eclass: EClass(A[eo; e]) eo-forward: eo.e event-ordering+: EO+(Info) es-loc: loc(e) es-E: E Id: Id uiff: uiff(P;Q) uimplies: supposing a uall: [x:A]. B[x] universe: Type equal: t ∈ T
Lemmas :  member-eo-forward-E equal_wf es-loc_wf eo-forward-locl classrel_wf es-le_wf es-locl_wf eo-forward_wf Id_wf event-ordering+_subtype eo-forward-E-subtype es-E_wf no-prior-classrel_wf eo-forward-E-member no-classrel-in-interval_wf event-ordering+_wf eclass_wf
\mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[es:EO+(Info)].  \mforall{}[start:E].  \mforall{}[e:E].
    uiff((no  X  prior  to  e);(no  X  between  start  and  e))  supposing  loc(e)  =  loc(start)

Date html generated: 2015_07_17-PM-00_29_54
Last ObjectModification: 2015_01_27-PM-11_33_35

Home Index