---

Step * of Lemma decidable__cs-archived

∀[V:Type]
  ∀A:Id List. ∀s:ConsensusState. ∀a:{a:Id| (a ∈ A)} . ∀i:ℤ. ∀v:V.
    ((∀v,v':V.  Dec(v = v' ∈ V)) ⇒ Dec(by state s, a archived v in inning i))
BY
{ (Auto THEN Unfold `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
6. v : V@i
7. ∀v,v':V.  Dec(v = v' ∈ V)@i
⊢ Dec((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{}.  \mforall{}v:V.
        ((\mforall{}v,v':V.    Dec(v  =  v'))  {}\mRightarrow{}  Dec(by  state  s,  a  archived  v  in  inning  i))


By

(Auto  THEN  Unfold  `cs-archived`  0)

---

Home Index