---

Step * 1 of Lemma consensus-ts4-passed-stable


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

1
1. V : Type@i'
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. s : ConsensusState@i
7. y : ConsensusState@i
8. by state s, a passed inning i without archiving a value@i
9. CR[s,y]@i
⊢ by state y, a passed inning i without archiving a value

---

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{}.
    ts-stable(consensus-ts4(V;A;W);s.by  state  s,  a  passed  inning  i  without  archiving  a  value)


By

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

---

Home Index