---

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

{ Proof }

---

Definitions occuring in Statement :  es-hist: es-hist(es;e1;e2),  event-ordering+: EO+(Info),  es-locl: (e <loc e'),  es-loc: loc(e),  es-E: E,  Id: Id,  null: null(as),  assert: b,  uimplies: b supposing a,  uall: [x:A]. B[x],  all: x:A. B[x],  iff: P  Q,  universe: Type,  equal: s = t
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  uimplies: b supposing a,  member: t  T,  prop: ,  iff: P  Q,  assert: b,  null: null(as),  es-hist: es-hist(es;e1;e2),  map: map(f;as),  ycomb: Y,  btrue: tt,  ifthenelse: if b then t else f fi ,  true: True,  and: P  Q,  implies: P  Q,  rev_implies: P  Q,  top: Top,  subtype: S  T,  decidable: Dec(P),  or: P  Q,  not: A,  false: False
Lemmas :  decidable__es-locl,  Id_wf,  es-loc_wf,  event-ordering+_inc,  es-E_wf,  event-ordering+_wf,  es-interval-is-nil,  true_wf,  es-locl_wf,  null-map,  es-interval_wf2,  top_wf,  assert_witness,  null_wf3,  assert_wf,  iff_weakening_uiff,  es-interval_wf,  assert_of_null,  es-interval-nil

---

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


Date html generated: 2011_08_16-AM-11_26_48
Last ObjectModification: 2011_06_20-AM-00_27_00

Home Index