---

{ [Info:Type]. [es:EO+(Info)]. [Q:E  E  ]. [X:EClass(Top)].
  [p:retrace(es;Q;X)].
    (retracer(p)  E  (E(X) List)) }

{ Proof }

---

Definitions occuring in Statement :  retracer: retracer(p),  retrace: retrace(es;Q;X),  es-E-interface: E(X),  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-E: E,  uall: [x:A]. B[x],  top: Top,  prop: ,  member: t  T,  function: x:A  B[x],  list: type List,  universe: Type
Definitions :  uall: [x:A]. B[x],  prop: ,  top: Top,  member: t  T,  es-E-interface: E(X),  retracer: retracer(p),  pi2: snd(t),  and: P  Q,  all: x:A. B[x],  implies: P  Q,  exists: x:A. B[x],  iff: P  Q,  l_all: (xL.P[x]),  so_lambda: x.t[x],  rev_implies: P  Q,  so_lambda: x y.t[x; y],  retrace: retrace(es;Q;X),  uimplies: b supposing a,  so_apply: x[s],  so_apply: x[s1;s2],  subtype: S  T
Lemmas :  pi1_wf_top,  es-E-interface_wf,  es-E_wf,  iff_wf,  l_member_wf,  l_before_wf,  list-set-type2,  assert_wf,  in-eclass_wf,  retrace_wf,  eclass_wf,  top_wf,  event-ordering+_inc,  event-ordering+_wf

---

\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[Q:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[X:EClass(Top)].  \mforall{}[p:retrace(es;Q;X)].
    (retracer(p)  \mmember{}  E  {}\mrightarrow{}  (E(X)  List))


Date html generated: 2011_08_16-PM-06_03_06
Last ObjectModification: 2011_06_20-AM-01_46_23

Home Index