---

Step * 1 2 of Lemma cs-archived-listable


1. [V] : Type
2. A : Id List@i
3. s : ConsensusState@i
4. ∀b:{a:Id| (a ∈ A)} . (map(λj.Estimate(s;b)(j);fpf-domain(Estimate(s;b))) ∈ V List)
⊢ ∃L:V List
   ∀b:{a:Id| (a ∈ A)} . ∀v:V. ∀j:ℤ.  ((v ∈ L)) supposing ((Estimate(s;b)(j) = v ∈ V) and (↑j ∈ dom(Estimate(s;b))))
BY
{ (Assert map(λb.map(λj.Estimate(s;b)(j);fpf-domain(Estimate(s;b)));A) ∈ V List List BY
         (Using [`A',⌜{a:Id| (a ∈ A)} ⌝] (BLemma `map_wf` )⋅ THEN Auto)) }

1
1. [V] : Type
2. A : Id List@i
3. s : ConsensusState@i
4. ∀b:{a:Id| (a ∈ A)} . (map(λj.Estimate(s;b)(j);fpf-domain(Estimate(s;b))) ∈ V List)
5. map(λb.map(λj.Estimate(s;b)(j);fpf-domain(Estimate(s;b)));A) ∈ V List List
⊢ ∃L:V List
   ∀b:{a:Id| (a ∈ A)} . ∀v:V. ∀j:ℤ.  ((v ∈ L)) supposing ((Estimate(s;b)(j) = v ∈ V) and (↑j ∈ dom(Estimate(s;b))))

---

Latex:

---

Latex:

1.  [V]  :  Type
2.  A  :  Id  List@i
3.  s  :  ConsensusState@i
4.  \mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  (map(\mlambda{}j.Estimate(s;b)(j);fpf-domain(Estimate(s;b)))  \mmember{}  V  List)
\mvdash{}  \mexists{}L:V  List
      \mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  \mforall{}v:V.  \mforall{}j:\mBbbZ{}.
          ((v  \mmember{}  L))  supposing  ((Estimate(s;b)(j)  =  v)  and  (\muparrow{}j  \mmember{}  dom(Estimate(s;b))))


By

---

Latex:
(Assert  map(\mlambda{}b.map(\mlambda{}j.Estimate(s;b)(j);fpf-domain(Estimate(s;b)));A)  \mmember{}  V  List  List  BY
              (Using  [`A',\mkleeneopen{}\{a:Id|  (a  \mmember{}  A)\}  \mkleeneclose{}]  (BLemma  `map\_wf`  )\mcdot{}  THEN  Auto))

---

Home Index