---

{ [M:Type  Type]
    r:pRunType(P.M[P]). e1,e2:runEvents(r).
      (e1 = e2)  (e1 run-lt(r) e2)  (e2 run-lt(r) e1) 
      supposing run-event-loc(e1) = run-event-loc(e2) }

{ Proof }

---

Definitions occuring in Statement :  run-lt: run-lt(r),  run-event-loc: run-event-loc(e),  runEvents: runEvents(r),  pRunType: pRunType(T.M[T]),  Id: Id,  uimplies: b supposing a,  uall: [x:A]. B[x],  infix_ap: x f y,  so_apply: x[s],  all: x:A. B[x],  or: P  Q,  function: x:A  B[x],  universe: Type,  equal: s = t
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  so_apply: x[s],  uimplies: b supposing a,  run-lt: run-lt(r),  member: t  T,  so_lambda: x.t[x],  prop: ,  or: P  Q,  infix_ap: x f y,  runEvents: runEvents(r),  assert: b,  btrue: tt,  ifthenelse: if b then t else f fi ,  true: True,  top: Top,  subtype: S  T,  nat: ,  rel_plus: R,  run-pred: run-pred(r),  exists: x:A. B[x],  nat_plus: ,  and: P  Q,  decidable: Dec(P),  sq_type: SQType(T),  implies: P  Q,  guard: {T},  run-event-loc: run-event-loc(e),  le: A  B,  run-event-step: run-event-step(e),  pi1: fst(t),  pi2: snd(t),  not: A,  false: False,  rev_implies: P  Q,  iff: P  Q
Lemmas :  decidable__le,  run-event-step_wf,  nat_wf,  Id_wf,  run-event-loc_wf,  runEvents_wf,  pRunType_wf,  rel_plus_wf,  run-pred_wf,  subtype_base_sq,  bool_wf,  bool_subtype_base,  assert_wf,  is-run-event_wf,  pi1_wf_top,  pi2_wf,  assert_elim,  le_wf,  rel_exp_one,  run-info_wf,  pMsg_wf,  rel_exp_wf,  nat_plus_inc

---

\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}r:pRunType(P.M[P]).  \mforall{}e1,e2:runEvents(r).
        (e1  =  e2)  \mvee{}  (e1  run-lt(r)  e2)  \mvee{}  (e2  run-lt(r)  e1) 
        supposing  run-event-loc(e1)  =  run-event-loc(e2)


Date html generated: 2011_08_17-PM-03_38_12
Last ObjectModification: 2011_06_18-AM-11_19_35

Home Index