---

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


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)))
BY
{ (Decide ↑null(A) THENA Auto) }

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

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

---

Latex:



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


By

(Decide  \muparrow{}null(A)  THENA  Auto)

---

Home Index