Step
*
2
of Lemma
archive-consensus-accum-num
1. V : Type
2. A : Id List
3. t : ℕ+
4. f : (V List) ─→ V
5. v0 : V
⊢ ∀ys:consensus-rcv(V;A) List. ∀y:consensus-rcv(V;A).
((∀[v:V]. ∀[i:ℤ]. ↑(fst(consensus-accum-num-state(t;f;v0;ys))) supposing archive-condition(V;A;t;f;i;v;ys))
⇒ (∀[v:V]. ∀[i:ℤ].
↑(fst(consensus-accum-num-state(t;f;v0;ys @ [y]))) supposing archive-condition(V;A;t;f;i;v;ys @ [y])))
BY
{ ((Assert IdDeq ∈ EqDecider({b:Id| (b ∈ A)} ) BY
Auto)
THEN (RepeatFor 2 ((D 0 THENA Auto)) THEN (Assert y ∈ consensus-rcv(V;A) BY Trivial))
THEN (At ⌈Type⌉ (D 0)⋅ THENA Auto)
THEN (InstLemma `consensus-accum-num-property1` [⌈V⌉;⌈A⌉;⌈t⌉;⌈f⌉;⌈v0⌉]⋅ THENA Auto)
THEN ((InstHyp [⌈ys @ [y]⌉] (-1)⋅ THENA Auto) THEN MoveToConcl (-1))
THEN (InstHyp [⌈ys⌉] (-1)⋅ THENA Auto)
THEN MoveToConcl (-1)
THEN Thin (-1)
THEN MoveToConcl (-1)
THEN (InstLemma `consensus-accum-num-property2` [⌈V⌉;⌈A⌉;⌈t⌉;⌈f⌉;⌈v0⌉;⌈ys⌉]⋅ THENA Auto)
THEN MoveToConcl (-1)
THEN Unfold `consensus-accum-num-state` 0
THEN (RWO "list_accum_append" 0 THENA Auto)
THEN Fold `consensus-accum-num-state` 0
THEN GenConclAtAddr [1;1]
THEN RepeatFor 4 (D -2)
THEN Reduce 0
THEN (D 0 THENA Auto)
THEN (D -9 THEN Try (RepeatFor 2 (D -9)))
THEN RepUR ``consensus-accum-num let`` 0
THEN All (Folds ``cs-initial-rcv cs-rcv-vote``)⋅
THEN Repeat (((SplitOnConclITE THENA Auto) THEN Reduce 0))
THEN (UnivCD THENA Auto)
THEN ExRepD
THEN (Try (Trivial) THEN Try (((RWO "archive-condition-append-init" (-1) THENA Auto) THEN D -1 THEN Auto)))
THEN Try (((RWO "archive-condition-append-vote" (-1) THENA Auto) THEN RepeatFor 2 ((SplitOrHyps THEN ExRepD))))
THEN Try (((Assert v3 = 0 ∈ ℤ BY
(DVar `ys'
THEN Auto
THEN OnMaybeHyp 16 (\h. (RepUR ``consensus-accum-num-state`` h THEN Complete (Auto)))))
THEN Complete (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. (((2 * t) + 1) ≤ ||remove-repeats(IdDeq;map(λp.(fst(p));votes-from-inning(v3 - 2;ys)))||) supposing
((votes-from-inning(v3 - 1;ys) = [] ∈ (({b:Id| (b ∈ A)} × V) List)) and
1 < v3)@i
19. y4 < v3 - 1
20. ∀[v@0:V]. ∀[i:ℤ]. ↑v1 supposing archive-condition(V;A;t;f;i;v@0;ys)@i
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.v3 - 1 <z inning(r);ys @ [Vote[y2;y4;y5]]) = [] ∈ (consensus-rcv(V;A) List)@i
28. ||v5|| = ||v7|| ∈ ℤ@i
29. zip(v5;v7) = votes-from-inning(v3 - 1;ys @ [Vote[y2;y4;y5]]) ∈ (({b:Id| (b ∈ A)} × V) List)@i
30. 0 ≤ v3@i
31. 1 ≤ v3 supposing ¬↑null(ys @ [Vote[y2;y4;y5]])@i
32. ||values-for-distinct(IdDeq;votes-from-inning(v3 - 1;ys @ [Vote[y2;y4;y5]]))|| ≤ (2 * t)@i
33. v@0 : V
34. i : ℤ
35. 0 < i
36. ||values-for-distinct(IdDeq;votes-from-inning(i - 1;ys))|| ≤ (2 * t)
37. ↑null(filter(λr.i - 1 <z inning(r);ys))
38. y4 = i ∈ ℤ
39. v@0 = y5 ∈ V
⊢ False
2
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. (((2 * t) + 1) ≤ ||remove-repeats(IdDeq;map(λp.(fst(p));votes-from-inning(v3 - 2;ys)))||) supposing
((votes-from-inning(v3 - 1;ys) = [] ∈ (({b:Id| (b ∈ A)} × V) List)) and
1 < v3)@i
19. y4 < v3 - 1
20. ∀[v@0:V]. ∀[i:ℤ]. ↑v1 supposing archive-condition(V;A;t;f;i;v@0;ys)@i
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.v3 - 1 <z inning(r);ys @ [Vote[y2;y4;y5]]) = [] ∈ (consensus-rcv(V;A) List)@i
28. ||v5|| = ||v7|| ∈ ℤ@i
29. zip(v5;v7) = votes-from-inning(v3 - 1;ys @ [Vote[y2;y4;y5]]) ∈ (({b:Id| (b ∈ A)} × V) List)@i
30. 0 ≤ v3@i
31. 1 ≤ v3 supposing ¬↑null(ys @ [Vote[y2;y4;y5]])@i
32. ||values-for-distinct(IdDeq;votes-from-inning(v3 - 1;ys @ [Vote[y2;y4;y5]]))|| ≤ (2 * t)@i
33. v@0 : V
34. i : ℤ
35. 0 < i
36. ||values-for-distinct(IdDeq;votes-from-inning(i - 1;ys))|| ≤ (2 * t)
37. ↑null(filter(λr.i - 1 <z inning(r);ys))
38. ((2 * t) + 1) ≤ ||values-for-distinct(IdDeq;votes-from-inning(i - 1;ys @ [Vote[y2;y4;y5]]))||
39. (f values-for-distinct(IdDeq;votes-from-inning(i - 1;ys @ [Vote[y2;y4;y5]]))) = v@0 ∈ V
⊢ False
3
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. (((2 * t) + 1) ≤ ||remove-repeats(IdDeq;map(λp.(fst(p));votes-from-inning(v3 - 2;ys)))||) supposing
((votes-from-inning(v3 - 1;ys) = [] ∈ (({b:Id| (b ∈ A)} × V) List)) and
1 < v3)@i
19. (v3 - 1) ≤ y4
20. y4 ≤ (v3 - 1)
21. ¬(||remove-repeats(IdDeq;v5 @ [y2])|| = ((2 * t) + 1) ∈ ℤ)
22. ∀[v@0:V]. ∀[i:ℤ]. ↑v1 supposing archive-condition(V;A;t;f;i;v@0;ys)@i
23. filter(λr.v3 - 1 <z inning(r);ys) = [] ∈ (consensus-rcv(V;A) List)@i
24. ||v5|| = ||v7|| ∈ ℤ@i
25. zip(v5;v7) = votes-from-inning(v3 - 1;ys) ∈ (({b:Id| (b ∈ A)} × V) List)@i
26. 0 ≤ v3@i
27. 1 ≤ v3 supposing ¬↑null(ys)@i
28. ||values-for-distinct(IdDeq;votes-from-inning(v3 - 1;ys))|| ≤ (2 * t)@i
29. filter(λr.v3 - 1 <z inning(r);ys @ [Vote[y2;y4;y5]]) = [] ∈ (consensus-rcv(V;A) List)@i
30. ||v5 @ [y2]|| = ||v7 @ [y5]|| ∈ ℤ@i
31. zip(v5 @ [y2];v7 @ [y5]) = votes-from-inning(v3 - 1;ys @ [Vote[y2;y4;y5]]) ∈ (({b:Id| (b ∈ A)} × V) List)@i
32. 0 ≤ v3@i
33. 1 ≤ v3 supposing ¬↑null(ys @ [Vote[y2;y4;y5]])@i
34. ||values-for-distinct(IdDeq;votes-from-inning(v3 - 1;ys @ [Vote[y2;y4;y5]]))|| ≤ (2 * t)@i
35. v@0 : V
36. i : ℤ
37. 0 < i
38. ||values-for-distinct(IdDeq;votes-from-inning(i - 1;ys))|| ≤ (2 * t)
39. ↑null(filter(λr.i - 1 <z inning(r);ys))
40. y4 = i ∈ ℤ
41. v@0 = y5 ∈ V
⊢ False
4
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. (((2 * t) + 1) ≤ ||remove-repeats(IdDeq;map(λp.(fst(p));votes-from-inning(v3 - 2;ys)))||) supposing
((votes-from-inning(v3 - 1;ys) = [] ∈ (({b:Id| (b ∈ A)} × V) List)) and
1 < v3)@i
19. (v3 - 1) ≤ y4
20. y4 ≤ (v3 - 1)
21. ¬(||remove-repeats(IdDeq;v5 @ [y2])|| = ((2 * t) + 1) ∈ ℤ)
22. ∀[v@0:V]. ∀[i:ℤ]. ↑v1 supposing archive-condition(V;A;t;f;i;v@0;ys)@i
23. filter(λr.v3 - 1 <z inning(r);ys) = [] ∈ (consensus-rcv(V;A) List)@i
24. ||v5|| = ||v7|| ∈ ℤ@i
25. zip(v5;v7) = votes-from-inning(v3 - 1;ys) ∈ (({b:Id| (b ∈ A)} × V) List)@i
26. 0 ≤ v3@i
27. 1 ≤ v3 supposing ¬↑null(ys)@i
28. ||values-for-distinct(IdDeq;votes-from-inning(v3 - 1;ys))|| ≤ (2 * t)@i
29. filter(λr.v3 - 1 <z inning(r);ys @ [Vote[y2;y4;y5]]) = [] ∈ (consensus-rcv(V;A) List)@i
30. ||v5 @ [y2]|| = ||v7 @ [y5]|| ∈ ℤ@i
31. zip(v5 @ [y2];v7 @ [y5]) = votes-from-inning(v3 - 1;ys @ [Vote[y2;y4;y5]]) ∈ (({b:Id| (b ∈ A)} × V) List)@i
32. 0 ≤ v3@i
33. 1 ≤ v3 supposing ¬↑null(ys @ [Vote[y2;y4;y5]])@i
34. ||values-for-distinct(IdDeq;votes-from-inning(v3 - 1;ys @ [Vote[y2;y4;y5]]))|| ≤ (2 * t)@i
35. v@0 : V
36. i : ℤ
37. 0 < i
38. ||values-for-distinct(IdDeq;votes-from-inning(i - 1;ys))|| ≤ (2 * t)
39. ↑null(filter(λr.i - 1 <z inning(r);ys))
40. ((2 * t) + 1) ≤ ||values-for-distinct(IdDeq;votes-from-inning(i - 1;ys @ [Vote[y2;y4;y5]]))||
41. (f values-for-distinct(IdDeq;votes-from-inning(i - 1;ys @ [Vote[y2;y4;y5]]))) = v@0 ∈ V
⊢ False
Latex:
1. V : Type
2. A : Id List
3. t : \mBbbN{}\msupplus{}
4. f : (V List) {}\mrightarrow{} V
5. v0 : V
\mvdash{} \mforall{}ys:consensus-rcv(V;A) List. \mforall{}y:consensus-rcv(V;A).
((\mforall{}[v:V]. \mforall{}[i:\mBbbZ{}].
\muparrow{}(fst(consensus-accum-num-state(t;f;v0;ys))) supposing archive-condition(V;A;t;f;i;v;ys))
{}\mRightarrow{} (\mforall{}[v:V]. \mforall{}[i:\mBbbZ{}].
\muparrow{}(fst(consensus-accum-num-state(t;f;v0;ys @ [y])))
supposing archive-condition(V;A;t;f;i;v;ys @ [y])))
By
((Assert IdDeq \mmember{} EqDecider(\{b:Id| (b \mmember{} A)\} ) BY
Auto)
THEN (RepeatFor 2 ((D 0 THENA Auto)) THEN (Assert y \mmember{} consensus-rcv(V;A) BY Trivial))
THEN (At \mkleeneopen{}Type\mkleeneclose{} (D 0)\mcdot{} THENA Auto)
THEN (InstLemma `consensus-accum-num-property1` [\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}v0\mkleeneclose{}]\mcdot{} THENA Auto)
THEN ((InstHyp [\mkleeneopen{}ys @ [y]\mkleeneclose{}] (-1)\mcdot{} THENA Auto) THEN MoveToConcl (-1))
THEN (InstHyp [\mkleeneopen{}ys\mkleeneclose{}] (-1)\mcdot{} THENA Auto)
THEN MoveToConcl (-1)
THEN Thin (-1)
THEN MoveToConcl (-1)
THEN (InstLemma `consensus-accum-num-property2` [\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}v0\mkleeneclose{};\mkleeneopen{}ys\mkleeneclose{}]\mcdot{} THENA Auto)
THEN MoveToConcl (-1)
THEN Unfold `consensus-accum-num-state` 0
THEN (RWO "list\_accum\_append" 0 THENA Auto)
THEN Fold `consensus-accum-num-state` 0
THEN GenConclAtAddr [1;1]
THEN RepeatFor 4 (D -2)
THEN Reduce 0
THEN (D 0 THENA Auto)
THEN (D -9 THEN Try (RepeatFor 2 (D -9)))
THEN RepUR ``consensus-accum-num let`` 0
THEN All (Folds ``cs-initial-rcv cs-rcv-vote``)\mcdot{}
THEN Repeat (((SplitOnConclITE THENA Auto) THEN Reduce 0))
THEN (UnivCD THENA Auto)
THEN ExRepD
THEN (Try (Trivial)
THEN Try (((RWO "archive-condition-append-init" (-1) THENA Auto) THEN D -1 THEN Auto))
)
THEN Try (((RWO "archive-condition-append-vote" (-1) THENA Auto)
THEN RepeatFor 2 ((SplitOrHyps THEN ExRepD))
))
THEN Try (((Assert v3 = 0 BY
(DVar `ys'
THEN Auto
THEN OnMaybeHyp 16 (\mbackslash{}h. (RepUR ``consensus-accum-num-state`` h
THEN Complete (Auto)
))))
THEN Complete (Auto')
)))
Home
Index