Nuprl Definition : acceptor
acceptor(Op;self) ==
smr-class(<inr 
, []>;s,m.let ballot,accptd = s
in case m
of inl(p) =>
let ldr,b = p
in let b' = ballot-max(ballot;b) in
<<b', accptd>, msg1b(Op;self;b';accptd), ldr>
| inr(q) =>
let ldr,b,c,cmd = q
in let b' = ballot-max(ballot;b) in
<<b'
, if eq_ballot(b';b)
then update-alist(IntDeq;accptd;c;<b, cmd>;v.<b, cmd>)
else accptd
fi
>
, msg2b(self; b'; c)
, ldr> ;class1a()+class2a(Op))
Proof not projected
Definitions occuring in Statement :
msg2b: msg2b(self; b; c),
msg1b: msg1b(Op;self;b;accptd),
class2a: class2a(Op),
class1a: class1a(),
ballot-max: ballot-max(b1;b2),
eq_ballot: eq_ballot(b1;b2),
smr-class: smr-class(init;s,x.F[s; x];X),
es-interface-union: X+Y,
ifthenelse: if b then t else f fi ,
let: let,
it: ,
spreadn: spread4,
spread: spread def,
pair: <a, b>,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inr: inr x ,
nil: [],
update-alist: update-alist(eq;L;x;z;v.f[v]),
int-deq: IntDeq
Definitions :
smr-class: smr-class(init;s,x.F[s; x];X),
inr: inr x ,
it: ,
nil: [],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
spread: spread def,
msg1b: msg1b(Op;self;b;accptd),
spreadn: spread4,
let: let,
ballot-max: ballot-max(b1;b2),
ifthenelse: if b then t else f fi ,
eq_ballot: eq_ballot(b1;b2),
update-alist: update-alist(eq;L;x;z;v.f[v]),
int-deq: IntDeq,
pair: <a, b>,
msg2b: msg2b(self; b; c),
es-interface-union: X+Y,
class1a: class1a(),
class2a: class2a(Op)
FDL editor aliases :
acceptor
acceptor(Op;self) ==
smr-class(<inr \mcdot{} , []>s,m.let ballot,accptd = s
in case m
of inl(p) =>
let ldr,b = p
in let b' = ballot-max(ballot;b) in
<<b', accptd>, msg1b(Op;self;b';accptd), ldr>
| inr(q) =>
let ldr,b,c,cmd = q
in let b' = ballot-max(ballot;b) in
<<b'
, if eq\_ballot(b';b)
then update-alist(IntDeq;accptd;c;<b, cmd>v.<b, cmd>)
else accptd
fi
>
, msg2b(self; b'; c)
, ldr> ;class1a()+class2a(Op))
Date html generated:
2011_10_20-PM-04_23_21
Last ObjectModification:
2011_01_26-PM-05_29_54
Home
Index