---

Step * 1 1 1 of Lemma consensus-state4-cases


1. [V] : Type
2. A : Id List@i
3. s : ConsensusState@i
4. a : {a:Id| (a ∈ A)} @i
5. i : ℤ@i
6. (i ∈ fpf-domain(Estimate(s;a)))
⊢ ∃v:V. ((i ∈ fpf-domain(Estimate(s;a))) ∧ (Estimate(s;a)(i) = v ∈ V))
BY
{ (InstConcl [⌈Estimate(s;a)(i)⌉]⋅ THEN Auto) }

---

Latex:



1.  [V]  :  Type
2.  A  :  Id  List@i
3.  s  :  ConsensusState@i
4.  a  :  \{a:Id|  (a  \mmember{}  A)\}  @i
5.  i  :  \mBbbZ{}@i
6.  (i  \mmember{}  fpf-domain(Estimate(s;a)))
\mvdash{}  \mexists{}v:V.  ((i  \mmember{}  fpf-domain(Estimate(s;a)))  \mwedge{}  (Estimate(s;a)(i)  =  v))


By

(InstConcl  [\mkleeneopen{}Estimate(s;a)(i)\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index