Step
*
of Lemma
consensus-accum-num-property2
∀[V:Type]
∀A:Id List. ∀t:ℕ+. ∀f:(V List) ⟶ V. ∀v0:V. ∀L:consensus-rcv(V;A) List.
let b,i,as,vs,v = consensus-accum-num-state(t;f;v0;L) in
(((2 * t) + 1) ≤ ||remove-repeats(IdDeq;map(λp.(fst(p));votes-from-inning(i - 2;L)))||) supposing
((votes-from-inning(i - 1;L) = [] ∈ (({b:Id| (b ∈ A)} × V) List)) and
1 < i)
BY
{ ((RepeatFor 5 ((D 0 THENA Auto)) THEN (Assert IdDeq ∈ EqDecider({b:Id| (b ∈ A)} ) BY Auto))
THEN (BLemma `last_induction` THENA (Auto THEN GenConclAtAddr [2;1] THEN Auto))
THEN Repeat ((D 0 THENA Complete (Auto)))
THEN RepUR ``consensus-accum-num-state`` 0
THEN Try ((RepUR ``votes-from-inning mapfilter values-for-distinct`` 0 THEN Complete (Auto)))
THEN (RWO "list_accum_append" 0 THENA Auto)
THEN Fold `consensus-accum-num-state` 0
THEN (GenConclAtAddr [1;1] THENA Auto)
THEN RepeatFor 4 (D -2)
THEN Reduce 0
THEN D -7
THEN Try (RepeatFor 2 (D -7))
THEN RepUR ``consensus-accum-num let`` 0
THEN Folds ``cs-initial-rcv cs-rcv-vote`` 0
THEN Repeat (((SplitOnConclITE THENA Complete (Auto)) THEN Reduce 0))
THEN Auto
THEN OnMaybeHyp 17 (\h. (Unfold `votes-from-inning` h
THEN ((RWO "mapfilter-append" h THENA Auto)
THEN Fold `votes-from-inning` h
THEN RWO "append_is_nil" h
THEN Auto
THEN Repeat (ThinTrivial))
))) }
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. x : V@i
9. v1 : 𝔹@i
10. v3 : ℤ@i
11. v5 : {a:Id| (a ∈ A)} List@i
12. v7 : V List@i
13. v8 : V@i
14. consensus-accum-num-state(t;f;v0;ys) = <v1, v3, v5, v7, v8> ∈ (𝔹 × ℤ × {a:Id| (a ∈ A)} List × V List × V)@i
15. ¬(v3 = 0 ∈ ℤ)
16. 1 < v3
17. votes-from-inning(v3 - 1;ys) = [] ∈ (({b:Id| (b ∈ A)} × V) List)
18. votes-from-inning(v3 - 1;[Init[x]]) = [] ∈ (({b:Id| (b ∈ A)} × V) List)
19. ((2 * t) + 1) ≤ ||remove-repeats(IdDeq;map(λp.(fst(p));votes-from-inning(v3 - 2;ys)))||
⊢ ((2 * t) + 1) ≤ ||remove-repeats(IdDeq;map(λp.(fst(p));votes-from-inning(v3 - 2;ys @ [Init[x]])))||
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. v1 : 𝔹@i
12. v3 : ℤ@i
13. v5 : {a:Id| (a ∈ A)} List@i
14. v7 : V List@i
15. v8 : V@i
16. consensus-accum-num-state(t;f;v0;ys) = <v1, v3, v5, v7, v8> ∈ (𝔹 × ℤ × {a:Id| (a ∈ A)} List × V List × V)@i
17. y4 < v3 - 1
18. 1 < v3
19. votes-from-inning(v3 - 1;ys) = [] ∈ (({b:Id| (b ∈ A)} × V) List)
20. votes-from-inning(v3 - 1;[Vote[y2;y4;y5]]) = [] ∈ (({b:Id| (b ∈ A)} × V) List)
21. ((2 * t) + 1) ≤ ||remove-repeats(IdDeq;map(λp.(fst(p));votes-from-inning(v3 - 2;ys)))||
⊢ ((2 * t) + 1) ≤ ||remove-repeats(IdDeq;map(λp.(fst(p));votes-from-inning(v3 - 2;ys @ [Vote[y2;y4;y5]])))||
3
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. v1 : 𝔹@i
12. v3 : ℤ@i
13. v5 : {a:Id| (a ∈ A)} List@i
14. v7 : V List@i
15. v8 : V@i
16. consensus-accum-num-state(t;f;v0;ys) = <v1, v3, v5, v7, v8> ∈ (𝔹 × ℤ × {a:Id| (a ∈ A)} List × V List × V)@i
17. (v3 - 1) ≤ y4
18. v3 - 1 < y4
19. (((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
20. 1 < y4 + 1
21. votes-from-inning((y4 + 1) - 1;ys) = [] ∈ (({b:Id| (b ∈ A)} × V) List)
22. votes-from-inning((y4 + 1) - 1;[Vote[y2;y4;y5]]) = [] ∈ (({b:Id| (b ∈ A)} × V) List)
⊢ ((2 * t) + 1) ≤ ||remove-repeats(IdDeq;map(λp.(fst(p));votes-from-inning((y4 + 1) - 2;ys @ [Vote[y2;y4;y5]])))||
4
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. v1 : 𝔹@i
12. v3 : ℤ@i
13. v5 : {a:Id| (a ∈ A)} List@i
14. v7 : V List@i
15. v8 : V@i
16. consensus-accum-num-state(t;f;v0;ys) = <v1, v3, v5, v7, v8> ∈ (𝔹 × ℤ × {a:Id| (a ∈ A)} List × V List × V)@i
17. (v3 - 1) ≤ y4
18. y4 ≤ (v3 - 1)
19. ||remove-repeats(IdDeq;v5 @ [y2])|| = ((2 * t) + 1) ∈ ℤ
20. (((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
21. 1 < v3 + 1
22. votes-from-inning((v3 + 1) - 1;ys) = [] ∈ (({b:Id| (b ∈ A)} × V) List)
23. votes-from-inning((v3 + 1) - 1;[Vote[y2;y4;y5]]) = [] ∈ (({b:Id| (b ∈ A)} × V) List)
⊢ ((2 * t) + 1) ≤ ||remove-repeats(IdDeq;map(λp.(fst(p));votes-from-inning((v3 + 1) - 2;ys @ [Vote[y2;y4;y5]])))||
5
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. v1 : 𝔹@i
12. v3 : ℤ@i
13. v5 : {a:Id| (a ∈ A)} List@i
14. v7 : V List@i
15. v8 : V@i
16. consensus-accum-num-state(t;f;v0;ys) = <v1, v3, v5, v7, v8> ∈ (𝔹 × ℤ × {a:Id| (a ∈ A)} List × V List × V)@i
17. (v3 - 1) ≤ y4
18. y4 ≤ (v3 - 1)
19. ¬(||remove-repeats(IdDeq;v5 @ [y2])|| = ((2 * t) + 1) ∈ ℤ)
20. 1 < v3
21. votes-from-inning(v3 - 1;ys) = [] ∈ (({b:Id| (b ∈ A)} × V) List)
22. votes-from-inning(v3 - 1;[Vote[y2;y4;y5]]) = [] ∈ (({b:Id| (b ∈ A)} × V) List)
23. ((2 * t) + 1) ≤ ||remove-repeats(IdDeq;map(λp.(fst(p));votes-from-inning(v3 - 2;ys)))||
⊢ ((2 * t) + 1) ≤ ||remove-repeats(IdDeq;map(λp.(fst(p));votes-from-inning(v3 - 2;ys @ [Vote[y2;y4;y5]])))||
Latex:
Latex:
\mforall{}[V:Type]
\mforall{}A:Id List. \mforall{}t:\mBbbN{}\msupplus{}. \mforall{}f:(V List) {}\mrightarrow{} V. \mforall{}v0:V. \mforall{}L:consensus-rcv(V;A) List.
let b,i,as,vs,v = consensus-accum-num-state(t;f;v0;L) in
(((2 * t) + 1) \mleq{} ||remove-repeats(IdDeq;map(\mlambda{}p.(fst(p));votes-from-inning(i
- 2;L)))||) supposing
((votes-from-inning(i - 1;L) = []) and
1 < i)
By
Latex:
((RepeatFor 5 ((D 0 THENA Auto)) THEN (Assert IdDeq \mmember{} EqDecider(\{b:Id| (b \mmember{} A)\} ) BY Auto))
THEN (BLemma `last\_induction` THENA (Auto THEN GenConclAtAddr [2;1] THEN Auto))
THEN Repeat ((D 0 THENA Complete (Auto)))
THEN RepUR ``consensus-accum-num-state`` 0
THEN Try ((RepUR ``votes-from-inning mapfilter values-for-distinct`` 0 THEN Complete (Auto)))
THEN (RWO "list\_accum\_append" 0 THENA Auto)
THEN Fold `consensus-accum-num-state` 0
THEN (GenConclAtAddr [1;1] THENA Auto)
THEN RepeatFor 4 (D -2)
THEN Reduce 0
THEN D -7
THEN Try (RepeatFor 2 (D -7))
THEN RepUR ``consensus-accum-num let`` 0
THEN Folds ``cs-initial-rcv cs-rcv-vote`` 0
THEN Repeat (((SplitOnConclITE THENA Complete (Auto)) THEN Reduce 0))
THEN Auto
THEN OnMaybeHyp 17 (\mbackslash{}h. (Unfold `votes-from-inning` h
THEN ((RWO "mapfilter-append" h THENA Auto)
THEN Fold `votes-from-inning` h
THEN RWO "append\_is\_nil" h
THEN Auto
THEN Repeat (ThinTrivial))
)))
Home
Index