---

Step * 1 of Lemma consensus-ts5-archive-invariant


1. [V] : Type
2. ∀v1,v2:V.  Dec(v1 = v2 ∈ V)@i
3. ∃v,v':V. (¬(v = v' ∈ V))@i
4. A : Id List@i
5. W : {a:Id| (a ∈ A)}  List List@i
⊢ ∀x:ts-reachable(consensus-ts5(V;A;W))
    SqStable(∀v:V. ∀b:{a:Id| (a ∈ A)} . ∀i:ℤ.
               (state fst(x) may consider v in inning i) supposing 
                  ((Estimate(fst(x);b)(i) = v ∈ V) and 
                  (↑i ∈ dom(Estimate(fst(x);b)))))
BY
{ ((D 0 THENA Auto)
   THEN D -1
   THEN RepUR ``ts-type consensus-ts5`` -2
   THEN D -2
   THEN Reduce 0
   THEN RepeatFor 2 (Auto)
   THEN BLemma `sq_stable_from_decidable`
   THEN Auto) }

---

Latex:



1.  [V]  :  Type
2.  \mforall{}v1,v2:V.    Dec(v1  =  v2)@i
3.  \mexists{}v,v':V.  (\mneg{}(v  =  v'))@i
4.  A  :  Id  List@i
5.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List@i
\mvdash{}  \mforall{}x:ts-reachable(consensus-ts5(V;A;W))
        SqStable(\mforall{}v:V.  \mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  \mforall{}i:\mBbbZ{}.
                              (state  fst(x)  may  consider  v  in  inning  i)  supposing 
                                    ((Estimate(fst(x);b)(i)  =  v)  and 
                                    (\muparrow{}i  \mmember{}  dom(Estimate(fst(x);b)))))


By

((D  0  THENA  Auto)
  THEN  D  -1
  THEN  RepUR  ``ts-type  consensus-ts5``  -2
  THEN  D  -2
  THEN  Reduce  0
  THEN  RepeatFor  2  (Auto)
  THEN  BLemma  `sq\_stable\_from\_decidable`
  THEN  Auto)

---

Home Index