---

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;...;||l|| + 4)
               of inl(x) => x
                | inr(x) => "$g";"$l_server";"$l_choose";"$l_comm";"$l_pi") 
  P

---

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

---

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: 2010_08_28-AM-01_42_08
Last ObjectModification: 2010_05_04-PM-06_03_44

Home Index