Nuprl Definition : pi-system-example

pi-system-example{$l_server,$l_choose,$l_comm,$l_pi,$a,$b,$c,$d,$e,$f,$g}(P) ==

  pi-system(λl.case apply-alist(NatDeq;ten-locs{$l_server,$l_choose,$l_comm,$l_pi,$a,$b,$c,$d,$e,$f,$g}();||l|| + 4)

                of inl(x) =>
                x
                | inr(x) =>
                "$g";"$l_server";"$l_choose";"$l_comm";"$l_pi")
  P

Definitions occuring in Statement : pi-system: pi-system(f;l_server;l_choose;l_comm;l_pi), ten-locs: ten-locs{$l_server,$l_choose,$l_comm,$l_pi,$a1,$a2,$a3,$a4,$a5,$a6,$a7}(), mkid: "$x", apply-alist: apply-alist(eq;L;x), nat-deq: NatDeq, length: ||as||, apply: f a, lambda: λx.A[x], decide: case b of inl(x) => s[x] | inr(y) => t[y], add: n + m, natural_number: $n
FDL editor aliases : pi-system-example

Latex:
pi-system-example\{\$l\_server,\$l\_choose,\$l\_comm,\$l\_pi,\$a,\$b,\$c,\$d,\$e,\$f,\$g\}(P) == pi-system(\mlambda{}l.case apply-alist(NatDeq;...;||l|| + 4) of inl(x) => x | inr(x) => "\$g";"\$l\_server";"\$l\_choose";"\$l\_comm";"\$l\_pi") P Date html generated: 2015_07_23-AM-11_59_38 Last ObjectModification: 2012_08_30-PM-01_51_00 Home Index