---

Step * of Lemma decidable__cs-inning-committed

∀[V:Type]
  ((∀v,v':V.  Dec(v = v' ∈ V))
  ⇒ (∀A:Id List. ∀W:{a:Id| (a ∈ A)}  List List. ∀s:ConsensusState. ∀i:ℤ. ∀v:V.
        Dec(in state s, inning i has committed v)))
BY
{ (Auto THEN Unfold `cs-inning-committed` 0 THEN RWO "l_exists_iff<" 0 THEN Auto) }

---

Latex:


\mforall{}[V:Type]
    ((\mforall{}v,v':V.    Dec(v  =  v'))
    {}\mRightarrow{}  (\mforall{}A:Id  List.  \mforall{}W:\{a:Id|  (a  \mmember{}  A)\}    List  List.  \mforall{}s:ConsensusState.  \mforall{}i:\mBbbZ{}.  \mforall{}v:V.
                Dec(in  state  s,  inning  i  has  committed  v)))


By

(Auto  THEN  Unfold  `cs-inning-committed`  0  THEN  RWO  "l\_exists\_iff<"  0  THEN  Auto)

---

Home Index