---

Step * of Lemma consensus-ts4-archived-stable

∀[V:Type]
  ∀A:Id List. ∀W:{a:Id| (a ∈ A)}  List List. ∀a:{a:Id| (a ∈ A)} . ∀i:ℤ. ∀v:V.
    ts-stable(consensus-ts4(V;A;W);s.by state s, a archived v in inning i)
BY
{ (Auto THEN (D 0 THENA Auto) THEN All (RepUR ``consensus-ts4 ts-type ts-rel``) THEN (UnivCD THENA Auto)) }

1
1. [V] : Type
2. A : Id List@i
3. W : {a:Id| (a ∈ A)}  List List@i
4. a : {a:Id| (a ∈ A)} @i
5. i : ℤ@i
6. v : V@i
7. s : ConsensusState@i
8. y : ConsensusState@i
9. by state s, a archived v in inning i@i
10. CR[s,y]@i
⊢ by state y, a archived v in inning i

---

Latex:


\mforall{}[V:Type]
    \mforall{}A:Id  List.  \mforall{}W:\{a:Id|  (a  \mmember{}  A)\}    List  List.  \mforall{}a:\{a:Id|  (a  \mmember{}  A)\}  .  \mforall{}i:\mBbbZ{}.  \mforall{}v:V.
        ts-stable(consensus-ts4(V;A;W);s.by  state  s,  a  archived  v  in  inning  i)


By

(Auto
  THEN  (D  0  THENA  Auto)
  THEN  All  (RepUR  ``consensus-ts4  ts-type  ts-rel``)
  THEN  (UnivCD  THENA  Auto))

---

Home Index