---

Step * 1 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. 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]])))||
BY
{ (Unfold `votes-from-inning` 0
   THEN ((RWO "mapfilter-append" 0 THENA Auto)
         THEN Fold `votes-from-inning` 0
         THEN (RWO "map_append_sq" 0 THENA Auto)
         THEN (RWO "remove-repeats-append-sq" 0 THENA Auto)
         THEN RWO "length-append" 0
         THEN Auto')
   )⋅ }

---

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.  x  :  V@i
9.  v1  :  \mBbbB{}@i
10.  v3  :  \mBbbZ{}@i
11.  v5  :  \{a:Id|  (a  \mmember{}  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>@i
15.  \mneg{}(v3  =  0)
16.  1  <  v3
17.  votes-from-inning(v3  -  1;ys)  =  []
18.  votes-from-inning(v3  -  1;[Init[x]])  =  []
19.  ((2  *  t)  +  1)  \mleq{}  ||remove-repeats(IdDeq;map(\mlambda{}p.(fst(p));votes-from-inning(v3  -  2;ys)))||
\mvdash{}  ((2  *  t)  +  1)  \mleq{}  ||remove-repeats(IdDeq;map(\mlambda{}p.(fst(p));votes-from-inning(v3  -  2;ys
                                                                                          @  [Init[x]])))||


By

(Unfold  `votes-from-inning`  0
  THEN  ((RWO  "mapfilter-append"  0  THENA  Auto)
              THEN  Fold  `votes-from-inning`  0
              THEN  (RWO  "map\_append\_sq"  0  THENA  Auto)
              THEN  (RWO  "remove-repeats-append-sq"  0  THENA  Auto)
              THEN  RWO  "length-append"  0
              THEN  Auto')
  )\mcdot{}

---

Home Index