Nuprl Lemma : Paxos-spec9-properties

es:event_system{i:l}.

T:Type.

leaders,failset:Id List.

tg1a:Id.

Decide,Input:Temporary AbsInterface(es;T).
(Paxos-spec9(es;T;leaders;failset;tg1a;Decide;Input)

(Decide values come from Input values

Consistent(Decide)

((

ldr

leaders. (

(ldr

failset))

(

ldr'

leaders.(

(ldr' = ldr))

(rcvs from ldr' with tag tg1a are bounded))

(

n:E(Input). (loc(n) = ldr)))

(

d:E. (

(d in Decide))))))

Proof not projected

Error : references

\mforall{}es:event\_system\{i:l\}. \mforall{}T:Type. \mforall{}leaders,failset:Id List. \mforall{}tg1a:Id. \mforall{}Decide,Input:Temporary AbsInterface(es;T). (Paxos-spec9(es;T;leaders;failset;tg1a;Decide;Input) {}\mRightarrow{} (Decide values come from Input values \mwedge{} Consistent(Decide) \mwedge{} ((\mexists{}ldr\mmember{}leaders. (\mneg{}(ldr \mmember{} failset)) \mwedge{} (\mforall{}ldr'\mmember{}leaders.(\mneg{}(ldr' = ldr)) {}\mRightarrow{} (rcvs from ldr' with tag tg1a are bounded)) \mwedge{} (\mexists{}n:E(Input). (loc(n) = ldr))) {}\mRightarrow{} (\mexists{}d:E. (\muparrow{}(d in Decide)))))) Date html generated: 2012_02_20-PM-07_50_51 Last ObjectModification: 2010_07_15-PM-03_07_10 Home Index