Nuprl Definition : chosen-command
chosen-command(P.M[P];env;r;t;x) ==
let Cs,G = run-system(r;t)
in let n = fst((env t r)) in
(↑lg-is-source(G;n)) ∧ (x = lg-label(G;n) ∈ pInTransit(P.M[P]))
Definitions occuring in Statement :
run-system: run-system(r;t),
pInTransit: pInTransit(P.M[P]),
lg-is-source: lg-is-source(g;i),
lg-label: lg-label(g;x),
assert: ↑b,
let: let,
pi1: fst(t),
and: P ∧ Q,
apply: f a,
spread: spread def,
equal: s = t ∈ T
FDL editor aliases :
chosen-command
Latex:
chosen-command(P.M[P];env;r;t;x) ==
let Cs,G = run-system(r;t)
in let n = fst((env t r)) in
(\muparrow{}lg-is-source(G;n)) \mwedge{} (x = lg-label(G;n))
Date html generated:
2015_07_23-AM-11_16_46
Last ObjectModification:
2012_02_25-PM-03_44_55
Home
Index