---

Step * 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)))
⊢ (i < Inning(s;a) ∧ (¬(i ∈ fpf-domain(Estimate(s;a)))))
∨ ((Inning(s;a) ≤ i) ∧ (¬(i ∈ fpf-domain(Estimate(s;a)))))
∨ (∃v:V. ((i ∈ fpf-domain(Estimate(s;a))) ∧ (Estimate(s;a)(i) = v ∈ V)))
BY
{ (Sel 3 (D 0) THEN Auto) }

1
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))

---

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{}  (i  <  Inning(s;a)  \mwedge{}  (\mneg{}(i  \mmember{}  fpf-domain(Estimate(s;a)))))
\mvee{}  ((Inning(s;a)  \mleq{}  i)  \mwedge{}  (\mneg{}(i  \mmember{}  fpf-domain(Estimate(s;a)))))
\mvee{}  (\mexists{}v:V.  ((i  \mmember{}  fpf-domain(Estimate(s;a)))  \mwedge{}  (Estimate(s;a)(i)  =  v)))


By

(Sel  3  (D  0)  THEN  Auto)

---

Home Index