---

Step * 1 of Lemma consensus-rcv-crosses-size


1. V : Type
2. A : Id List
3. t : ℕ+
4. n : ℤ
5. L : consensus-rcv(V;A) List
6. r : consensus-rcv(V;A)
7. ||remove-repeats(IdDeq;map(λp.(fst(p));votes-from-inning(n;L)))|| ≤ (2 * t)
8. ((2 * t) + 1) ≤ ||remove-repeats(IdDeq;map(λp.(fst(p));votes-from-inning(n;L))
   @ map(λp.(fst(p));votes-from-inning(n;[r])))||
⊢ ||remove-repeats(IdDeq;map(λp.(fst(p));votes-from-inning(n;L)) @ map(λp.(fst(p));votes-from-inning(n;[r])))||
= ((2 * t) + 1)
∈ ℤ
BY
{ ((RepeatFor 2 (MoveToConcl (-1)) THEN (GenConclAtAddrType ⌈{b:Id| (b ∈ A)}  List⌉ [1;1;1;2]⋅ THENA Auto))
   THEN RepUR ``votes-from-inning mapfilter rcvd-inning-eq rcv-vote? rcvd-vote`` 0
   THEN (D -3 THEN Try (RepeatFor 2 (D -3)))
   THEN Reduce 0
   THEN Try ((RWO "append-nil" 0 THEN Auto))
   THEN (SplitOnConclITE THEN Reduce 0 THEN Try ((RWO "append-nil" 0 THEN Auto)))
   THEN Auto) }

1
1. V : Type
2. A : Id List
3. t : ℕ+
4. n : ℤ
5. L : consensus-rcv(V;A) List
6. y1 : {b:Id| (b ∈ A)} 
7. y3 : ℕ
8. y4 : V
9. v : {b:Id| (b ∈ A)}  List@i
10. map(λp.(fst(p));votes-from-inning(n;L)) = v ∈ ({b:Id| (b ∈ A)}  List)@i
11. n = y3 ∈ ℤ
12. ||remove-repeats(IdDeq;v)|| ≤ (2 * t)@i
13. ((2 * t) + 1) ≤ ||remove-repeats(IdDeq;v @ [y1])||@i
⊢ ||remove-repeats(IdDeq;v @ [y1])|| = ((2 * t) + 1) ∈ ℤ

---

Latex:



1.  V  :  Type
2.  A  :  Id  List
3.  t  :  \mBbbN{}\msupplus{}
4.  n  :  \mBbbZ{}
5.  L  :  consensus-rcv(V;A)  List
6.  r  :  consensus-rcv(V;A)
7.  ||remove-repeats(IdDeq;map(\mlambda{}p.(fst(p));votes-from-inning(n;L)))||  \mleq{}  (2  *  t)
8.  ((2  *  t)  +  1)  \mleq{}  ||remove-repeats(IdDeq;map(\mlambda{}p.(fst(p));votes-from-inning(n;L))
      @  map(\mlambda{}p.(fst(p));votes-from-inning(n;[r])))||
\mvdash{}  ||remove-repeats(IdDeq;map(\mlambda{}p.(fst(p));votes-from-inning(n;L))
@  map(\mlambda{}p.(fst(p));votes-from-inning(n;[r])))||
=  ((2  *  t)  +  1)


By

((RepeatFor  2  (MoveToConcl  (-1))
    THEN  (GenConclAtAddrType  \mkleeneopen{}\{b:Id|  (b  \mmember{}  A)\}    List\mkleeneclose{}  [1;1;1;2]\mcdot{}  THENA  Auto)
    )
  THEN  RepUR  ``votes-from-inning  mapfilter  rcvd-inning-eq  rcv-vote?  rcvd-vote``  0
  THEN  (D  -3  THEN  Try  (RepeatFor  2  (D  -3)))
  THEN  Reduce  0
  THEN  Try  ((RWO  "append-nil"  0  THEN  Auto))
  THEN  (SplitOnConclITE  THEN  Reduce  0  THEN  Try  ((RWO  "append-nil"  0  THEN  Auto)))
  THEN  Auto)

---

Home Index