---

Step * of Lemma cs-inning-committed-committable

∀[V:Type]
  ∀A:Id List. ∀W:{a:Id| (a ∈ A)}  List List. ∀s:ConsensusState. ∀i:ℤ. ∀v:V.
    (in state s, inning i has committed v ⇒ in state s, inning i could commit v )
BY
{ (Auto THEN UnfoldTopAb (-1) THEN UnfoldTopAb 0 THEN RepeatFor 4 (ParallelLast) THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  UnfoldTopAb  (-1)  THEN  UnfoldTopAb  0  THEN  RepeatFor  4  (ParallelLast)  THEN  Auto)

---

Home Index