Nuprl Definition : CLK_upd_clock
CLK_upd_clock(MsgType) ==  λslf,z,clock. let z,timestamp = z in imax(timestamp;clock) + 1
Definitions occuring in Statement : 
imax: imax(a;b)
, 
lambda: λx.A[x]
, 
spread: spread def, 
add: n + m
, 
natural_number: $n
FDL editor aliases : 
CLK_upd_clock
Latex:
CLK\_upd\_clock(MsgType)  ==    \mlambda{}slf,z,clock.  let  z,timestamp  =  z  in  imax(timestamp;clock)  +  1
Date html generated:
2016_05_17-PM-02_44_22
Last ObjectModification:
2013_11_23-PM-09_22_17
Theory : lamport!s!clocks
Home
Index