Nuprl Definition : CLK_messages-delivered
CLK_messages-delivered{i:l}(MsgType;locs;reply;f) == msgs-interface-delivered{i:l}(CLK_main(MsgType;locs;reply;f);f)
Definitions occuring in Statement :
CLK_main: CLK_main(MsgType;locs;reply;f),
msgs-interface-delivered: msgs-interface-delivered{i:l}(X;f)
FDL editor aliases :
CLK_messages-delivered
Latex:
CLK\_messages-delivered\{i:l\}(MsgType;locs;reply;f) ==
msgs-interface-delivered\{i:l\}(CLK\_main(MsgType;locs;reply;f);f)
Date html generated:
2016_05_17-PM-02_45_35
Last ObjectModification:
2013_11_23-PM-09_22_49
Theory : lamport!s!clocks
Home
Index