---

Step * of Lemma consensus-ts4-inning-committed-stable

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

1
1. [V] : Type
2. A : Id List@i
3. W : {a:Id| (a ∈ A)}  List List@i
4. v : V@i
5. i : ℤ@i
6. s : ConsensusState@i
7. y : ConsensusState@i
8. ws : {a:Id| (a ∈ A)}  List@i
9. (ws ∈ W)@i
10. ∀a:{a:Id| (a ∈ A)} . ((a ∈ ws) ⇒ by state s, a archived v in inning i)@i
11. CR[s,y]@i
12. a : {a:Id| (a ∈ A)} @i
13. (a ∈ ws)@i
14. by state s, a archived v in inning 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{}v:V.  \mforall{}i:\mBbbZ{}.
        ts-stable(consensus-ts4(V;A;W);s.in  state  s,  inning  i  has  committed  v)


By

(Auto
  THEN  (D  0  THENA  Auto)
  THEN  All  (RepUR  ``consensus-ts4  ts-type  ts-rel``)
  THEN  (UnivCD  THENA  Auto)
  THEN  RepeatFor  4  (ParallelOp  -2)
  THEN  ParallelLast)

---

Home Index