---

{ [Info:Type]
    es:EO+(Info). e1,e2,e:E.
      e loc e2   es-hist(es;e1;e)  es-hist(es;e1;e2) 
      supposing loc(e2) = loc(e1) }

{ Proof }

---

Definitions occuring in Statement :  es-hist: es-hist(es;e1;e2),  event-ordering+: EO+(Info),  es-le: e loc e' ,  es-loc: loc(e),  es-E: E,  Id: Id,  uimplies: b supposing a,  uall: [x:A]. B[x],  all: x:A. B[x],  implies: P  Q,  universe: Type,  equal: s = t,  iseg: l1  l2
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  uimplies: b supposing a,  implies: P  Q,  es-hist: es-hist(es;e1;e2),  member: t  T,  prop: ,  decidable: Dec(P),  or: P  Q,  trans: Trans(T;x,y.E[x; y]),  iff: P  Q,  and: P  Q,  rev_implies: P  Q,  not: A,  false: False,  subtype: S  T
Lemmas :  iseg_map,  es-info_wf,  es-interval_wf,  es-le_wf,  event-ordering+_inc,  Id_wf,  es-loc_wf,  es-E_wf,  event-ordering+_wf,  decidable__es-le,  es-interval-iseg,  es-le-trans,  iseg_wf,  es-interval-nil,  es-le-loc,  decidable__es-locl,  es-le-not-locl,  nil_iseg

---

\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}e1,e2,e:E.
        e  \mleq{}loc  e2    {}\mRightarrow{}  es-hist(es;e1;e)  \mleq{}  es-hist(es;e1;e2)  supposing  loc(e2)  =  loc(e1)


Date html generated: 2011_08_16-AM-11_26_55
Last ObjectModification: 2011_06_20-AM-00_27_06

Home Index