---

Step * 1 1 1 1 2 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)||
⊢ ∃n:ℕ. ∀i:ℕ. (i < n ⇐⇒ ∃a:{a:Id| (a ∈ A)} . (i ≤ Inning(s;a)))
BY
{ ((InstLemma `imax-list_wf` [⌜map(λa.Inning(s;a);A)⌝]⋅ THENA Auto)
   THEN (InstLemma `imax-list-lb` [⌜map(λa.Inning(s;a);A)⌝]⋅ THENA Auto)
   THEN (InstLemma `imax-list-ub` [⌜map(λa.Inning(s;a);A)⌝]⋅ THENA Auto)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN (GenConcl ⌜imax-list(map(λa.Inning(s;a);A)) = n ∈ ℤ⌝⋅ 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∈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))))

---

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
6.  0  <  ||map(\mlambda{}a.Inning(s;a);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

---

Latex:
((InstLemma  `imax-list\_wf`  [\mkleeneopen{}map(\mlambda{}a.Inning(s;a);A)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `imax-list-lb`  [\mkleeneopen{}map(\mlambda{}a.Inning(s;a);A)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `imax-list-ub`  [\mkleeneopen{}map(\mlambda{}a.Inning(s;a);A)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  (GenConcl  \mkleeneopen{}imax-list(map(\mlambda{}a.Inning(s;a);A))  =  n\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index