---

Step * 1 1 1 1 2 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
{ (InstLemma `map_wf` [⌈{a:Id| (a ∈ A)} ⌉;⌈ℤ⌉;⌈λa.Inning(s;a)⌉;⌈A⌉]⋅ 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
⊢ ∃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)
\mvdash{}  \mexists{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}.  (i  <  n  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:\{a:Id|  (a  \mmember{}  A)\}  .  (i  \mleq{}  Inning(s;a)))


By

(InstLemma  `map\_wf`  [\mkleeneopen{}\{a:Id|  (a  \mmember{}  A)\}  \mkleeneclose{};\mkleeneopen{}\mBbbZ{}\mkleeneclose{};\mkleeneopen{}\mlambda{}a.Inning(s;a)\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index