Nuprl Definition : RSC_agreement
RSC_agreement(Cmd;es) ==
e1,e2:E. v1,v2:
Cmd.
(v1 
RSC_Decided(Cmd)(e1) 
v2 RSC_Decided(Cmd)(e2) ((fst(v1)) = (fst(v2))) ((snd(v1)) = (snd(v2))))
hello world
Definitions occuring in Statement :
RSC_Decided: RSC_Decided(Cmd),
classrel: v X(e),
es-E: E,
pi1: fst(t),
pi2: snd(t),
all: x:A. B[x],
implies: P Q,
product: x:A B[x],
int: ,
equal: s = t
FDL editor aliases :
RSC_agreement
RSC\_agreement(Cmd;es) ==
\mforall{}e1,e2:E. \mforall{}v1,v2:\mBbbZ{} \mtimes{} Cmd.
(v1 \mmember{} RSC\_Decided(Cmd)(e1)
{}\mRightarrow{} v2 \mmember{} RSC\_Decided(Cmd)(e2)
{}\mRightarrow{} ((fst(v1)) = (fst(v2)))
{}\mRightarrow{} ((snd(v1)) = (snd(v2))))
Date html generated:
2012_02_20-PM-04_01_46
Last ObjectModification:
2012_02_02-PM-01_59_26
Home
Index