---

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


1. [V] : Type
2. A : Id List@i
3. s : ConsensusState@i
4. ¬↑null(A)
5. map(λa.Inning(s;a);A) ∈ ℤ List
⊢ ∃n:ℕ. ∀i:ℕ. (i < n ⇐⇒ ∃a:{a:Id| (a ∈ A)} . (i ≤ Inning(s;a)))
BY
{ (Assert 0 < ||map(λa.Inning(s;a);A)|| BY
         (DVar `A' THEN All Reduce THEN Try (RWO "length-map" 0) THEN Auto')) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(Assert  0  <  ||map(\mlambda{}a.Inning(s;a);A)||  BY
              (DVar  `A'  THEN  All  Reduce  THEN  Try  (RWO  "length-map"  0)  THEN  Auto'))

---

Home Index