Nuprl Definition : paxos_R4

paxos_R4{i:l}(RepState; es; ReplicaState) ==
  all-class-value-ordered-pairs+{i:l}(es;replica-state(RepState);ReplicaState;rs1,rs2.let sn1 = slot_num(rs1) in
                                                                                       let sn2 = slot_num(rs2) in
                                                                                       sn1  sn2)


Proof not projected



Definitions occuring in Statement :  slot_num: slot_num(rstate),  replica-state: replica-state(RepState),  all-class-value-ordered-pairs+: all-class-value-ordered-pairs+{i:l}(es;T;A;t1,t2.Q[t1; t2]),  let: let,  le: A  B
Definitions :  all-class-value-ordered-pairs+: all-class-value-ordered-pairs+{i:l}(es;T;A;t1,t2.Q[t1; t2]),  replica-state: replica-state(RepState),  let: let,  slot_num: slot_num(rstate),  le: A  B
paxos\_R4\{i:l\}(RepState;  es;  ReplicaState)  ==
    all-class-value-ordered-pairs+\{i:l\}(es;replica-state(RepState);ReplicaState;rs1,rs2....)


Date html generated: 2011_10_20-PM-11_54_54
Last ObjectModification: 2011_05_12-PM-01_48_21

Home Index