---

{ the_es:EO. e',e:E.
    ((e  before(e'))  (l:E List. (before(e') = (before(e) @ [e] @ l)))) }

{ Proof }

---

Definitions occuring in Statement :  es-before: before(e),  es-E: E,  event_ordering: EO,  append: as @ bs,  all: x:A. B[x],  exists: x:A. B[x],  implies: P  Q,  cons: [car / cdr],  nil: [],  list: type List,  equal: s = t,  l_member: (x  l)
Definitions :  and: P  Q,  iff: P  Q,  rev_implies: P  Q,  prop: ,  subtype: S  T,  top: Top,  false: False,  implies: P  Q,  not: A,  le: A  B,  ycomb: Y,  label: ...$L... t,  ge: i  j ,  all: x:A. B[x],  member: t  T,  length: ||as||
Lemmas :  add_functionality_wrt_eq,  length_append,  length_cons,  non_neg_length,  top_wf,  length_wf_nat,  length_nil,  length_wf1

---

\mforall{}the$_{es}$:EO.  \mforall{}e',e:E.    ((e  \mmember{}  before(e'))  {}\mRightarrow{}  (\mexists{}l:E  List.  (before(e')  =  (before\000C(e)  @  [e]  @  l))))


Date html generated: 2011_08_16-AM-10_43_43
Last ObjectModification: 2010_09_24-PM-09_04_26

Home Index