---

Step * 3 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,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))))))
BY
{ (RepeatFor 2 (((D 0 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
6. x1 : ConsensusState@i
7. x2 : Knowledge(ConsensusState)@i
8. \\%3 : ts-init(consensus-ts5(V;A;W)) (ts-rel(consensus-ts5(V;A;W))^*) <x1, x2>@i
9. y1 : ConsensusState@i
10. y2 : Knowledge(ConsensusState)@i
11. \\%5 : ts-init(consensus-ts5(V;A;W)) (ts-rel(consensus-ts5(V;A;W))^*) <y1, y2>@i
12. ∀v:V. ∀b:{a:Id| (a ∈ A)} . ∀i:ℤ.
      (state x1 may consider v in inning i) supposing ((Estimate(x1;b)(i) = v ∈ V) and (↑i ∈ dom(Estimate(x1;b))))@i
13. <x1, x2> ts-rel(consensus-ts5(V;A;W)) <y1, y2>@i
14. v : V@i
15. b : {a:Id| (a ∈ A)} @i
16. i : ℤ@i
17. ↑i ∈ dom(Estimate(y1;b))
18. Estimate(y1;b)(i) = v ∈ V
⊢ state y1 may consider v in inning i

---

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,y: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)))))
        {}\mRightarrow{}  (x  ts-rel(consensus-ts5(V;A;W))  y)
        {}\mRightarrow{}  (\mforall{}v:V.  \mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  \mforall{}i:\mBbbZ{}.
                    (state  fst(y)  may  consider  v  in  inning  i)  supposing 
                          ((Estimate(fst(y);b)(i)  =  v)  and 
                          (\muparrow{}i  \mmember{}  dom(Estimate(fst(y);b))))))


By

(RepeatFor  2  (((D  0  THENA  Auto)
                              THEN  D  -1
                              THEN  RepUR  ``ts-type  consensus-ts5``  -2
                              THEN  D  -2
                              THEN  Reduce  0))
  THEN  Auto
  )

---

Home Index