Nuprl Definition : choosable-command
choosable-command(P.M[P];r;t;x) ==
let Cs,G = run-system(r;t)
in ∃n:ℕ. ((↑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),
nat: ℕ,
assert: ↑b,
exists: ∃x:A. B[x],
and: P ∧ Q,
spread: spread def,
equal: s = t ∈ T
FDL editor aliases :
choosable-command
Latex:
choosable-command(P.M[P];r;t;x) ==
let Cs,G = run-system(r;t)
in \mexists{}n:\mBbbN{}. ((\muparrow{}lg-is-source(G;n)) \mwedge{} (x = lg-label(G;n)))
Date html generated:
2015_07_23-AM-11_16_42
Last ObjectModification:
2012_02_25-PM-03_44_49
Home
Index