---

{ [M:Type  Type]
    r:pRunType(P.M[P])
      rel_finite(runEvents(r);run-lt(r)) 
      supposing e:runEvents(r)
                  ((fst(fst(run-info(r;e)))) < run-event-step(e)) }

{ Proof }

---

Definitions occuring in Statement :  run-lt: run-lt(r),  run-event-step: run-event-step(e),  runEvents: runEvents(r),  run-info: run-info(r;e),  pRunType: pRunType(T.M[T]),  uimplies: b supposing a,  uall: [x:A]. B[x],  so_apply: x[s],  pi1: fst(t),  all: x:A. B[x],  less_than: a < b,  function: x:A  B[x],  universe: Type,  rel_finite: rel_finite(T;R)
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  so_apply: x[s],  uimplies: b supposing a,  rel_finite: rel_finite(T;R),  member: t  T,  so_lambda: x.t[x],  top: Top,  subtype: S  T,  exists: x:A. B[x],  implies: P  Q,  infix_ap: x f y,  prop: ,  nat: ,  iff: P  Q,  and: P  Q,  rev_implies: P  Q
Lemmas :  runEvents_wf,  pi1_wf_top,  top_wf,  run-info_wf,  Id_wf,  pMsg_wf,  run-event-step_wf,  nat_wf,  pRunType_wf,  prior-run-events_wf,  run-lt_wf,  l_member_wf,  member-prior-run-events,  run-lt-step-less

---

\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}r:pRunType(P.M[P])
        rel\_finite(runEvents(r);run-lt(r)) 
        supposing  \mforall{}e:runEvents(r).  ((fst(fst(run-info(r;e))))  <  run-event-step(e))


Date html generated: 2011_08_16-PM-07_05_59
Last ObjectModification: 2011_06_18-AM-11_18_51

Home Index