Nuprl Definition : paxos_R1
paxos_R1{i:l}(RepState; es; ReplicaState) ==
all-class-value-pairs+{i:l}(es;replica-state(RepState);ReplicaState;rs1,rs2.compat-pair-lists(...;...;
;Command()))
Proof not projected
Definitions occuring in Statement :
proposals: proposals(rstate),
replica-state: replica-state(RepState),
Command: Command(),
compat-pair-lists: compat-pair-lists(x;y;S;T),
all-class-value-pairs+: all-class-value-pairs+{i:l}(es;T;A;t1,t2.Q[t1; t2]),
int:
Definitions :
all-class-value-pairs+: all-class-value-pairs+{i:l}(es;T;A;t1,t2.Q[t1; t2]),
replica-state: replica-state(RepState),
compat-pair-lists: compat-pair-lists(x;y;S;T),
proposals: proposals(rstate),
int: ,
Command: Command()
paxos\_R1\{i:l\}(RepState; es; ReplicaState) ==
all-class-value-pairs+\{i:l\}(es;replica-state(RepState);ReplicaState;rs1,rs2....)
Date html generated:
2011_10_20-PM-11_53_53
Last ObjectModification:
2011_05_12-PM-01_33_05
Home
Index