---

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:


\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

((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