Nuprl Definition : nysiad_InputQueue-program

nysiad_InputQueue-program(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf) ==
  eclass0-program(λslf,x. {inl x};
  nysiad_kdeliver'base-program(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf))
  || eclass0-program(λslf,x. {inr x };

     nysiad_ready'base-program(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf))

Definitions occuring in Statement : nysiad_kdeliver'base-program: nysiad_kdeliver'base-program(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf), nysiad_ready'base-program: nysiad_ready'base-program(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf), parallel-class-program: X || Y, eclass0-program: eclass0-program(f;pr), lambda: λx.A[x], inr: inr x , inl: inl x, single-bag: {x}
FDL editor aliases : nysiad_InputQueue-program

Latex:
nysiad\_InputQueue-program(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;...;readyhdr;...;mf) == eclass0-program(\mlambda{}slf,x. \{inl x\}; nysiad\_kdeliver'base-program(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;...;...;...;mf)) || eclass0-program(\mlambda{}slf,x. \{inr x \}; nysiad\_ready'base-program(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;...;...;...;mf)) Date html generated: 2015_07_23-PM-03_46_08 Last ObjectModification: 2014_08_06-PM-03_33_34 Home Index