---

Step * 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
⊢ (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
{ (Decide (i ∈ fpf-domain(Estimate(s;a))) THENA 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)))
⊢ (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)))

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

---

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
\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

(Decide  (i  \mmember{}  fpf-domain(Estimate(s;a)))  THENA  Auto)

---

Home Index