---

run-pred(r) ==
  e1,e2.
   (((run-event-loc(e1) = run-event-loc(e2))
    (run-event-step(e1) < run-event-step(e2)))
    (e1 = (fst(run-info(r;e2)))))

---

Definitions :  lambda: x.A[x],  or: P  Q,  and: P  Q,  run-event-loc: run-event-loc(e),  less_than: a < b,  run-event-step: run-event-step(e),  equal: s = t,  product: x:A  B[x],  int: ,  Id: Id,  pi1: fst(t),  run-info: run-info(r;e)
FDL editor aliases :  run-pred

---

run-pred(r)  ==
    \mlambda{}e1,e2.
      (((run-event-loc(e1)  =  run-event-loc(e2))  \mwedge{}  (run-event-step(e1)  <  run-event-step(e2)))
      \mvee{}  (e1  =  (fst(run-info(r;e2)))))


Date html generated: 2010_08_27-PM-06_34_35
Last ObjectModification: 2010_04_30-AM-12_14_15

Home Index