---

Step * 1 of Lemma consensus-accum-num-property1


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. (v3 - 1) ≤ y4
17. y4 ≤ (v3 - 1)
18. ¬(||remove-repeats(IdDeq;v5 @ [y2])|| = ((2 * t) + 1) ∈ ℤ)
19. filter(λr.v3 - 1 <z inning(r);ys) = [] ∈ (consensus-rcv(V;A) List)@i
20. ||v5|| = ||v7|| ∈ ℤ@i
21. zip(v5;v7) = votes-from-inning(v3 - 1;ys) ∈ (({b:Id| (b ∈ A)}  × V) List)@i
22. 0 ≤ v3@i
23. 1 ≤ v3 supposing ¬↑null(ys)@i
24. ||values-for-distinct(IdDeq;votes-from-inning(v3 - 1;ys))|| ≤ (2 * t)@i
25. filter(λr.v3 - 1 <z inning(r);ys @ [Vote[y2;y4;y5]]) = [] ∈ (consensus-rcv(V;A) List)
26. ||v5 @ [y2]|| = ||v7 @ [y5]|| ∈ ℤ
⊢ zip(v5 @ [y2];v7 @ [y5])
= (votes-from-inning(v3 - 1;ys) @ votes-from-inning(v3 - 1;[Vote[y2;y4;y5]]))
∈ (({b:Id| (b ∈ A)}  × V) List)
BY
{ ((RWO "length-append" (-1) THENM Reduce (-1) THENM RWO "zip-append" 0 THENM Reduce 0)
   THEN Auto
   THEN EqCD
   THEN Auto
   THEN RepUR ``votes-from-inning mapfilter rcvd-inning-eq rcv-vote? cs-initial-rcv cs-rcv-vote rcvd-vote`` 0
   THEN Try (SplitOnConclITE)
   THEN Reduce 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.  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.  (v3  -  1)  \mleq{}  y4
17.  y4  \mleq{}  (v3  -  1)
18.  \mneg{}(||remove-repeats(IdDeq;v5  @  [y2])||  =  ((2  *  t)  +  1))
19.  filter(\mlambda{}r.v3  -  1  <z  inning(r);ys)  =  []@i
20.  ||v5||  =  ||v7||@i
21.  zip(v5;v7)  =  votes-from-inning(v3  -  1;ys)@i
22.  0  \mleq{}  v3@i
23.  1  \mleq{}  v3  supposing  \mneg{}\muparrow{}null(ys)@i
24.  ||values-for-distinct(IdDeq;votes-from-inning(v3  -  1;ys))||  \mleq{}  (2  *  t)@i
25.  filter(\mlambda{}r.v3  -  1  <z  inning(r);ys  @  [Vote[y2;y4;y5]])  =  []
26.  ||v5  @  [y2]||  =  ||v7  @  [y5]||
\mvdash{}  zip(v5  @  [y2];v7  @  [y5])
=  (votes-from-inning(v3  -  1;ys)  @  votes-from-inning(v3  -  1;[Vote[y2;y4;y5]]))


By


((RWO  "length-append"  (-1)  THENM  Reduce  (-1)  THENM  RWO  "zip-append"  0  THENM  Reduce  0)
  THEN  Auto
  THEN  EqCD
  THEN  Auto
  THEN  ...
  THEN  Try  (SplitOnConclITE)
  THEN  Reduce  0
  THEN  Auto)\mcdot{}

---

Home Index