---

{ [M:Type  Type]. [r:pRunType(P.M[P])]. [t:].
    (prior-run-events(r;t)  runEvents(r) List) }

{ Proof }

---

Definitions occuring in Statement :  prior-run-events: prior-run-events(r;t),  runEvents: runEvents(r),  pRunType: pRunType(T.M[T]),  nat: ,  uall: [x:A]. B[x],  so_apply: x[s],  member: t  T,  function: x:A  B[x],  list: type List,  universe: Type
Definitions :  uall: [x:A]. B[x],  pRunType: pRunType(T.M[T]),  so_apply: x[s],  nat: ,  member: t  T,  prior-run-events: prior-run-events(r;t),  so_lambda: x.t[x],  top: Top,  all: x:A. B[x],  subtype: S  T,  pi1: fst(t),  runEvents: runEvents(r),  pi2: snd(t),  assert: b,  isl: isl(x),  is-run-event: is-run-event(r;t;x),  outl: outl(x),  implies: P  Q,  band: p  q,  spreadn: spread3,  btrue: tt,  bfalse: ff,  ifthenelse: if b then t else f fi ,  true: True,  false: False,  int_seg: {i..j},  lelt: i  j < k,  prop: ,  and: P  Q,  uimplies: b supposing a,  sq_type: SQType(T),  guard: {T}
Lemmas :  mapfilter_wf,  int_seg_wf,  nat_properties,  upto_wf,  isl_wf,  Id_wf,  pMsg_wf,  unit_wf,  pi1_wf_top,  le_wf,  top_wf,  ldag_wf,  pInTransit_wf,  runEvents_wf,  assert_wf,  nat_wf,  pRunType_wf,  pi2_wf,  outl_wf,  is-run-event_wf,  subtype_base_sq,  bool_wf,  bool_subtype_base,  true_wf,  false_wf,  eq_id_self,  btrue_wf

---

\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[r:pRunType(P.M[P])].  \mforall{}[t:\mBbbN{}].    (prior-run-events(r;t)  \mmember{}  runEvents(r)  List)


Date html generated: 2011_08_16-PM-07_02_44
Last ObjectModification: 2011_06_18-AM-11_16_28

Home Index