Nuprl Definition : nysiad_MessageBagState-program
nysiad_MessageBagState-program(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;inputmsghdr;...;readyhdr;...;...;mf;msg2m) ==
memory-class2-program(λslf.<[], map-sig-empty(waitingmap)>;...;...;...;...)
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-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)
,
memory-class2-program: memory-class2-program(init;tr1;pr1;tr2;pr2)
,
nil: []
,
lambda: λx.A[x]
,
pair: <a, b>
,
map-sig-empty: map-sig-empty(m)
FDL editor aliases :
nysiad_MessageBagState-program
Latex:
nysiad\_MessageBagState-program(M;add2baghdr;addwaitinghdr;...;deqM;...;...;...;...;...;mf;msg2m) ==
memory-class2-program(\mlambda{}slf.<[], map-sig-empty(waitingmap)>...;...;...;...)
Date html generated:
2015_07_23-PM-03_43_50
Last ObjectModification:
2014_08_06-PM-03_30_31
Home
Index