Nuprl Definition : nysiad_MessageBagState
nysiad_MessageBagState(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;inputmsghdr;kdeliverhdr;readyhdr;...;...;mf;msg2m) ==
memory-class2(λslf.<[], map-sig-empty(waitingmap)>;
nysiad_add_waiting(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;inputmsghdr;...;readyhdr;...;...;mf;...);
nysiad_addwaiting'base(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;...;mf);
nysiad_add_to_bag(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;inputmsghdr;...;readyhdr;...;...;mf;...);
nysiad_add2bag'base(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;...;mf))
Definitions occuring in Statement :
nysiad_add_to_bag: nysiad_add_to_bag(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;...;mf;...),
nysiad_add_waiting: nysiad_add_waiting(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;...;mf;...),
nysiad_addwaiting'base: nysiad_addwaiting'base(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf),
nysiad_add2bag'base: nysiad_add2bag'base(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf),
memory-class2: memory-class2(init;tr1;X1;tr2;X2),
nil: [],
lambda: λx.A[x],
pair: <a, b>,
map-sig-empty: map-sig-empty(m)
FDL editor aliases :
nysiad_MessageBagState
Latex:
nysiad\_MessageBagState(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;...;...;...;...;...;mf;msg2m) ==
...
Date html generated:
2015_07_23-PM-03_43_25
Last ObjectModification:
2014_08_06-PM-03_29_55
Home
Index