---

{ [es:EO]. [e,e':E].  [e, e'] = ([e, pred(e')] @ [e']) supposing (e <loc e') }

{ Proof }

---

Definitions occuring in Statement :  es-interval: [e, e'],  es-locl: (e <loc e'),  es-pred: pred(e),  es-E: E,  event_ordering: EO,  append: as @ bs,  uimplies: b supposing a,  uall: [x:A]. B[x],  cons: [car / cdr],  nil: [],  list: type List,  equal: s = t
Definitions :  member: t  T,  uimplies: b supposing a,  uall: [x:A]. B[x],  implies: P  Q,  false: False,  not: A
Lemmas :  es-locl-first,  es-first_wf,  assert_elim,  btrue_neq_bfalse

---

\mforall{}[es:EO].  \mforall{}[e,e':E].    [e,  e']  =  ([e,  pred(e')]  @  [e'])  supposing  (e  <loc  e')


Date html generated: 2011_08_16-AM-10_40_02
Last ObjectModification: 2011_06_18-AM-09_18_35

Home Index