Nuprl Definition : pi-system
pi-system(f;l_server;l_choose;l_comm;l_pi) ==
λP.<[<l_server, loc-Server(f;[l_server; l_choose; l_comm; l_pi];1)>; <l_choose, processChoose(l_comm)>; <l_comm, proce\000CssComm(l_comm;l_choose)>; <l_pi, pi-trans(l_server;P) l_pi nat-to-incomparable(0) pi-names(P)>]
, make-lg([<<-1, l_pi>, l_pi, "msg", pDVfire()>])
>
Definitions occuring in Statement :
pi-trans: pi-trans(l_loc;P),
processComm: processComm(l_comm;l_choose),
processChoose: processChoose(l_comm),
loc-Server: loc-Server(f;L0;n0),
pDVfire: pDVfire(),
pi-names: pi-names(p),
make-lg: make-lg(L),
nat-to-incomparable: nat-to-incomparable(n),
cons: [a / b],
nil: [],
apply: f a,
lambda: λx.A[x],
pair: <a, b>,
minus: -n,
natural_number: $n,
token: "$token"
FDL editor aliases :
pi-system
Latex:
pi-system(f;l$_{server}$;l$_{choose}$;l$_{comm\mbackslash{}f\000Cf7d$;l$_{pi}$) ==
\mlambda{}P.<[<l$_{server}$, loc-Server(f;[l$_{server}$; l$\mbackslash{}ff5\000Cf{choose}$; l$_{comm}$; l$_{pi}$];1)>
<l$_{choose}$, processChoose(l$_{comm}$)>
<l$_{comm}$, processComm(l$_{comm}$;l$_{c\000Choose}$)>
<l$_{pi}$, pi-trans(l$_{server}$;P) l$_{p\000Ci}$ nat-to-incomparable(0) pi-names(P)>]
, make-lg([<<-1, l$_{pi}$>, l$_{pi}$, "msg", pDVfire()>\000C])
>
Date html generated:
2015_07_23-AM-11_59_34
Last ObjectModification:
2012_08_30-PM-01_50_54
Home
Index