Nuprl Definition : pv11_p1_decision
pv11_p1_decision{i:l}(Cmd;f;accpts;ldrs;ldrs_uid;reps;es;e;k;v) ==
∃delay:ℤ. ∃client:Id. make-msg-interface(delay;client;make-Msg([decision];<k, v>)) ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs\000C_uid;reps;f)(e)
Definitions occuring in Statement :
pv11_p1_main: pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;mf),
make-msg-interface: make-msg-interface(i;l;m),
msg-interface: Interface,
make-Msg: make-Msg(hdr;val),
classrel: v ∈ X(e),
Id: Id,
cons: [a / b],
nil: [],
exists: ∃x:A. B[x],
pair: <a, b>,
int: ℤ,
token: "$token"
FDL editor aliases :
pv11_p1_decision
Latex:
pv11\_p1\_decision\{i:l\}(Cmd;f;accpts;ldrs;ldrs$_{uid}$;reps;es;e;k;v) ==
\mexists{}delay:\mBbbZ{}. \mexists{}client:Id. make-msg-interface(delay;client;make-Msg([decision];<k, v>)) \mmember{} pv11\_p1\_main(\000CCmd;accpts;ldrs;ldrs$_{uid}$;reps;f)(e)
Date html generated:
2016_05_17-PM-04_16_34
Last ObjectModification:
2013_12_18-PM-06_19_42
Theory : paxos!synod
Home
Index