Step
*
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
⊢ ((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
{ (Decide ↑null(ys) THENA 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. 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))))
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. 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))))
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
\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
(Decide \muparrow{}null(ys) THENA Auto)
Home
Index