---

Step * 1 2 1 1 1 1 1 1 1 2 1 1 2 2 3 of Lemma three-cs-safety1


1. V : Type
2. eq : EqDecider(V)
3. A : Id List
4. t : ℕ+
5. no_repeats(Id;A)
6. ||A|| = ((3 * t) + 1) ∈ ℤ
7. W : {a:Id| (a ∈ A)}  List List
8. ∀ws:{a:Id| (a ∈ A)}  List. ((ws ∈ W) ⇐⇒ (||ws|| = ((2 * t) + 1) ∈ ℤ) ∧ no_repeats({a:Id| (a ∈ A)} ;ws))
9. three-intersection(A;W)
10. f : (V List) ⟶ V
11. ∀vs:V List. ∀v:V.
      ((||vs|| = ((2 * t) + 1) ∈ ℤ) ⇒ ((t + 1) ≤ ||filter(λx.(eqof(eq) x v);vs)||) ⇒ ((f vs) = v ∈ V))
12. v : V
13. w : V
14. s : ts-type(three-consensus-ts(V;A;t;f))
15. ts-init(three-consensus-ts(V;A;t;f)) (ts-rel(three-consensus-ts(V;A;t;f))^*) s
16. s ∈ {a:Id| (a ∈ A)}  ⟶ (consensus-rcv(V;A) List)
17. two-intersection(A;W)
18. i : ℤ@i
19. ws : {a:Id| (a ∈ A)}  List@i
20. x : V@i
21. no_repeats({a:Id| (a ∈ A)} ;ws)@i
22. ||ws|| = ((2 * t) + 1) ∈ ℤ@i
23. (∀a∈ws.∃L:consensus-rcv(V;A) List. (L ≤ s a ∧ archive-condition(V;A;t;f;i;x;L)))@i
24. d : ℤ
25. 0 < d
26. 0 < d - 1
⇒ (∀b:{a:Id| (a ∈ A)} 
      ((b ∈ ws)
      ⇒ (∀z:V. ∀L:consensus-rcv(V;A) List.  (L ≤ s b ⇒ archive-condition(V;A;t;f;i + (d - 1);z;L) ⇒ (z = x ∈ V)))))
