---

Step * of Lemma consensus-state4-cases

∀[V:Type]
  ∀A:Id List. ∀s:ConsensusState. ∀a:{a:Id| (a ∈ A)} . ∀i:ℤ.
    (by state s, a passed inning i without archiving a value
    ∨ in state s, a has not completed inning i
    ∨ (∃v:V. by state s, a archived v in inning i))
BY
{ (Auto THEN Unfolds ``cs-passed cs-not-completed cs-archived`` 0) }

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

---

Latex:


\mforall{}[V:Type]
    \mforall{}A:Id  List.  \mforall{}s:ConsensusState.  \mforall{}a:\{a:Id|  (a  \mmember{}  A)\}  .  \mforall{}i:\mBbbZ{}.
        (by  state  s,  a  passed  inning  i  without  archiving  a  value
        \mvee{}  in  state  s,  a  has  not  completed  inning  i
        \mvee{}  (\mexists{}v:V.  by  state  s,  a  archived  v  in  inning  i))


By

(Auto  THEN  Unfolds  ``cs-passed  cs-not-completed  cs-archived``  0)

---

Home Index