---

Step * 2 4 1 of Lemma archive-consensus-accum-num

.....assertion..... 
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
⊢ y4 = (i - 1) ∈ ℤ
BY
{ (SupposeNot
   THEN OnMaybeHyp 39 (\h. (RepUR ``votes-from-inning`` h
                            THEN (RWO "mapfilter-append" h THENA Auto)
                            THEN Fold `votes-from-inning` h
                            THEN Subst' votes-from-inning(i - 1;[Vote[y2;y4;y5]]) ~ [] h
                            THEN Try ((RWO "append-nil" h THEN Auto))
                            THEN RepUR ``votes-from-inning cs-rcv-vote  rcvd-inning-eq rcv-vote? rcvd-vote mapfilter`` 0
                            THEN SplitOnConclITE
                            THEN Reduce 0
                            THEN Auto))
   ) }

---

Latex:


.....assertion..... 
1.  V  :  Type
2.  A  :  Id  List
3.  t  :  \mBbbN{}\msupplus{}
4.  f  :  (V  List)  {}\mrightarrow{}  V
5.  v0  :  V
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.  Vote[y2;y4;y5]  \mmember{}  consensus-rcv(V;A)
12.  v1  :  \mBbbB{}@i
13.  v3  :  \mBbbZ{}@i
14.  v5  :  \{a:Id|  (a  \mmember{}  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>@i
18.  (((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
19.  (v3  -  1)  \mleq{}  y4
20.  y4  \mleq{}  (v3  -  1)
21.  \mneg{}(||remove-repeats(IdDeq;v5  @  [y2])||  =  ((2  *  t)  +  1))
22.  \mforall{}[v@0:V].  \mforall{}[i:\mBbbZ{}].    \muparrow{}v1  supposing  archive-condition(V;A;t;f;i;v@0;ys)@i
23.  filter(\mlambda{}r.v3  -  1  <z  inning(r);ys)  =  []@i
24.  ||v5||  =  ||v7||@i
25.  zip(v5;v7)  =  votes-from-inning(v3  -  1;ys)@i
26.  0  \mleq{}  v3@i
27.  1  \mleq{}  v3  supposing  \mneg{}\muparrow{}null(ys)@i
28.  ||values-for-distinct(IdDeq;votes-from-inning(v3  -  1;ys))||  \mleq{}  (2  *  t)@i
29.  filter(\mlambda{}r.v3  -  1  <z  inning(r);ys  @  [Vote[y2;y4;y5]])  =  []@i
30.  ||v5  @  [y2]||  =  ||v7  @  [y5]||@i
31.  zip(v5  @  [y2];v7  @  [y5])  =  votes-from-inning(v3  -  1;ys  @  [Vote[y2;y4;y5]])@i
32.  0  \mleq{}  v3@i
33.  1  \mleq{}  v3  supposing  \mneg{}\muparrow{}null(ys  @  [Vote[y2;y4;y5]])@i
34.  ||values-for-distinct(IdDeq;votes-from-inning(v3  -  1;ys  @  [Vote[y2;y4;y5]]))||  \mleq{}  (2  *  t)@i
35.  v@0  :  V
36.  i  :  \mBbbZ{}
37.  0  <  i
38.  ||values-for-distinct(IdDeq;votes-from-inning(i  -  1;ys))||  \mleq{}  (2  *  t)
39.  \muparrow{}null(filter(\mlambda{}r.i  -  1  <z  inning(r);ys))
40.  ((2  *  t)  +  1)  \mleq{}  ||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
\mvdash{}  y4  =  (i  -  1)


By

(SupposeNot
  THEN  OnMaybeHyp  39  (\mbackslash{}h.
            (RepUR  ``votes-from-inning``  h
              THEN  (RWO  "mapfilter-append"  h  THENA  Auto)
              THEN  Fold  `votes-from-inning`  h
              THEN  Subst'  votes-from-inning(i  -  1;[Vote[y2;y4;y5]])  \msim{}  []  h
              THEN  Try  ((RWO  "append-nil"  h  THEN  Auto))
              THEN  RepUR  ``votes-from-inning  cs-rcv-vote    rcvd-inning-eq  rcv-vote?  rcvd-vote  mapfilter``  0
              THEN  SplitOnConclITE
              THEN  Reduce  0
              THEN  Auto))
  )

---

Home Index