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>
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:
2016_05_17-PM-01_24_59
Last ObjectModification:
2014_08_06-PM-03_30_31
Theory : event-logic-applications
Home
Index