Nuprl Definition : commander

commander(ldr;num;acceptors;b;c) ==
once-class(smr-class(acceptors;waitfor,m.let a,b' = m
in let wait = filter(

x.(

x = a);waitfor) in
                                                  <wait
                                                  , if eq_ballot(b;b')
                                                    then if 2 * ||wait|| <z num
                                                         then inl <msgPreempted(b'), ldr>
                                                         else inr

                                                         fi
                                                    else inl <msgPreempted(b'), ldr>
                                                    fi
                                                  >;class2b(c)))

Proof not projected

Definitions occuring in Statement : msgPreempted: msgPreempted(b), class2b: class2b(c), eq_ballot: eq_ballot(b1;b2), smr-class: smr-class(init;s,x.F[s; x];X), once-class: once-class(X), eq_id: a = b, length: ||as||, bnot:

b, lt_int: i <z j, ifthenelse: if b then t else f fi , let: let, it:

, lambda:

x.A[x], spread: spread def, pair: <a, b>, inr: inr x , inl: inl x , multiply: n * m, natural_number: $n, filter: filter(P;l)
Definitions : once-class: once-class(X), smr-class: smr-class(init;s,x.F[s; x];X), spread: spread def, let: let, filter: filter(P;l), lambda:

x.A[x], bnot:

b, eq_id: a = b, eq_ballot: eq_ballot(b1;b2), ifthenelse: if b then t else f fi , lt_int: i <z j, multiply: n * m, natural_number: $n, length: ||as||, inr: inr x , it:

, inl: inl x , pair: <a, b>, msgPreempted: msgPreempted(b), class2b: class2b(c)
FDL editor aliases : commander

commander(ldr;num;acceptors;b;c) == once-class(smr-class(acceptors;waitfor,m.let a,b' = m in let wait = filter(\mlambda{}x.(\mneg{}\msubb{}x = a);waitfor) in <wait , if eq\_ballot(b;b') then if 2 * ||wait|| <z num then inl <msgPreempted(b'), ldr> else inr \mcdot{} fi else inl <msgPreempted(b'), ldr> fi >class2b(c))) Date html generated: 2011_10_20-PM-04_24_14 Last ObjectModification: 2011_01_29-AM-00_59_25 Home Index