Nuprl Definition : pv11_p1_consistent-pvalues
pv11_p1_consistent-pvalues(Cmd;x;y) ==
((fst(x)) = (fst(y)) ∈ pv11_p1_Ballot_Num())
⇒ ((fst(snd(x))) = (fst(snd(y))) ∈ ℤ)
⇒ (x = y ∈ (pv11_p1_Ballot_Num() × ℤ × Cmd))
Definitions occuring in Statement :
pv11_p1_Ballot_Num: pv11_p1_Ballot_Num(),
pi1: fst(t),
pi2: snd(t),
implies: P ⇒ Q,
product: x:A × B[x],
int: ℤ,
equal: s = t ∈ T
FDL editor aliases :
pv11_p1_consistent-pvalues
Latex:
pv11\_p1\_consistent-pvalues(Cmd;x;y) ==
((fst(x)) = (fst(y))) {}\mRightarrow{} ((fst(snd(x))) = (fst(snd(y)))) {}\mRightarrow{} (x = y)
Date html generated:
2016_05_17-PM-04_15_17
Last ObjectModification:
2013_12_18-PM-06_19_13
Theory : paxos!synod
Home
Index