Nuprl Definition : OARcast_SenderState
OARcast_SenderState(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf) ==
state-class1(λslf.0;OARcast_on_oarcast_update(M);OARcast_oarcast'base(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf))
Definitions occuring in Statement :
OARcast_on_oarcast_update: OARcast_on_oarcast_update(M),
OARcast_oarcast'base: OARcast_oarcast'base(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf),
state-class1: state-class1(init;tr;X),
lambda: λx.A[x],
natural_number: $n
FDL editor aliases :
OARcast_SenderState
Latex:
OARcast\_SenderState(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf) ==
state-class1(\mlambda{}slf.0;OARcast\_on\_oarcast\_update(M);OARcast\_oarcast'base(M;...;...;...;orderhdr;mf))
Date html generated:
2015_07_23-PM-00_30_19
Last ObjectModification:
2014_08_20-PM-00_01_48
Home
Index