---

Step * 4 of Lemma consensus-accum-num-property2


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]])))||
BY
{ ((InstLemma `consensus-accum-num-property1` [⌈V⌉;⌈A⌉;⌈t⌉;⌈f⌉;⌈v0⌉;⌈ys⌉]⋅ THENA Auto)
   THEN At ⌈Type⌉ (HypSubst' 16 -1)⋅
   THEN (Reduce (-1) 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. 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)
24. filter(λr.v3 - 1 <z inning(r);ys) = [] ∈ (consensus-rcv(V;A) List)
25. ||v5|| = ||v7|| ∈ ℤ
26. zip(v5;v7) = votes-from-inning(v3 - 1;ys) ∈ (({b:Id| (b ∈ A)}  × V) List)
27. 0 ≤ v3
28. 1 ≤ v3 supposing ¬↑null(ys)
29. ||values-for-distinct(IdDeq;votes-from-inning(v3 - 1;ys))|| ≤ (2 * t)
⊢ ((2 * t) + 1) ≤ ||remove-repeats(IdDeq;map(λp.(fst(p));votes-from-inning((v3 + 1) - 2;ys @ [Vote[y2;y4;y5]])))||

---

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.  v1  :  \mBbbB{}@i
12.  v3  :  \mBbbZ{}@i
13.  v5  :  \{a:Id|  (a  \mmember{}  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>@i
17.  (v3  -  1)  \mleq{}  y4
18.  y4  \mleq{}  (v3  -  1)
19.  ||remove-repeats(IdDeq;v5  @  [y2])||  =  ((2  *  t)  +  1)
20.  (((2  *  t)  +  1)  \mleq{}  ||remove-repeats(IdDeq;map(\mlambda{}p.(fst(p));votes-from-inning(v3 
                                                                                                -  2;ys)))||)  supposing 
              ((votes-from-inning(v3  -  1;ys)  =  [])  and 
              1  <  v3)@i
21.  1  <  v3  +  1
22.  votes-from-inning((v3  +  1)  -  1;ys)  =  []
23.  votes-from-inning((v3  +  1)  -  1;[Vote[y2;y4;y5]])  =  []
\mvdash{}  ((2  *  t)  +  1)  \mleq{}  ||remove-repeats(IdDeq;map(\mlambda{}p.(fst(p));votes-from-inning((v3  +  1)  -  2;ys
                                                                                          @  [Vote[y2;y4;y5]])))||


By

((InstLemma  `consensus-accum-num-property1`  [\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}v0\mkleeneclose{};\mkleeneopen{}ys\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  At  \mkleeneopen{}Type\mkleeneclose{}  (HypSubst'  16  -1)\mcdot{}
  THEN  (Reduce  (-1)  THEN  Auto)\mcdot{})

---

Home Index