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)))
Definitions :
spread: spread def,
run-system: run-system(r;t),
exists: x:A. B[x],
nat: ,
and: P Q,
assert: b,
lg-is-source: lg-is-source(g;i),
equal: s = t,
pInTransit: pInTransit(P.M[P]),
lg-label: lg-label(g;x)
FDL editor aliases :
choosable-command
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:
2010_08_27-PM-06_44_02
Last ObjectModification:
2010_05_05-PM-01_04_43
Home
Index