Nuprl Definition : paxos_A4
paxos_A4{i:l}(es;AcceptorState) ==
all-class-value-pairs+{i:l}(es;acceptor-state();AcceptorState;as1,as2.let acc1 = accepted(as1) in
let acc2 = accepted(as2) in
compat-trip-lists(acc1;acc2;Ballot_Num();
;...)\000C)
Proof not projected
Definitions occuring in Statement :
accepted: accepted(astate),
acceptor-state: acceptor-state(),
Command: Command(),
Ballot_Num: Ballot_Num(),
compat-trip-lists: compat-trip-lists(x;y;R;S;T),
all-class-value-pairs+: all-class-value-pairs+{i:l}(es;T;A;t1,t2.Q[t1; t2]),
let: let,
int:
Definitions :
all-class-value-pairs+: all-class-value-pairs+{i:l}(es;T;A;t1,t2.Q[t1; t2]),
acceptor-state: acceptor-state(),
let: let,
accepted: accepted(astate),
compat-trip-lists: compat-trip-lists(x;y;R;S;T),
Ballot_Num: Ballot_Num(),
int: ,
Command: Command()
FDL editor aliases :
paxos_A4
paxos\_A4\{i:l\}(es;AcceptorState) ==
all-class-value-pairs+\{i:l\}(es;acceptor-state();AcceptorState;as1,as2.let acc1 = accepted(as1) in
let acc2 = accepted(as2) in
...)
Date html generated:
2011_10_20-PM-11_58_57
Last ObjectModification:
2011_05_13-PM-05_13_04
Home
Index