---

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

{ Proof }

---

Definitions occuring in Statement :  run-pred: run-pred(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],  infix_ap: x f y,  so_apply: x[s],  pi1: fst(t),  all: x:A. B[x],  less_than: a < b,  function: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  so_apply: x[s],  uimplies: b supposing a,  all: x:A. B[x],  infix_ap: x f y,  member: t  T,  so_lambda: x.t[x],  top: Top,  subtype: S  T,  run-event-step: run-event-step(e),  Id: Id,  run-pred: run-pred(r),  or: P  Q,  and: P  Q,  nat: ,  sq_type: SQType(T),  implies: P  Q,  guard: {T},  prop:
Lemmas :  run-pred_wf,  runEvents_wf,  pi1_wf_top,  top_wf,  run-info_wf,  Id_wf,  pMsg_wf,  run-event-step_wf,  nat_wf,  pRunType_wf,  subtype_base_sq,  product_subtype_base,  int_subtype_base,  atom2_subtype_base

---

\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[r:pRunType(P.M[P])].
    \mforall{}[x,y:runEvents(r)].    run-event-step(x)  <  run-event-step(y)  supposing  x  run-pred(r)  y 
    supposing  \mforall{}e:runEvents(r).  ((fst(fst(run-info(r;e))))  <  run-event-step(e))


Date html generated: 2011_08_16-PM-07_03_07
Last ObjectModification: 2011_06_18-AM-11_16_51

Home Index