Nuprl Definition : 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(λc.(snd(c));λc.fst(c) = run-event-loc(e);fst(S0))

Definitions occuring in Statement : run-event-local-pred: run-event-local-pred(r;e), run-event-loc: run-event-loc(e), run-event-state: run-event-state(r;e), eq_id: a = b, mapfilter: mapfilter(f;P;L), pi1: fst(t), pi2: snd(t), lambda: λx.A[x], decide: case b of inl(x) => s[x] | inr(y) => t[y]
FDL editor aliases : run-prior-state

Latex:
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: 2015_07_23-AM-11_11_39 Last ObjectModification: 2012_02_25-PM-03_42_03 Home Index