---

Step * 1 2 1 2 1 1 1 1 of Lemma three-cs-archive-condition


1. V : Type@i'
2. A : Id List@i
3. t : ℕ+@i
4. f : (V List) ─→ V@i
5. s : {a:Id| (a ∈ A)}  ─→ (consensus-rcv(V;A) List)@i
6. ts-init(three-consensus-ts(V;A;t;f)) (ts-rel(three-consensus-ts(V;A;t;f))^*) s@i
7. y : {a:Id| (a ∈ A)}  ─→ (consensus-rcv(V;A) List)@i
8. ∀v:V. ∀a:{a:Id| (a ∈ A)} . ∀n:ℕ+. ∀L:consensus-rcv(V;A) List.
     (L ≤ s a
     ⇒ archive-condition(V;A;t;f;n;v;L)
     ⇒ (∃as:{a:Id| (a ∈ A)}  List
          (no_repeats({a:Id| (a ∈ A)} ;as)
          ∧ (||as|| = ((2 * t) + 1) ∈ ℤ)
          ∧ (∃vs:V List
              ((||vs|| = ||as|| ∈ ℤ)
              ∧ (v = (f vs) ∈ V)
              ∧ (∀i:ℕ||as||
                   ∃L:consensus-rcv(V;A) List. (L ≤ s as[i] ∧ archive-condition(V;A;t;f;n - 1;vs[i];L))))))))@i
9. a1 : {a:Id| (a ∈ A)} @i
10. y2 : {b:Id| (b ∈ A)} @i
11. y4 : ℕ@i
12. y5 : V@i
13. ∀b:{a:Id| (a ∈ A)} . ∀i:ℕ. ∀v:V.
      ((Vote[y2;y4;y5] = Vote[b;i;v] ∈ consensus-rcv(V;A))
      ⇒ ((∃L:consensus-rcv(V;A) List. (L ≤ s b ∧ archive-condition(V;A;t;f;i;v;L))) ∧ (¬(Vote[y2;y4;y5] ∈ s a1))))@i
14. ∀b:{a:Id| (a ∈ A)} . ((¬(b = a1 ∈ Id)) ⇒ ((y b) = (s b) ∈ (consensus-rcv(V;A) List)))@i
15. (y a1) = ((s a1) @ [Vote[y2;y4;y5]]) ∈ (consensus-rcv(V;A) List)@i
16. v : V@i
17. n : ℕ+@i
18. (s a1) = [] ∈ (consensus-rcv(V;A) List)
19. y4 = n ∈ ℤ
20. v = y5 ∈ V
21. (∃as:{a:Id| (a ∈ A)}  List
      (no_repeats({a:Id| (a ∈ A)} ;as)
      ∧ (||as|| = ((2 * t) + 1) ∈ ℤ)
      ∧ (∃vs:V List
          ((||vs|| = ||as|| ∈ ℤ)
          ∧ (v = (f vs) ∈ V)
          ∧ (∀i:ℕ||as||. ∃L:consensus-rcv(V;A) List. (L ≤ s as[i] ∧ archive-condition(V;A;t;f;n - 1;vs[i];L)))))))
⇒ (∃as:{a:Id| (a ∈ A)}  List
     (no_repeats({a:Id| (a ∈ A)} ;as)
     ∧ (||as|| = ((2 * t) + 1) ∈ ℤ)
     ∧ (∃vs:V List
         ((||vs|| = ||as|| ∈ ℤ)
         ∧ (v = (f vs) ∈ V)
         ∧ (∀i:ℕ||as||. ∃L:consensus-rcv(V;A) List. (L ≤ y as[i] ∧ archive-condition(V;A;t;f;n - 1;vs[i];L)))))))
⊢ ∃as:{a:Id| (a ∈ A)}  List
   (no_repeats({a:Id| (a ∈ A)} ;as)
   ∧ (||as|| = ((2 * t) + 1) ∈ ℤ)
   ∧ (∃vs:V List
       ((||vs|| = ||as|| ∈ ℤ)
       ∧ (y5 = (f vs) ∈ V)
       ∧ (∀i:ℕ||as||. ∃L:consensus-rcv(V;A) List. (L ≤ s as[i] ∧ archive-condition(V;A;t;f;y4 - 1;vs[i];L))))))
BY
{ (((InstHyp [⌈y2⌉;⌈y4⌉;⌈y5⌉] (-9)⋅ THENM (D -1 THEN Thin (-1) THEN RepeatFor 2 (D -1))) THENA Auto)
   THEN FHyp 8 [-1;-2]
   THEN Auto) }

---

Latex:



1.  V  :  Type@i'
2.  A  :  Id  List@i
3.  t  :  \mBbbN{}\msupplus{}@i
4.  f  :  (V  List)  {}\mrightarrow{}  V@i
5.  s  :  \{a:Id|  (a  \mmember{}  A)\}    {}\mrightarrow{}  (consensus-rcv(V;A)  List)@i
6.  ts-init(three-consensus-ts(V;A;t;f)) 
      (ts-rel(three-consensus-ts(V;A;t;f))\^{}*) 
      s@i
