---

Step * of Lemma consensus-ts4-archived-invariant

∀[V:Type]
  ∀[A:Id List]. ∀[W:{a:Id| (a ∈ A)}  List List]. ∀[x:ts-reachable(consensus-ts4(V;A;W))]. ∀[i:ℤ]. ∀[v:V]. ∀[a:{a:Id| 
                                                                                                              (a ∈ A)} ]\000C.
    ∀[j:ℕi]. ∀[v':V].  v' = v ∈ V supposing in state x, inning j could commit v'  
    supposing by state x, a archived v in inning i 
  supposing ∀v1,v2:V.  Dec(v1 = v2 ∈ V)
BY
{ RemoveUniform Auto (Auto THEN (All (RepUR ``ts-reachable consensus-ts4 ts-type``) THEN Auto))⋅ }

1
∀V:Type
  ((∀v1,v2:V.  Dec(v1 = v2 ∈ V))
  ⇒ (∀A:Id List. ∀W:{a:Id| (a ∈ A)}  List List. ∀x:ts-reachable(consensus-ts4(V;A;W)). ∀i:ℤ. ∀v:V. ∀a:{a:Id| (a ∈ A)} .
        (by state x, a archived v in inning i
        ⇒ (∀j:ℕi. ∀v':V.  (in state x, inning j could commit v'  ⇒ (v' = v ∈ V))))))

---

Latex:


\mforall{}[V:Type]
    \mforall{}[A:Id  List].  \mforall{}[W:\{a:Id|  (a  \mmember{}  A)\}    List  List].  \mforall{}[x:ts-reachable(consensus-ts4(V;A;W))].  \mforall{}[i:\mBbbZ{}].
    \mforall{}[v:V].  \mforall{}[a:\{a:Id|  (a  \mmember{}  A)\}  ].
        \mforall{}[j:\mBbbN{}i].  \mforall{}[v':V].    v'  =  v  supposing  in  state  x,  inning  j  could  commit  v'   
        supposing  by  state  x,  a  archived  v  in  inning  i 
    supposing  \mforall{}v1,v2:V.    Dec(v1  =  v2)


By

RemoveUniform  Auto  (Auto  THEN  (All  (RepUR  ``ts-reachable  consensus-ts4  ts-type``)  THEN  Auto))\mcdot{}

---

Home Index