EO(r) ==
mk-eo(runEvents(r);
e.tt;e.run-event-loc(e);run-lt(r);
deq-runEvents-witness();well-founded-run-lt-witness();decd-run-lt(r);
run-lt-transitive-witness();finite-run-lt-witness(r);
total-run-lt-witness())["info" := e.run-event-msg(r;e)]
Definitions occuring in Statement :
run-lt-transitive-witness: run-lt-transitive-witness(),
total-run-lt-witness: total-run-lt-witness(),
well-founded-run-lt-witness: well-founded-run-lt-witness(),
finite-run-lt-witness: finite-run-lt-witness(r),
decd-run-lt: decd-run-lt(r),
run-lt: run-lt(r),
run-event-loc: run-event-loc(e),
deq-runEvents-witness: deq-runEvents-witness(),
run-event-msg: run-event-msg(r;e),
runEvents: runEvents(r),
mk-eo: mk-eo(E;dom;l;R;a;b;c;d;e;f),
btrue: tt,
lambda: x.A[x],
token: "$token",
record-update: r[x := v]
Definitions :
record-update: r[x := v],
mk-eo: mk-eo(E;dom;l;R;a;b;c;d;e;f),
runEvents: runEvents(r),
btrue: tt,
run-event-loc: run-event-loc(e),
run-lt: run-lt(r),
deq-runEvents-witness: deq-runEvents-witness(),
well-founded-run-lt-witness: well-founded-run-lt-witness(),
decd-run-lt: decd-run-lt(r),
run-lt-transitive-witness: run-lt-transitive-witness(),
finite-run-lt-witness: finite-run-lt-witness(r),
total-run-lt-witness: total-run-lt-witness(),
token: "$token",
lambda: x.A[x],
run-event-msg: run-event-msg(r;e)
FDL editor aliases :
run-eo
EO(r) ==
mk-eo(runEvents(r);\mlambda{}e.tt;\mlambda{}e.run-event-loc(e);run-lt(r);deq-runEvents-witness();
well-founded-run-lt-witness();decd-run-lt(r);run-lt-transitive-witness();
finite-run-lt-witness(r);total-run-lt-witness())["info" := \mlambda{}e.run-event-msg(r;e)]
Date html generated:
2011_08_17-PM-03_39_19
Last ObjectModification:
2010_12_17-AM-01_00_39
Home
Index