Nuprl Definition : RSC-slow-round

RSC-slow-round(Cmd;es;n;r;slow) ==

i,j:Id.

e1,e2:E.

c1,c2:Cmd.
((loc(e1) = loc(e2))

(

loc(e1)

slow)

(

i

slow)

j

slow

<<<n, r>, c1>, i>

RSC_Vote(Cmd)(e1)

<<<n, r>, c2>, j>

RSC_Vote(Cmd)(e2)

(e1 <loc e2))

Definitions occuring in Statement : RSC_Vote: RSC_Vote(Cmd), classrel: v

X(e), es-locl: (e <loc e'), es-loc: loc(e), es-E: E, Id: Id, all:

x:A. B[x], not:

A, implies: P

Q, pair: <a, b>, product: x:A

B[x], int:

, equal: s = t, bag-member: x

bs
FDL editor aliases : RSC-slow-round

RSC-slow-round(Cmd;es;n;r;slow) == \mforall{}i,j:Id. \mforall{}e1,e2:E. \mforall{}c1,c2:Cmd. ((loc(e1) = loc(e2)) {}\mRightarrow{} (\mneg{}loc(e1) \mdownarrow{}\mmember{} slow) {}\mRightarrow{} (\mneg{}i \mdownarrow{}\mmember{} slow) {}\mRightarrow{} j \mdownarrow{}\mmember{} slow {}\mRightarrow{} <<<n, r>, c1>, i> \mmember{} RSC\_Vote(Cmd)(e1) {}\mRightarrow{} <<<n, r>, c2>, j> \mmember{} RSC\_Vote(Cmd)(e2) {}\mRightarrow{} (e1 <loc e2)) Date html generated: 2012_02_20-PM-04_04_53 Last ObjectModification: 2012_02_02-PM-01_59_56 Home Index