27. 0 < d@i
28. b : {a:Id| (a ∈ A)} @i
29. (b ∈ ws)@i
30. z : V@i
31. L : consensus-rcv(V;A) List@i
32. L ≤ s b@i
33. archive-condition(V;A;t;f;i + d;z;L)@i
34. 0 ≤ i
35. as : {a:Id| (a ∈ A)}  List
36. no_repeats({a:Id| (a ∈ A)} ;as)
37. ||as|| = ((2 * t) + 1) ∈ ℤ
38. vs : V List
39. ||vs|| = ||as|| ∈ ℤ
40. z = (f vs) ∈ V
41. ∀i1:ℕ||as||. ∃L:consensus-rcv(V;A) List. (L ≤ s as[i1] ∧ archive-condition(V;A;t;f;(i + d) - 1;vs[i1];L))
42. ∀i:ℕ||as||. ((as[i] ∈ ws) ⇒ (vs[i] = x ∈ V))
43. λi.as[i] ∈ {i:ℕ||vs||| ¬↑(eq vs[i] x)}  ⟶ {a:{a:Id| (a ∈ A)} | ¬(a ∈ ws)} 
44. (||vs|| - t) ≤ ||filter(λ2x@0.eq x@0 x;vs)||
⊢ (t + 1) ≤ ||filter(λx@0.(eqof(eq) x@0 x);vs)||
BY
{ (Unfold `eqof` 0 THEN RepUR ``so_lambda`` -1 THEN Auto') }

---

Latex:

---

Latex:

1.  V  :  Type
2.  eq  :  EqDecider(V)
3.  A  :  Id  List
4.  t  :  \mBbbN{}\msupplus{}
5.  no\_repeats(Id;A)
6.  ||A||  =  ((3  *  t)  +  1)
7.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List
8.  \mforall{}ws:\{a:Id|  (a  \mmember{}  A)\}    List.  ((ws  \mmember{}  W)  \mLeftarrow{}{}\mRightarrow{}  (||ws||  =  ((2  *  t)  +  1))  \mwedge{}  no\_repeats(\{a:Id|  (a  \mmember{}  A)\}  ;w\000Cs))
9.  three-intersection(A;W)
10.  f  :  (V  List)  {}\mrightarrow{}  V
11.  \mforall{}vs:V  List.  \mforall{}v:V.
            ((||vs||  =  ((2  *  t)  +  1))  {}\mRightarrow{}  ((t  +  1)  \mleq{}  ||filter(\mlambda{}x.(eqof(eq)  x  v);vs)||)  {}\mRightarrow{}  ((f  vs)  =  v))
12.  v  :  V
13.  w  :  V
14.  s  :  ts-type(three-consensus-ts(V;A;t;f))
15.  ts-init(three-consensus-ts(V;A;t;f)) 
        (ts-rel(three-consensus-ts(V;A;t;f))\^{}*) 
        s
16.  s  \mmember{}  \{a:Id|  (a  \mmember{}  A)\}    {}\mrightarrow{}  (consensus-rcv(V;A)  List)
17.  two-intersection(A;W)
18.  i  :  \mBbbZ{}@i
19.  ws  :  \{a:Id|  (a  \mmember{}  A)\}    List@i
20.  x  :  V@i
21.  no\_repeats(\{a:Id|  (a  \mmember{}  A)\}  ;ws)@i
22.  ||ws||  =  ((2  *  t)  +  1)@i
23.  (\mforall{}a\mmember{}ws.\mexists{}L:consensus-rcv(V;A)  List.  (L  \mleq{}  s  a  \mwedge{}  archive-condition(V;A;t;f;i;x;L)))@i
24.  d  :  \mBbbZ{}
25.  0  <  d
26.  0  <  d  -  1
{}\mRightarrow{}  (\mforall{}b:\{a:Id|  (a  \mmember{}  A)\} 
            ((b  \mmember{}  ws)
            {}\mRightarrow{}  (\mforall{}z:V.  \mforall{}L:consensus-rcv(V;A)  List.
                        (L  \mleq{}  s  b  {}\mRightarrow{}  archive-condition(V;A;t;f;i  +  (d  -  1);z;L)  {}\mRightarrow{}  (z  =  x)))))
27.  0  <  d@i
28.  b  :  \{a:Id|  (a  \mmember{}  A)\}  @i
29.  (b  \mmember{}  ws)@i
30.  z  :  V@i
31.  L  :  consensus-rcv(V;A)  List@i
32.  L  \mleq{}  s  b@i
33.  archive-condition(V;A;t;f;i  +  d;z;L)@i
34.  0  \mleq{}  i
35.  as  :  \{a:Id|  (a  \mmember{}  A)\}    List
36.  no\_repeats(\{a:Id|  (a  \mmember{}  A)\}  ;as)
37.  ||as||  =  ((2  *  t)  +  1)
38.  vs  :  V  List
39.  ||vs||  =  ||as||
40.  z  =  (f  vs)
41.  \mforall{}i1:\mBbbN{}||as||
            \mexists{}L:consensus-rcv(V;A)  List.  (L  \mleq{}  s  as[i1]  \mwedge{}  archive-condition(V;A;t;f;(i  +  d)  -  1;vs[i1];L))
42.  \mforall{}i:\mBbbN{}||as||.  ((as[i]  \mmember{}  ws)  {}\mRightarrow{}  (vs[i]  =  x))
43.  \mlambda{}i.as[i]  \mmember{}  \{i:\mBbbN{}||vs|||  \mneg{}\muparrow{}(eq  vs[i]  x)\}    {}\mrightarrow{}  \{a:\{a:Id|  (a  \mmember{}  A)\}  |  \mneg{}(a  \mmember{}  ws)\} 
44.  (||vs||  -  t)  \mleq{}  ||filter(\mlambda{}\msubtwo{}x@0.eq  x@0  x;vs)||
\mvdash{}  (t  +  1)  \mleq{}  ||filter(\mlambda{}x@0.(eqof(eq)  x@0  x);vs)||


By

---

Latex:
(Unfold  `eqof`  0  THEN  RepUR  ``so\_lambda``  -1  THEN  Auto')

---

Home Index