Step * of 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))))
BY
(Auto THEN All (Unfold `consensus-rcv`)) }

1
1. [V] Type
2. ∀v,w:V.  Dec(v w ∈ V)@i
3. Id List@i
4. ({b:Id| (b ∈ A)}  × ℕ × V)@i
5. ({b:Id| (b ∈ A)}  × ℕ × V)@i
⊢ Dec(x y ∈ (V ({b:Id| (b ∈ A)}  × ℕ × V)))


Latex:


\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)))


By

(Auto  THEN  All  (Unfold  `consensus-rcv`))




Home Index