Nuprl Definition : paxos_A3
paxos_A3{i:l}(es;AcceptorState) ==
all-class-value-ordered-pairs+{i:l}(es;acceptor-state();AcceptorState;as1,as2.let acc1 = accepted(as1) in
let acc2 = accepted(as2) in
list_contained-in(acc1;acc2;PValue()))
Proof not projected
Definitions occuring in Statement :
accepted: accepted(astate),
acceptor-state: acceptor-state(),
PValue: PValue(),
all-class-value-ordered-pairs+: all-class-value-ordered-pairs+{i:l}(es;T;A;t1,t2.Q[t1; t2]),
list_contained-in: list_contained-in(L1;L2;T),
let: let
Definitions :
all-class-value-ordered-pairs+: all-class-value-ordered-pairs+{i:l}(es;T;A;t1,t2.Q[t1; t2]),
acceptor-state: acceptor-state(),
let: let,
accepted: accepted(astate),
list_contained-in: list_contained-in(L1;L2;T),
PValue: PValue()
FDL editor aliases :
paxos_A3
paxos\_A3\{i:l\}(es;AcceptorState) ==
all-class-value-ordered-pairs+\{i:l\}(es;acceptor-state();AcceptorState;as1,as2.let acc1 = ... in
let acc2 = ... in
...)
Date html generated:
2011_10_20-PM-11_58_25
Last ObjectModification:
2011_05_19-AM-09_48_11
Home
Index