---

Step * 1 2 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. e : consensus-rcv(V;A)@i
11. ∀b:{a:Id| (a ∈ A)} . ∀i:ℕ. ∀v:V.
      ((e = 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))) ∧ (¬(e ∈ s a1))))@i
12. ∀b:{a:Id| (a ∈ A)} . ((¬(b = a1 ∈ Id)) ⇒ ((y b) = (s b) ∈ (consensus-rcv(V;A) List)))@i
13. (y a1) = ((s a1) @ [e]) ∈ (consensus-rcv(V;A) List)@i
14. v : V@i
15. n : ℕ+@i
16. L : consensus-rcv(V;A) List@i
17. L ≤ s a1
18. archive-condition(V;A;t;f;n;v;L)@i
19. (∃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|| ∈ ℤ)
       ∧ (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))))))
BY
{ ((InstHyp [⌈v⌉;⌈a1⌉;⌈n⌉;⌈L⌉] 8⋅ THENA Auto) THEN BackThruSomeHyp 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.  e  :  consensus-rcv(V;A)@i
11.  \mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  \mforall{}i:\mBbbN{}.  \mforall{}v:V.
            ((e  =  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{}(e  \mmember{}  s  a1))))@i
12.  \mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  ((\mneg{}(b  =  a1))  {}\mRightarrow{}  ((y  b)  =  (s  b)))@i
13.  (y  a1)  =  ((s  a1)  @  [e])@i
14.  v  :  V@i
15.  n  :  \mBbbN{}\msupplus{}@i
16.  L  :  consensus-rcv(V;A)  List@i
17.  L  \mleq{}  s  a1
18.  archive-condition(V;A;t;f;n;v;L)@i
19.  (\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{}  (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))))))


By

((InstHyp  [\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]  8\mcdot{}  THENA  Auto)  THEN  BackThruSomeHyp  THEN  Auto)

---

Home Index