Nuprl Definition : supercompat-pvals
supercompat-pvals(Id-lt;bsp;bsp') ==
(ballot-lt(Id-lt) (fst(bsp)) (fst(bsp')))
((fst(snd(bsp))) = (fst(snd(bsp'))))
((snd(snd(bsp))) = (snd(snd(bsp'))))
Proof not projected
Definitions occuring in Statement :
Command: Command(),
ballot-lt: ballot-lt(Id-lt),
pi1: fst(t),
pi2: snd(t),
implies: P Q,
apply: f a,
int: 
,
equal: s = t
Definitions :
apply: f a,
ballot-lt: ballot-lt(Id-lt),
implies: P Q,
int: ,
pi1: fst(t),
equal: s = t,
Command: Command(),
pi2: snd(t)
FDL editor aliases :
supercompat-pvals
supercompat-pvals(Id-lt;bsp;bsp') ==
(ballot-lt(Id-lt) (fst(bsp)) (fst(bsp')))
{}\mRightarrow{} ((fst(snd(bsp))) = (fst(snd(bsp'))))
{}\mRightarrow{} ((snd(snd(bsp))) = (snd(snd(bsp'))))
Date html generated:
2011_10_20-PM-11_42_51
Last ObjectModification:
2011_05_26-PM-03_54_21
Home
Index