Nuprl Definition : run-msg-commands
run-msg-commands(r) ==
t:ℕ × {n:ℕ| run-command-node(r;t;n) ∧ (com-kind(snd(snd(run-command(r;t;n)))) ∈ ``msg choose new``)}
Definitions occuring in Statement :
run-command: run-command(r;t;n),
run-command-node: run-command-node(r;t;n),
com-kind: com-kind(c),
l_member: (x ∈ l),
cons: [a / b],
nil: [],
nat: ℕ,
pi2: snd(t),
and: P ∧ Q,
set: {x:A| B[x]} ,
product: x:A × B[x],
token: "$token",
atom: Atom
FDL editor aliases :
run-msg-commands
Latex:
run-msg-commands(r) ==
t:\mBbbN{} \mtimes{} \{n:\mBbbN{}|
run-command-node(r;t;n) \mwedge{} (com-kind(snd(snd(run-command(r;t;n)))) \mmember{} ``msg choose new``)\}
Date html generated:
2015_07_23-AM-11_17_23
Last ObjectModification:
2012_02_25-PM-03_45_34
Home
Index