---

Step * 1 1 of Lemma cs-archived-listable


1. [V] : Type
2. A : Id List@i
3. s : ConsensusState@i
4. b : {a:Id| (a ∈ A)} @i
⊢ map(λj.Estimate(s;b)(j);fpf-domain(Estimate(s;b))) ∈ V List
BY
{ (BLemma `map-wf2`  THEN Try (Complete (Auto))) }

---

Latex:

---

Latex:

1.  [V]  :  Type
2.  A  :  Id  List@i
3.  s  :  ConsensusState@i
4.  b  :  \{a:Id|  (a  \mmember{}  A)\}  @i
\mvdash{}  map(\mlambda{}j.Estimate(s;b)(j);fpf-domain(Estimate(s;b)))  \mmember{}  V  List


By

---

Latex:
(BLemma  `map-wf2`    THEN  Try  (Complete  (Auto)))

---

Home Index