Nuprl Definition : scout

scout(Op;ldr;num;acceptors;b) ==
  once-class(smr-class(<acceptors, []>;s,m.let a,b',r = m in
  let waitfor,pvals = s
  in let wait = filter(

x.(

x = a);waitfor) in
      let pvals' = pvals @ r in
      <<wait, pvals'>
      , if eq_ballot(b;b')
        then if 2 * ||wait|| <z num then inl <msgAdopted(Op;b;pvals'), ldr>  else inr

  fi
        else inl <msgPreempted(b'), ldr>
        fi
      >;class1b(Op)))

Proof not projected

Definitions occuring in Statement : msgAdopted: msgAdopted(Op;b;pvals), msgPreempted: msgPreempted(b), class1b: class1b(Op), 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||, append: as @ bs, bnot:

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

, spreadn: spread3, lambda:

x.A[x], spread: spread def, pair: <a, b>, inr: inr x , inl: inl x , nil: [], 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), nil: [], spreadn: spread3, spread: spread def, filter: filter(P;l), lambda:

x.A[x], bnot:

b, eq_id: a = b, let: let, append: as @ bs, 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||, msgAdopted: msgAdopted(Op;b;pvals), inr: inr x , it:

, inl: inl x , pair: <a, b>, msgPreempted: msgPreempted(b), class1b: class1b(Op)
FDL editor aliases : scout

scout(Op;ldr;num;acceptors;b) == once-class(smr-class(<acceptors, []>s,m.let a,b',r = m in let waitfor,pvals = s in let wait = filter(\mlambda{}x.(\mneg{}\msubb{}x = a);waitfor) in let pvals' = pvals @ r in <<wait, pvals'> , if eq\_ballot(b;b') then if 2 * ||wait|| <z num then inl <msgAdopted(Op;b;pvals'), ldr> else inr \mcdot{} fi else inl <msgPreempted(b'), ldr> fi >class1b(Op))) Date html generated: 2011_10_20-PM-04_24_53 Last ObjectModification: 2011_01_26-PM-04_03_30 Home Index