---

{ the_es:EO. WellFnd{i}(E;x,y.(x < y)) }

{ Proof }

---

Definitions occuring in Statement :  es-causl: (e < e'),  es-E: E,  event_ordering: EO,  wellfounded: WellFnd{i}(A;x,y.R[x; y]),  all: x:A. B[x]
Definitions :  all: x:A. B[x],  member: t  T,  so_lambda: x y.t[x; y],  and: P  Q,  implies: P  Q,  so_apply: x[s1;s2],  prop:
Lemmas :  pes-axioms,  strongwf-implies,  es-E_wf,  es-causl_wf,  event_ordering_wf

---

\mforall{}the$_{es}$:EO.  WellFnd\{i\}(E;x,y.(x  <  y))


Date html generated: 2011_08_16-AM-10_31_03
Last ObjectModification: 2010_09_24-PM-09_11_38

Home Index