Nuprl Definition : nysiad

Nuprl Definition : nysiad_MessageBag

nysiad_MessageBag(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;inputmsghdr;kdeliverhdr;readyhdr;...;...;...;mf;msg2m) ==

  ((nysiad_on_input_message_bag(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;inputmsghdr;...;...;...;...;...;mf;msg2m) o

nysiad_MessageBagInput(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf)) o

  nysiad_MessageBagState(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;inputmsghdr;kdeliverhdr;readyhdr;...;...;mf;msg2m))

Definitions occuring in Statement : nysiad_MessageBagInput: nysiad_MessageBagInput(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf), nysiad_on_input_message_bag: nysiad_on_input_message_bag(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;inputmsghdr;kdeliverhdr;...;...;...;...;mf;...), nysiad_MessageBagState: nysiad_MessageBagState(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;inputmsghdr;kdeliverhdr;readyhdr;...;...;mf;msg2m), eclass2: (X o Y), eclass1: (f o X)
FDL editor aliases : nysiad_MessageBag

Latex:
nysiad\_MessageBag(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;...;...;...;senders;...;...;mf;...) == (... o nysiad\_MessageBagState(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;...;...;...;...;...;mf;msg2m)) Date html generated: 2015_07_23-PM-03_44_54 Last ObjectModification: 2014_08_06-PM-03_31_47 Home Index