---

Step * 2 2 2 of Lemma consensus-accum-num-archives


1. [V] : Type
2. A : Id List@i
3. t : ℕ+@i
4. f : (V List) ─→ V@i
5. v0 : V@i
6. IdDeq ∈ EqDecider({b:Id| (b ∈ A)} )
7. ys : consensus-rcv(V;A) List@i
8. y2 : {b:Id| (b ∈ A)} @i
9. y4 : ℕ@i
10. y5 : V@i
11. Vote[y2;y4;y5] ∈ consensus-rcv(V;A)
12. v1 : 𝔹@i
13. v3 : ℤ@i
14. v5 : {a:Id| (a ∈ A)}  List@i
15. v7 : V List@i
16. v8 : V@i
17. consensus-accum-num-state(t;f;v0;ys) = <v1, v3, v5, v7, v8> ∈ (𝔹 × ℤ × {a:Id| (a ∈ A)}  List × V List × V)@i
18. archive-condition(V;A;t;f;v3 - 1;v8;ys) supposing ↑v1@i
19. (v3 - 1) ≤ y4
20. v3 - 1 < y4
21. filter(λr.v3 - 1 <z inning(r);ys) = [] ∈ (consensus-rcv(V;A) List)@i
22. ||v5|| = ||v7|| ∈ ℤ@i
23. zip(v5;v7) = votes-from-inning(v3 - 1;ys) ∈ (({b:Id| (b ∈ A)}  × V) List)@i
24. 0 ≤ v3@i
25. 1 ≤ v3 supposing ¬↑null(ys)@i
26. ||values-for-distinct(IdDeq;votes-from-inning(v3 - 1;ys))|| ≤ (2 * t)@i
27. filter(λr.(y4 + 1) - 1 <z inning(r);ys @ [Vote[y2;y4;y5]]) = [] ∈ (consensus-rcv(V;A) List)@i
28. 1 = 1 ∈ ℤ@i
29. [<y2, y5>] = votes-from-inning((y4 + 1) - 1;ys @ [Vote[y2;y4;y5]]) ∈ (({b:Id| (b ∈ A)}  × V) List)@i
30. 0 ≤ (y4 + 1)@i
31. 1 ≤ (y4 + 1) supposing ¬↑null(ys @ [Vote[y2;y4;y5]])@i
32. ||values-for-distinct(IdDeq;votes-from-inning((y4 + 1) - 1;ys @ [Vote[y2;y4;y5]]))|| ≤ (2 * t)@i
33. True
34. ¬↑null(ys)
⊢ ((ys = [] ∈ (consensus-rcv(V;A) List)) ∧ (y4 = ((y4 + 1) - 1) ∈ ℤ) ∧ (y5 = y5 ∈ V))
∨ ((0 < (y4 + 1) - 1 ∧ (||values-for-distinct(IdDeq;votes-from-inning((y4 + 1) - 1 - 1;ys))|| ≤ (2 * t)))
  ∧ (↑null(filter(λr.(y4 + 1) - 1 - 1 <z inning(r);ys)))
  ∧ (((y4 = ((y4 + 1) - 1) ∈ ℤ) ∧ (y5 = y5 ∈ V))
    ∨ ((((2 * t) + 1) ≤ ||values-for-distinct(IdDeq;votes-from-inning((y4 + 1) - 1 - 1;ys @ [Vote[y2;y4;y5]]))||)
      ∧ ((f values-for-distinct(IdDeq;votes-from-inning((y4 + 1) - 1 - 1;ys @ [Vote[y2;y4;y5]]))) = y5 ∈ V))))
BY
{ (ThinTrivial THEN OrRight THEN Auto) }

