Nuprl Definition : paxos_R2

paxos_R2{i:l}(RepState; es; ReplicaState) ==
  all-class-values+{i:l}(es;replica-state(RepState);ReplicaState;rs.let sn = slot_num(rs) in
                                                                     let ds = decisions(rs) in
                                                                     let decided = map(x.(fst(x));ds) in
                                                                     i:. (((1  i)  (i < sn))  (i  decided)))


Proof not projected



Definitions occuring in Statement :  decisions: decisions(rstate),  slot_num: slot_num(rstate),  replica-state: replica-state(RepState),  all-class-values+: all-class-values+{i:l}(es;T;A;t.P[t]),  map: map(f;as),  let: let,  pi1: fst(t),  le: A  B,  all: x:A. B[x],  implies: P  Q,  and: P  Q,  less_than: a < b,  lambda: x.A[x],  natural_number: $n,  int: ,  l_member: (x  l)
Definitions :  all-class-values+: all-class-values+{i:l}(es;T;A;t.P[t]),  replica-state: replica-state(RepState),  slot_num: slot_num(rstate),  decisions: decisions(rstate),  let: let,  map: map(f;as),  lambda: x.A[x],  pi1: fst(t),  all: x:A. B[x],  implies: P  Q,  and: P  Q,  le: A  B,  natural_number: $n,  less_than: a < b,  l_member: (x  l),  int:
paxos\_R2\{i:l\}(RepState;  es;  ReplicaState)  ==
    all-class-values+\{i:l\}(es;replica-state(RepState);ReplicaState;rs.let  sn  =  slot\_num(rs)  in
                                                                                                                                          let  ds  =  decisions(rs)  in
                                                                                                                                          let  decided  =  map(\mlambda{}x.(fst(x));
                                                                                                                                                                              ds)  in
                                                                                                                                          \mforall{}i:\mBbbZ{}
                                                                                                                                              (((1  \mleq{}  i)  \mwedge{}  (i  <  sn))
                                                                                                                                              {}\mRightarrow{}  (i  \mmember{}  decided)))


Date html generated: 2011_10_20-PM-11_54_23
Last ObjectModification: 2011_05_12-PM-01_40_01

Home Index