Step
*
2
3
1
of Lemma
archive-consensus-accum-num
1. V : Type
2. A : Id List
3. t : ℕ+
4. f : (V List) ─→ V
5. v0 : V
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. (v3 - 1) ≤ y4
19. y4 ≤ (v3 - 1)
20. ¬(||remove-repeats(IdDeq;v5 @ [y2])|| = ((2 * t) + 1) ∈ ℤ)
21. ∀[v@0:V]. ∀[i:ℤ]. ↑v1 supposing archive-condition(V;A;t;f;i;v@0;ys)@i
22. filter(λr.v3 - 1 <z inning(r);ys) = [] ∈ (consensus-rcv(V;A) List)@i
23. ||v5|| = ||v7|| ∈ ℤ@i
24. zip(v5;v7) = votes-from-inning(v3 - 1;ys) ∈ (({b:Id| (b ∈ A)} × V) List)@i
25. 0 ≤ v3@i
26. 1 ≤ v3 supposing ¬↑null(ys)@i
27. ||values-for-distinct(IdDeq;votes-from-inning(v3 - 1;ys))|| ≤ (2 * t)@i
28. filter(λr.v3 - 1 <z inning(r);ys @ [Vote[y2;y4;y5]]) = [] ∈ (consensus-rcv(V;A) List)@i
29. ||v5 @ [y2]|| = ||v7 @ [y5]|| ∈ ℤ@i
30. zip(v5 @ [y2];v7 @ [y5]) = votes-from-inning(v3 - 1;ys @ [Vote[y2;y4;y5]]) ∈ (({b:Id| (b ∈ A)} × V) List)@i
31. 0 ≤ v3@i
32. 1 ≤ v3 supposing ¬↑null(ys @ [Vote[y2;y4;y5]])@i
33. ||values-for-distinct(IdDeq;votes-from-inning(v3 - 1;ys @ [Vote[y2;y4;y5]]))|| ≤ (2 * t)@i
34. v@0 : V
35. i : ℤ
36. 0 < i
37. ||values-for-distinct(IdDeq;votes-from-inning(i - 1;ys))|| ≤ (2 * t)
38. ↑null(filter(λr.i - 1 <z inning(r);ys))
39. y4 = i ∈ ℤ
40. v@0 = y5 ∈ V
41. i < v3
42. votes-from-inning(v3 - 1;ys) ~ []
43. ((2 * t) + 1) ≤ ||remove-repeats(IdDeq;map(λp.(fst(p));votes-from-inning(v3 - 2;ys)))||
⊢ False
BY
{ ((Decide i < v3 - 1 THENA Auto)
THENL [((Assert votes-from-inning(v3 - 2;ys) ~ [] BY
OnMaybeHyp 36 (\h. ((RW assert_pushdownC h THENA Auto)
THEN Using [`i',⌈v3 - 2⌉] (FLemma `votes-from-inning-is-nil` [h])⋅
THEN Auto)))
THEN HypSubst' -1 -3
THEN Reduce (-3)
THEN Auto')
; ((Assert i = (v3 - 1) ∈ ℤ BY Auto) THEN ElimVar `i' THEN Auto)]
) }
1
1. V : Type
2. A : Id List
3. t : ℕ+
4. f : (V List) ─→ V
5. v0 : V
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. (v3 - 1) ≤ y4
19. y4 ≤ (v3 - 1)
20. ¬(||remove-repeats(IdDeq;v5 @ [y2])|| = ((2 * t) + 1) ∈ ℤ)
21. ∀[v@0:V]. ∀[i:ℤ]. ↑v1 supposing archive-condition(V;A;t;f;i;v@0;ys)@i
22. filter(λr.v3 - 1 <z inning(r);ys) = [] ∈ (consensus-rcv(V;A) List)@i
23. ||v5|| = ||v7|| ∈ ℤ@i
24. zip(v5;v7) = votes-from-inning(v3 - 1;ys) ∈ (({b:Id| (b ∈ A)} × V) List)@i
25. 0 ≤ v3@i
26. 1 ≤ v3 supposing ¬↑null(ys)@i
27. ||values-for-distinct(IdDeq;votes-from-inning(v3 - 1;ys))|| ≤ (2 * t)@i
28. filter(λr.v3 - 1 <z inning(r);ys @ [Vote[y2;y4;y5]]) = [] ∈ (consensus-rcv(V;A) List)@i
29. ||v5 @ [y2]|| = ||v7 @ [y5]|| ∈ ℤ@i
30. zip(v5 @ [y2];v7 @ [y5]) = votes-from-inning(v3 - 1;ys @ [Vote[y2;y4;y5]]) ∈ (({b:Id| (b ∈ A)} × V) List)@i
31. 0 ≤ v3@i
32. 1 ≤ v3 supposing ¬↑null(ys @ [Vote[y2;y4;y5]])@i
33. ||values-for-distinct(IdDeq;votes-from-inning(v3 - 1;ys @ [Vote[y2;y4;y5]]))|| ≤ (2 * t)@i
34. v@0 : V
35. i : ℤ
36. y4 ∈ ℤ
37. 0 < y4
38. ||values-for-distinct(IdDeq;votes-from-inning(y4 - 1;ys))|| ≤ (2 * t)
39. ↑null(filter(λr.y4 - 1 <z inning(r);ys))
40. v@0 = y5 ∈ V
41. y4 < v3
42. votes-from-inning(v3 - 1;ys) ~ []
43. ((2 * t) + 1) ≤ ||remove-repeats(IdDeq;map(λp.(fst(p));votes-from-inning(v3 - 2;ys)))||
44. ¬y4 < v3 - 1
45. y4 = (v3 - 1) ∈ ℤ
⊢ False
Latex:
1. V : Type
2. A : Id List
3. t : \mBbbN{}\msupplus{}
4. f : (V List) {}\mrightarrow{} V
5. v0 : V
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. (v3 - 1) \mleq{} y4
19. y4 \mleq{} (v3 - 1)
20. \mneg{}(||remove-repeats(IdDeq;v5 @ [y2])|| = ((2 * t) + 1))
21. \mforall{}[v@0:V]. \mforall{}[i:\mBbbZ{}]. \muparrow{}v1 supposing archive-condition(V;A;t;f;i;v@0;ys)@i
22. filter(\mlambda{}r.v3 - 1 <z inning(r);ys) = []@i
23. ||v5|| = ||v7||@i
24. zip(v5;v7) = votes-from-inning(v3 - 1;ys)@i
25. 0 \mleq{} v3@i
26. 1 \mleq{} v3 supposing \mneg{}\muparrow{}null(ys)@i
27. ||values-for-distinct(IdDeq;votes-from-inning(v3 - 1;ys))|| \mleq{} (2 * t)@i
28. filter(\mlambda{}r.v3 - 1 <z inning(r);ys @ [Vote[y2;y4;y5]]) = []@i
29. ||v5 @ [y2]|| = ||v7 @ [y5]||@i
30. zip(v5 @ [y2];v7 @ [y5]) = votes-from-inning(v3 - 1;ys @ [Vote[y2;y4;y5]])@i
31. 0 \mleq{} v3@i
32. 1 \mleq{} v3 supposing \mneg{}\muparrow{}null(ys @ [Vote[y2;y4;y5]])@i
33. ||values-for-distinct(IdDeq;votes-from-inning(v3 - 1;ys @ [Vote[y2;y4;y5]]))|| \mleq{} (2 * t)@i
34. v@0 : V
35. i : \mBbbZ{}
36. 0 < i
37. ||values-for-distinct(IdDeq;votes-from-inning(i - 1;ys))|| \mleq{} (2 * t)
38. \muparrow{}null(filter(\mlambda{}r.i - 1 <z inning(r);ys))
39. y4 = i
40. v@0 = y5
41. i < v3
42. votes-from-inning(v3 - 1;ys) \msim{} []
43. ((2 * t) + 1) \mleq{} ||remove-repeats(IdDeq;map(\mlambda{}p.(fst(p));votes-from-inning(v3 - 2;ys)))||
\mvdash{} False
By
((Decide i < v3 - 1 THENA Auto)
THENL [((Assert votes-from-inning(v3 - 2;ys) \msim{} [] BY
OnMaybeHyp 36 (\mbackslash{}h. ((RW assert\_pushdownC h THENA Auto)
THEN Using [`i',\mkleeneopen{}v3 - 2\mkleeneclose{}
] (FLemma `votes-from-inning-is-nil` [h])\mcdot{}
THEN Auto)))
THEN HypSubst' -1 -3
THEN Reduce (-3)
THEN Auto')
; ((Assert i = (v3 - 1) BY Auto) THEN ElimVar `i' THEN Auto)]
)
Home
Index