Nuprl Lemma : pv11_p1_consistent-pvalues_wf
∀[Cmd:Type]. ∀[x,y:pv11_p1_Ballot_Num() × ℤ × Cmd].  (pv11_p1_consistent-pvalues(Cmd;x;y) ∈ ℙ)
Proof
Definitions occuring in Statement : 
pv11_p1_consistent-pvalues: pv11_p1_consistent-pvalues(Cmd;x;y)
, 
pv11_p1_Ballot_Num: pv11_p1_Ballot_Num()
, 
uall: ∀[x:A]. B[x]
, 
prop: ℙ
, 
member: t ∈ T
, 
product: x:A × B[x]
, 
int: ℤ
, 
universe: Type
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
pv11_p1_consistent-pvalues: pv11_p1_consistent-pvalues(Cmd;x;y)
, 
implies: P 
⇒ Q
, 
prop: ℙ
, 
pi1: fst(t)
, 
pi2: snd(t)
Latex:
\mforall{}[Cmd:Type].  \mforall{}[x,y:pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd].    (pv11\_p1\_consistent-pvalues(Cmd;x;y)  \mmember{}  \mBbbP{})
Date html generated:
2016_05_17-PM-04_15_21
Last ObjectModification:
2015_12_29-PM-11_13_33
Theory : paxos!synod
Home
Index