---

Step * of Lemma decidable__cs-not-completed

∀[V:Type]. ∀A:Id List. ∀s:ConsensusState. ∀a:{a:Id| (a ∈ A)} . ∀i:ℤ.  Dec(in state s, a has not completed inning i)
BY
{ (Unfold `cs-not-completed` 0 THEN RepeatFor 2 (Auto)) }

---

Latex:


\mforall{}[V:Type]
    \mforall{}A:Id  List.  \mforall{}s:ConsensusState.  \mforall{}a:\{a:Id|  (a  \mmember{}  A)\}  .  \mforall{}i:\mBbbZ{}.
        Dec(in  state  s,  a  has  not  completed  inning  i)


By

(Unfold  `cs-not-completed`  0  THEN  RepeatFor  2  (Auto))

---

Home Index