7.  y  :  \{a:Id|  (a  \mmember{}  A)\}    {}\mrightarrow{}  (consensus-rcv(V;A)  List)@i
8.  \mforall{}v:V.  \mforall{}a:\{a:Id|  (a  \mmember{}  A)\}  .  \mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}L:consensus-rcv(V;A)  List.
          (L  \mleq{}  s  a
          {}\mRightarrow{}  archive-condition(V;A;t;f;n;v;L)
          {}\mRightarrow{}  (\mexists{}as:\{a:Id|  (a  \mmember{}  A)\}    List
                    (no\_repeats(\{a:Id|  (a  \mmember{}  A)\}  ;as)
                    \mwedge{}  (||as||  =  ((2  *  t)  +  1))
                    \mwedge{}  (\mexists{}vs:V  List
                            ((||vs||  =  ||as||)
                            \mwedge{}  (v  =  (f  vs))
                            \mwedge{}  (\mforall{}i:\mBbbN{}||as||
                                      \mexists{}L:consensus-rcv(V;A)  List
                                        (L  \mleq{}  s  as[i]  \mwedge{}  archive-condition(V;A;t;f;n  -  1;vs[i];L))))))))@i
9.  a1  :  \{a:Id|  (a  \mmember{}  A)\}  @i
10.  y2  :  \{b:Id|  (b  \mmember{}  A)\}  @i
11.  y4  :  \mBbbN{}@i
12.  y5  :  V@i
13.  \mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  \mforall{}i:\mBbbN{}.  \mforall{}v:V.
            ((Vote[y2;y4;y5]  =  Vote[b;i;v])
            {}\mRightarrow{}  ((\mexists{}L:consensus-rcv(V;A)  List.  (L  \mleq{}  s  b  \mwedge{}  archive-condition(V;A;t;f;i;v;L)))
                  \mwedge{}  (\mneg{}(Vote[y2;y4;y5]  \mmember{}  s  a1))))@i
14.  \mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  ((\mneg{}(b  =  a1))  {}\mRightarrow{}  ((y  b)  =  (s  b)))@i
15.  (y  a1)  =  ((s  a1)  @  [Vote[y2;y4;y5]])@i
16.  v  :  V@i
17.  n  :  \mBbbN{}\msupplus{}@i
18.  (s  a1)  =  []
19.  y4  =  n
20.  v  =  y5
21.  (\mexists{}as:\{a:Id|  (a  \mmember{}  A)\}    List
            (no\_repeats(\{a:Id|  (a  \mmember{}  A)\}  ;as)
            \mwedge{}  (||as||  =  ((2  *  t)  +  1))
            \mwedge{}  (\mexists{}vs:V  List
                    ((||vs||  =  ||as||)
                    \mwedge{}  (v  =  (f  vs))
                    \mwedge{}  (\mforall{}i:\mBbbN{}||as||
                              \mexists{}L:consensus-rcv(V;A)  List
                                (L  \mleq{}  s  as[i]  \mwedge{}  archive-condition(V;A;t;f;n  -  1;vs[i];L)))))))
{}\mRightarrow{}  (\mexists{}as:\{a:Id|  (a  \mmember{}  A)\}    List
          (no\_repeats(\{a:Id|  (a  \mmember{}  A)\}  ;as)
          \mwedge{}  (||as||  =  ((2  *  t)  +  1))
          \mwedge{}  (\mexists{}vs:V  List
                  ((||vs||  =  ||as||)
                  \mwedge{}  (v  =  (f  vs))
                  \mwedge{}  (\mforall{}i:\mBbbN{}||as||
                            \mexists{}L:consensus-rcv(V;A)  List
                              (L  \mleq{}  y  as[i]  \mwedge{}  archive-condition(V;A;t;f;n  -  1;vs[i];L)))))))
\mvdash{}  \mexists{}as:\{a:Id|  (a  \mmember{}  A)\}    List
      (no\_repeats(\{a:Id|  (a  \mmember{}  A)\}  ;as)
      \mwedge{}  (||as||  =  ((2  *  t)  +  1))
      \mwedge{}  (\mexists{}vs:V  List
              ((||vs||  =  ||as||)
              \mwedge{}  (y5  =  (f  vs))
              \mwedge{}  (\mforall{}i:\mBbbN{}||as||
                        \mexists{}L:consensus-rcv(V;A)  List
                          (L  \mleq{}  s  as[i]  \mwedge{}  archive-condition(V;A;t;f;y4  -  1;vs[i];L))))))


By

(((InstHyp  [\mkleeneopen{}y2\mkleeneclose{};\mkleeneopen{}y4\mkleeneclose{};\mkleeneopen{}y5\mkleeneclose{}]  (-9)\mcdot{}  THENM  (D  -1  THEN  Thin  (-1)  THEN  RepeatFor  2  (D  -1)))  THENA  Auto)
  THEN  FHyp  8  [-1;-2]
  THEN  Auto)

---

Home Index