---

Step * 1 1 1 2 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. a : {a:Id| (a ∈ A)} @i
16. n : ℕ+@i
17. L : consensus-rcv(V;A) List@i
18. L ≤ y a@i
19. archive-condition(V;A;t;f;n;v;L)@i
20. as : {a:Id| (a ∈ A)}  List@i
21. no_repeats({a:Id| (a ∈ A)} ;as)@i
22. ||as|| = ((2 * t) + 1) ∈ ℤ@i
23. vs : V List@i
24. ||vs|| = ||as|| ∈ ℤ@i
25. v = (f vs) ∈ V@i
26. ∀i:ℕ||as||. ∃L:consensus-rcv(V;A) List. (L ≤ s as[i] ∧ archive-condition(V;A;t;f;n - 1;vs[i];L))@i
27. i : ℕ||as||@i
28. L1 : consensus-rcv(V;A) List
29. archive-condition(V;A;t;f;n - 1;vs[i];L1)
30. L1 ≤ s as[i]
31. ¬(as[i] = a1 ∈ Id)
⊢ s as[i] ≤ y as[i]
BY
{ ((Subst' (y as[i]) = (s as[i]) ∈ (consensus-rcv(V;A) List) 0 THEN Auto) THEN BLemma `iseg_weakening` 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.  a  :  \{a:Id|  (a  \mmember{}  A)\}  @i
16.  n  :  \mBbbN{}\msupplus{}@i
17.  L  :  consensus-rcv(V;A)  List@i
18.  L  \mleq{}  y  a@i
19.  archive-condition(V;A;t;f;n;v;L)@i
20.  as  :  \{a:Id|  (a  \mmember{}  A)\}    List@i
21.  no\_repeats(\{a:Id|  (a  \mmember{}  A)\}  ;as)@i
22.  ||as||  =  ((2  *  t)  +  1)@i
23.  vs  :  V  List@i
24.  ||vs||  =  ||as||@i
25.  v  =  (f  vs)@i
26.  \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
27.  i  :  \mBbbN{}||as||@i
28.  L1  :  consensus-rcv(V;A)  List
29.  archive-condition(V;A;t;f;n  -  1;vs[i];L1)
30.  L1  \mleq{}  s  as[i]
31.  \mneg{}(as[i]  =  a1)
\mvdash{}  s  as[i]  \mleq{}  y  as[i]


By

((Subst'  (y  as[i])  =  (s  as[i])  0  THEN  Auto)  THEN  BLemma  `iseg\_weakening`  THEN  Auto)

---

Home Index