Nuprl Definition : pi-run-example
pi-run-example{$l_server,$l_choose,$l_comm,$l_pi,$a,$b,$c,$d,$e,$f,$g}(P;t) ==
pRun2(pi-system-example{$l_server,$l_choose,$l_comm,$l_pi,$a,$b,$c,
$d,$e,$f,$g}(P);std-env("$l_server");λn.pDVfire();λl.pDVfire();t)
Definitions occuring in Statement :
pi-system-example: pi-system-example{$l_server,$l_choose,$l_comm,$l_pi,$a,$b,$c,$d,$e,$f,$g}(P),
pDVfire: pDVfire(),
std-env: std-env(nm),
pRun2: pRun2(S0;env;nat2msg;loc2msg;t),
mkid: "$x",
lambda: λx.A[x]
FDL editor aliases :
pi-run-example
Latex:
pi-run-example\{\$l\_server,\$l\_choose,\$l\_comm,\$l\_pi,\$a,\$b,\$c,\$d,\$e,\$f,\$g\}(P;t) ==
pRun2(pi-system-example\{\$l\_server,\$l\_choose,\$l\_comm,\$l\_pi,\$a,\$b,\$c,
\$d,\$e,\$f,\$g\}(P);std-env("\$l\_server");\mlambda{}n.pDVfire();\mlambda{}l.pDVfire();t)
Date html generated:
2015_07_23-AM-11_59_42
Last ObjectModification:
2012_08_30-PM-01_51_06
Home
Index