---

Step * of Lemma cs-archived-listable

∀[V:Type]
  ∀A:Id List. ∀s:ConsensusState.
    ∃L:V List
     ∀b:{a:Id| (a ∈ A)} . ∀v:V. ∀j:ℤ.  ((v ∈ L)) supposing ((Estimate(s;b)(j) = v ∈ V) and (↑j ∈ dom(Estimate(s;b))))
BY
{ Auto }

1
1. [V] : Type
2. A : Id List@i
3. s : ConsensusState@i
⊢ ∃L:V List
   ∀b:{a:Id| (a ∈ A)} . ∀v:V. ∀j:ℤ.  ((v ∈ L)) supposing ((Estimate(s;b)(j) = v ∈ V) and (↑j ∈ dom(Estimate(s;b))))

---

Latex:


\mforall{}[V:Type]
    \mforall{}A:Id  List.  \mforall{}s:ConsensusState.
        \mexists{}L:V  List
          \mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  \mforall{}v:V.  \mforall{}j:\mBbbZ{}.
              ((v  \mmember{}  L))  supposing  ((Estimate(s;b)(j)  =  v)  and  (\muparrow{}j  \mmember{}  dom(Estimate(s;b))))


By

Auto

---

Home Index