run-prior-state(S0;r;e) ==
case run-event-local-pred(r;e)
of inl(e') => run-event-state(r;e')
| inr(x) => mapfilter(
c.(snd(c));c.fst(c) = run-event-loc(e);fst(S0))
Definitions :
decide: case b of inl(x) => s[x] | inr(y) => t[y],
run-event-local-pred: run-event-local-pred(r;e),
run-event-state: run-event-state(r;e),
mapfilter: mapfilter(f;P;L),
pi2: snd(t),
lambda: x.A[x],
eq_id: a = b,
run-event-loc: run-event-loc(e),
pi1: fst(t)
FDL editor aliases :
run-prior-state
run-prior-state(S0;r;e) ==
case run-event-local-pred(r;e)
of inl(e') => run-event-state(r;e')
| inr(x) => mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c) = run-event-loc(e);fst(S0))
Date html generated:
2010_08_27-PM-06_18_21
Last ObjectModification:
2010_05_24-PM-04_51_57
Home
Index