1
1. [V] : Type
2. A : Id List@i
3. t : ℕ+@i
4. f : (V List) ─→ V@i
5. v0 : V@i
6. IdDeq ∈ EqDecider({b:Id| (b ∈ A)} )
7. ys : consensus-rcv(V;A) List@i
8. y2 : {b:Id| (b ∈ A)} @i
9. y4 : ℕ@i
10. y5 : V@i
11. Vote[y2;y4;y5] ∈ consensus-rcv(V;A)
12. v1 : 𝔹@i
13. v3 : ℤ@i
14. v5 : {a:Id| (a ∈ A)}  List@i
15. v7 : V List@i
16. v8 : V@i
17. consensus-accum-num-state(t;f;v0;ys) = <v1, v3, v5, v7, v8> ∈ (𝔹 × ℤ × {a:Id| (a ∈ A)}  List × V List × V)@i
18. archive-condition(V;A;t;f;v3 - 1;v8;ys) supposing ↑v1@i
19. (v3 - 1) ≤ y4
20. v3 - 1 < y4
21. filter(λr.v3 - 1 <z inning(r);ys) = [] ∈ (consensus-rcv(V;A) List)@i
22. ||v5|| = ||v7|| ∈ ℤ@i
23. zip(v5;v7) = votes-from-inning(v3 - 1;ys) ∈ (({b:Id| (b ∈ A)}  × V) List)@i
24. 0 ≤ v3@i
25. ||values-for-distinct(IdDeq;votes-from-inning(v3 - 1;ys))|| ≤ (2 * t)@i
26. filter(λr.(y4 + 1) - 1 <z inning(r);ys @ [Vote[y2;y4;y5]]) = [] ∈ (consensus-rcv(V;A) List)@i
27. 1 = 1 ∈ ℤ@i
28. [<y2, y5>] = votes-from-inning((y4 + 1) - 1;ys @ [Vote[y2;y4;y5]]) ∈ (({b:Id| (b ∈ A)}  × V) List)@i
29. 0 ≤ (y4 + 1)@i
30. 1 ≤ (y4 + 1) supposing ¬↑null(ys @ [Vote[y2;y4;y5]])@i
31. ||values-for-distinct(IdDeq;votes-from-inning((y4 + 1) - 1;ys @ [Vote[y2;y4;y5]]))|| ≤ (2 * t)@i
32. ¬↑null(ys)
33. 1 ≤ v3
34. 0 < (y4 + 1) - 1
⊢ ||values-for-distinct(IdDeq;votes-from-inning((y4 + 1) - 1 - 1;ys))|| ≤ (2 * t)

2
1. V : Type
2. A : Id List@i
3. t : ℕ+@i
4. f : (V List) ─→ V@i
5. v0 : V@i
6. IdDeq ∈ EqDecider({b:Id| (b ∈ A)} )
7. ys : consensus-rcv(V;A) List@i
8. y2 : {b:Id| (b ∈ A)} @i
9. y4 : ℕ@i
10. y5 : V@i
11. Vote[y2;y4;y5] ∈ consensus-rcv(V;A)
12. v1 : 𝔹@i
13. v3 : ℤ@i
14. v5 : {a:Id| (a ∈ A)}  List@i
15. v7 : V List@i
16. v8 : V@i
17. consensus-accum-num-state(t;f;v0;ys) = <v1, v3, v5, v7, v8> ∈ (𝔹 × ℤ × {a:Id| (a ∈ A)}  List × V List × V)@i
18. archive-condition(V;A;t;f;v3 - 1;v8;ys) supposing ↑v1@i
19. (v3 - 1) ≤ y4
20. v3 - 1 < y4
21. filter(λr.v3 - 1 <z inning(r);ys) = [] ∈ (consensus-rcv(V;A) List)@i
22. ||v5|| = ||v7|| ∈ ℤ@i
23. zip(v5;v7) = votes-from-inning(v3 - 1;ys) ∈ (({b:Id| (b ∈ A)}  × V) List)@i
24. 0 ≤ v3@i
25. ||values-for-distinct(IdDeq;votes-from-inning(v3 - 1;ys))|| ≤ (2 * t)@i
26. filter(λr.(y4 + 1) - 1 <z inning(r);ys @ [Vote[y2;y4;y5]]) = [] ∈ (consensus-rcv(V;A) List)@i
27. 1 = 1 ∈ ℤ@i
28. [<y2, y5>] = votes-from-inning((y4 + 1) - 1;ys @ [Vote[y2;y4;y5]]) ∈ (({b:Id| (b ∈ A)}  × V) List)@i
29. 0 ≤ (y4 + 1)@i
30. 1 ≤ (y4 + 1) supposing ¬↑null(ys @ [Vote[y2;y4;y5]])@i
31. ||values-for-distinct(IdDeq;votes-from-inning((y4 + 1) - 1;ys @ [Vote[y2;y4;y5]]))|| ≤ (2 * t)@i
32. ¬↑null(ys)
33. 1 ≤ v3
34. 0 < (y4 + 1) - 1
35. ||values-for-distinct(IdDeq;votes-from-inning((y4 + 1) - 1 - 1;ys))|| ≤ (2 * t)
⊢ filter(λr.(y4 + 1) - 1 - 1 <z inning(r);ys) = [] ∈ (consensus-rcv(V;A) List)

