Nuprl Definition : compat-pvals
compat-pvals(bsp;bsp') ==
((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_Num: Ballot_Num(),
pi1: fst(t),
pi2: snd(t),
implies: P Q,
int: 
,
equal: s = t
Definitions :
implies: P Q,
int: ,
pi1: fst(t),
equal: s = t,
pi2: snd(t)
FDL editor aliases :
compat-pvals
compat-pvals(bsp;bsp') ==
((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_24
Last ObjectModification:
2011_05_23-PM-03_39_17
Home
Index