---

Step * of Lemma consensus-ts5-archive-invariant

∀[V:Type]
  ((∀v1,v2:V.  Dec(v1 = v2 ∈ V))
  ⇒ (∃v,v':V. (¬(v = v' ∈ V)))
  ⇒ (∀A:Id List. ∀W:{a:Id| (a ∈ A)}  List List. ∀x:ts-reachable(consensus-ts5(V;A;W)). ∀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
{ (RepeatFor 5 ((D 0 THENA Auto))
   THEN (BLemma `ts-reachable-induction` 
         THENA (Try (Complete (Auto))
                THEN Try (((MemCD THENA Auto)
                           THEN D -1
                           THEN RepUR ``ts-type consensus-ts5`` -2
                           THEN D -2
                           THEN Reduce 0
                           THEN Auto))
                )
         )
   ) }

1
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)))))

2
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
⊢ ∀v:V. ∀b:{a:Id| (a ∈ A)} . ∀i:ℤ.
    (state fst(ts-init(consensus-ts5(V;A;W))) may consider v in inning i) supposing 
       ((Estimate(fst(ts-init(consensus-ts5(V;A;W)));b)(i) = v ∈ V) and 
       (↑i ∈ dom(Estimate(fst(ts-init(consensus-ts5(V;A;W)));b))))

3
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,y:ts-reachable(consensus-ts5(V;A;W)).
    ((∀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)))))
    ⇒ (x ts-rel(consensus-ts5(V;A;W)) y)
    ⇒ (∀v:V. ∀b:{a:Id| (a ∈ A)} . ∀i:ℤ.
          (state fst(y) may consider v in inning i) supposing 
             ((Estimate(fst(y);b)(i) = v ∈ V) and 
             (↑i ∈ dom(Estimate(fst(y);b))))))

---

Latex:


\mforall{}[V:Type]
    ((\mforall{}v1,v2:V.    Dec(v1  =  v2))
    {}\mRightarrow{}  (\mexists{}v,v':V.  (\mneg{}(v  =  v')))
    {}\mRightarrow{}  (\mforall{}A:Id  List.  \mforall{}W:\{a:Id|  (a  \mmember{}  A)\}    List  List.  \mforall{}x:ts-reachable(consensus-ts5(V;A;W)).  \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

(RepeatFor  5  ((D  0  THENA  Auto))
  THEN  (BLemma  `ts-reachable-induction` 
              THENA  (Try  (Complete  (Auto))
                            THEN  Try  (((MemCD  THENA  Auto)
                                                  THEN  D  -1
                                                  THEN  RepUR  ``ts-type  consensus-ts5``  -2
                                                  THEN  D  -2
                                                  THEN  Reduce  0
                                                  THEN  Auto))
                            )
              )
  )

---

Home Index