---

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


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)))
BY
{ ((InstConcl [⌈0⌉]⋅ THEN Auto) THEN D -1 THEN D -2 THEN D 2 THEN All Reduce THEN Auto) }

---

Latex:



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


By

((InstConcl  [\mkleeneopen{}0\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  D  -1  THEN  D  -2  THEN  D  2  THEN  All  Reduce  THEN  Auto)

---

Home Index