---

Step * 1 1 1 1 2 1 1 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
6. 0 < ||map(λa.Inning(s;a);A)||
7. imax-list(map(λa.Inning(s;a);A)) ∈ ℤ
8. n : ℤ@i
9. imax-list(map(λa.Inning(s;a);A)) = n ∈ ℤ@i
⊢ (∀[a:ℤ]. uiff(n ≤ a;(∀b∈map(λa.Inning(s;a);A).b ≤ a)) supposing 0 < ||map(λa.Inning(s;a);A)||)
⇒ (∀a:ℤ. a ≤ n ⇐⇒ (∃b∈map(λa.Inning(s;a);A). a ≤ b) supposing 0 < ||map(λa.Inning(s;a);A)||)
⇒ (∃n:ℕ. ∀i:ℕ. (i < n ⇐⇒ ∃a:{a:Id| (a ∈ A)} . (i ≤ Inning(s;a))))
BY
{ (RWO "l_all_iff l_exists_iff" 0 THENA 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)||
7. imax-list(map(λa.Inning(s;a);A)) ∈ ℤ
8. n : ℤ@i
9. imax-list(map(λa.Inning(s;a);A)) = n ∈ ℤ@i
⊢ (∀[a:ℤ]. uiff(n ≤ a;∀b:ℤ. ((b ∈ map(λa.Inning(s;a);A)) ⇒ (b ≤ a))) supposing 0 < ||map(λa.Inning(s;a);A)||)
⇒ (∀a:ℤ. a ≤ n ⇐⇒ ∃b:ℤ. ((b ∈ map(λa.Inning(s;a);A)) ∧ (a ≤ b)) supposing 0 < ||map(λa.Inning(s;a);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
4.  \mneg{}\muparrow{}null(A)
5.  map(\mlambda{}a.Inning(s;a);A)  \mmember{}  \mBbbZ{}  List
6.  0  <  ||map(\mlambda{}a.Inning(s;a);A)||
7.  imax-list(map(\mlambda{}a.Inning(s;a);A))  \mmember{}  \mBbbZ{}
8.  n  :  \mBbbZ{}@i
9.  imax-list(map(\mlambda{}a.Inning(s;a);A))  =  n@i
\mvdash{}  (\mforall{}[a:\mBbbZ{}].  uiff(n  \mleq{}  a;(\mforall{}b\mmember{}map(\mlambda{}a.Inning(s;a);A).b  \mleq{}  a))  supposing  0  <  ||map(\mlambda{}a.Inning(s;a);A)||)
{}\mRightarrow{}  (\mforall{}a:\mBbbZ{}.  a  \mleq{}  n  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}b\mmember{}map(\mlambda{}a.Inning(s;a);A).  a  \mleq{}  b)  supposing  0  <  ||map(\mlambda{}a.Inning(s;a);A)||)
{}\mRightarrow{}  (\mexists{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}.  (i  <  n  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:\{a:Id|  (a  \mmember{}  A)\}  .  (i  \mleq{}  Inning(s;a))))


By

(RWO  "l\_all\_iff  l\_exists\_iff"  0  THENA  Auto)

---

Home Index