---

Step * 1 1 1 of Lemma consensus-ts4-ref-map


1. [V] : Type
2. A : Id List@i
⊢ ∀s:ConsensusState. ∃n:ℕ. ∀i:ℕ. (i < n ⇐⇒ ∃a:{a:Id| (a ∈ A)} . (i ≤ Inning(s;a)))
BY
{ Auto }

1
1. [V] : Type
2. A : Id List@i
3. s : ConsensusState@i
⊢ ∃n:ℕ. ∀i:ℕ. (i < n ⇐⇒ ∃a:{a:Id| (a ∈ A)} . (i ≤ Inning(s;a)))

---

Latex:



1.  [V]  :  Type
2.  A  :  Id  List@i
\mvdash{}  \mforall{}s:ConsensusState.  \mexists{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}.  (i  <  n  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:\{a:Id|  (a  \mmember{}  A)\}  .  (i  \mleq{}  Inning(s;a)))


By

Auto

---

Home Index