Nuprl Definition : run-pred
run-pred(r) ==
λe1,e2. (((run-event-loc(e1) = run-event-loc(e2) ∈ Id) ∧ run-event-step(e1) < run-event-step(e2))
∨ (e1 = (fst(run-info(r;e2))) ∈ (ℤ × Id)))
Definitions occuring in Statement :
run-event-step: run-event-step(e),
run-event-loc: run-event-loc(e),
run-info: run-info(r;e),
Id: Id,
less_than: a < b,
pi1: fst(t),
or: P ∨ Q,
and: P ∧ Q,
lambda: λx.A[x],
product: x:A × B[x],
int: ℤ,
equal: s = t ∈ T
FDL editor aliases :
run-pred
Latex:
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:
2015_07_23-AM-11_13_47
Last ObjectModification:
2012_02_25-PM-03_42_25
Home
Index