Nuprl Lemma : decidable__equal_consensus-rcv
∀[V:Type]. ((∀v,w:V. Dec(v = w ∈ V)) ⇒ (∀A:Id List. ∀x,y:consensus-rcv(V;A). Dec(x = y ∈ consensus-rcv(V;A))))
Proof
Definitions occuring in Statement :
consensus-rcv: consensus-rcv(V;A),
Id: Id,
list: T List,
decidable: Dec(P),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
universe: Type,
equal: s = t ∈ T
Lemmas :
consensus-rcv_wf,
list_wf,
Id_wf,
all_wf,
decidable_wf,
equal_wf,
decidable__equal_union,
l_member_wf,
nat_wf,
decidable__equal_product,
decidable__equal_set,
decidable__equal_Id,
set_wf,
decidable__equal_nat
\mforall{}[V:Type]. ((\mforall{}v,w:V. Dec(v = w)) {}\mRightarrow{} (\mforall{}A:Id List. \mforall{}x,y:consensus-rcv(V;A). Dec(x = y)))
Date html generated:
2015_07_17-AM-11_46_44
Last ObjectModification:
2015_01_28-AM-01_29_34
Home
Index