Nuprl Definition : nysiad_MessageBagInput-program

nysiad_MessageBagInput-program(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf) ==

eclass0-program(λslf,x. {inl x};

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

|| eclass0-program(λslf,x. {inr x };

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

Definitions occuring in Statement : nysiad_addwaiting'base-program: nysiad_addwaiting'base-program(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf), nysiad_add2bag'base-program: nysiad_add2bag'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_MessageBagInput-program

Latex:
nysiad\_MessageBagInput-program(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;...;...;...;mf) == eclass0-program(\mlambda{}slf,x. \{inl x\}; nysiad\_addwaiting'base-program(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;...;...;...;mf)) || eclass0-program(\mlambda{}slf,x. \{inr x \}; nysiad\_add2bag'base-program(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;...;...;...;mf)) Date html generated: 2016_05_17-PM-01_26_23 Last ObjectModification: 2014_08_06-PM-03_31_35 Theory : event-logic-applications Home Index