Nuprl Definition : nysiad_on_input_message

Nuprl Definition : nysiad_on_input_message_bag

nysiad_on_input_message_bag(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;inputmsghdr;...;readyhdr;...;...;...;mf;...) ==
λslf,i,s. if isl(i)

           then nysiad_on_addwaiting(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;inputmsghdr;...;...;...;...;mf;msg2m)

                slf
                outl(i)
                s

           else nysiad_on_add2bag(M;add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;...;...;...;...;mf)

                slf
                outr(i)
                s
           fi

Definitions occuring in Statement : nysiad_on_add2bag: nysiad_on_add2bag(M;add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;senders;tooarcasthdr;...;mf), nysiad_on_addwaiting: nysiad_on_addwaiting(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;inputmsghdr;kdeliverhdr;readyhdr;...;waitingmap;mf;...), outr: outr(x), outl: outl(x), ifthenelse: if b then t else f fi , isl: isl(x), apply: f a, lambda: λx.A[x]
FDL editor aliases : nysiad_on_input_message_bag

Latex:
nysiad\_on\_input\_message\_bag(M;add2baghdr;addwaitinghdr;...;deqM;...;...;...;...;...;...;mf;msg2m) == \mlambda{}slf,i,s. if isl(i) then nysiad\_on\_addwaiting(M;add2baghdr;addwaitinghdr;...;...;...;...;...;...;...;mf;...) slf outl(i) s else nysiad\_on\_add2bag(M;add2baghdr;addwaitinghdr;...;...;...;readyhdr;...;...;...;mf) slf outr(i) s fi Date html generated: 2015_07_23-PM-03_44_26 Last ObjectModification: 2014_08_06-PM-03_31_09 Home Index