---

Latex:



1.  [V]  :  Type
2.  A  :  Id  List@i
3.  t  :  \mBbbN{}\msupplus{}@i
4.  f  :  (V  List)  {}\mrightarrow{}  V@i
5.  v0  :  V@i
6.  IdDeq  \mmember{}  EqDecider(\{b:Id|  (b  \mmember{}  A)\}  )
7.  ys  :  consensus-rcv(V;A)  List@i
8.  y2  :  \{b:Id|  (b  \mmember{}  A)\}  @i
9.  y4  :  \mBbbN{}@i
10.  y5  :  V@i
11.  Vote[y2;y4;y5]  \mmember{}  consensus-rcv(V;A)
12.  v1  :  \mBbbB{}@i
13.  v3  :  \mBbbZ{}@i
14.  v5  :  \{a:Id|  (a  \mmember{}  A)\}    List@i
15.  v7  :  V  List@i
16.  v8  :  V@i
17.  consensus-accum-num-state(t;f;v0;ys)  =  <v1,  v3,  v5,  v7,  v8>@i
18.  archive-condition(V;A;t;f;v3  -  1;v8;ys)  supposing  \muparrow{}v1@i
19.  (v3  -  1)  \mleq{}  y4
20.  v3  -  1  <  y4
21.  filter(\mlambda{}r.v3  -  1  <z  inning(r);ys)  =  []@i
22.  ||v5||  =  ||v7||@i
23.  zip(v5;v7)  =  votes-from-inning(v3  -  1;ys)@i
24.  0  \mleq{}  v3@i
25.  1  \mleq{}  v3  supposing  \mneg{}\muparrow{}null(ys)@i
26.  ||values-for-distinct(IdDeq;votes-from-inning(v3  -  1;ys))||  \mleq{}  (2  *  t)@i
27.  filter(\mlambda{}r.(y4  +  1)  -  1  <z  inning(r);ys  @  [Vote[y2;y4;y5]])  =  []@i
28.  1  =  1@i
29.  [<y2,  y5>]  =  votes-from-inning((y4  +  1)  -  1;ys  @  [Vote[y2;y4;y5]])@i
30.  0  \mleq{}  (y4  +  1)@i
31.  1  \mleq{}  (y4  +  1)  supposing  \mneg{}\muparrow{}null(ys  @  [Vote[y2;y4;y5]])@i
32.  ||values-for-distinct(IdDeq;votes-from-inning((y4  +  1)  -  1;ys  @  [Vote[y2;y4;y5]]))||  \mleq{}  (2  *  t)@i
33.  True
34.  \mneg{}\muparrow{}null(ys)
\mvdash{}  ((ys  =  [])  \mwedge{}  (y4  =  ((y4  +  1)  -  1))  \mwedge{}  (y5  =  y5))
\mvee{}  ((0  <  (y4  +  1)  -  1
      \mwedge{}  (||values-for-distinct(IdDeq;votes-from-inning((y4  +  1)  -  1  -  1;ys))||  \mleq{}  (2  *  t)))
    \mwedge{}  (\muparrow{}null(filter(\mlambda{}r.(y4  +  1)  -  1  -  1  <z  inning(r);ys)))
    \mwedge{}  (((y4  =  ((y4  +  1)  -  1))  \mwedge{}  (y5  =  y5))
        \mvee{}  ((((2  *  t)  +  1)  \mleq{}  ||values-for-distinct(IdDeq;votes-from-inning((y4  +  1)  -  1  -  1;ys
                @  [Vote[y2;y4;y5]]))||)
            \mwedge{}  ((f  values-for-distinct(IdDeq;votes-from-inning((y4  +  1)  -  1  -  1;ys  @  [Vote[y2;y4;y5]])))
                =  y5))))


By

(ThinTrivial  THEN  OrRight  THEN  Auto)

---

Home Index