---

Step * 1 of Lemma consensus-ts4-archived-invariant


∀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))))))
BY
{ (RepeatFor 4 ((D 0 THENA Auto))
   THEN BLemma `ts-reachable-induction`
   THEN Auto
   THEN All
    (RepUR ``ts-type ts-init ts-rel consensus-ts4 ts-reachable``)⋅
   THEN Auto
   THEN Try (OnMaybeHyp 7 (\h. (RepUR ``cs-archived cs-estimate`` h THEN D h THEN Complete (Auto))))
   THEN (RepUR ``consensus-state4`` 0 THEN Auto)
   THEN DVar `x'
   THEN DVar `y') }

1
1. V : Type@i'
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. A : Id List@i
4. W : {a:Id| (a ∈ A)}  List List@i
5. x : ConsensusState@i
6. (λa.<-1, ⊗>) ((λx,y. CR[x,y])^*) x@i
7. y : ConsensusState@i
8. (λa.<-1, ⊗>) ((λx,y. CR[x,y])^*) y@i
9. ∀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))))@i
10. CR[x,y]@i
11. i : ℤ@i
12. v : V@i
13. a : {a:Id| (a ∈ A)} @i
14. by state y, a archived v in inning i@i
15. j : ℕi@i
16. v' : V@i
17. in state y, inning j could commit v' @i
⊢ v' = v ∈ V

---

Latex:



\mforall{}V:Type
    ((\mforall{}v1,v2:V.    Dec(v1  =  v2))
    {}\mRightarrow{}  (\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)\}  .
                (by  state  x,  a  archived  v  in  inning  i
                {}\mRightarrow{}  (\mforall{}j:\mBbbN{}i.  \mforall{}v':V.    (in  state  x,  inning  j  could  commit  v'    {}\mRightarrow{}  (v'  =  v))))))


By

(RepeatFor  4  ((D  0  THENA  Auto))
  THEN  BLemma  `ts-reachable-induction`
  THEN  Auto
  THEN  All
    (RepUR  ``ts-type  ts-init  ts-rel  consensus-ts4  ts-reachable``)\mcdot{}
  THEN  Auto
  THEN  Try  (OnMaybeHyp  7  (\mbackslash{}h.  (RepUR  ``cs-archived  cs-estimate``  h  THEN  D  h  THEN  Complete  (Auto))))
  THEN  (RepUR  ``consensus-state4``  0  THEN  Auto)
  THEN  DVar  `x'
  THEN  DVar  `y')

---

Home Index