---

Step * 1 1 2 of Lemma archive-condition-one-one


1. V : Type
2. A : Id List
3. IdDeq ∈ EqDecider({b:Id| (b ∈ A)} )
4. t : ℕ+
5. f : (V List) ─→ V
6. L : consensus-rcv(V;A) List
7. n1 : ℤ
8. n2 : ℤ
9. v1 : V
10. v2 : V
11. [] = [] ∈ (consensus-rcv(V;A) List)
12. 0 ≤ n1
13. a : {a:Id| (a ∈ A)} 
14. 0 < n2
15. ||values-for-distinct(IdDeq;votes-from-inning(n2 - 1;[]))|| ≤ (2 * t)
16. True
17. ((2 * t) + 1) ≤ ||values-for-distinct(IdDeq;votes-from-inning(n2 - 1;[Vote[a;n1;v1]]))||
18. (f values-for-distinct(IdDeq;votes-from-inning(n2 - 1;[Vote[a;n1;v1]]))) = v2 ∈ V
⊢ (n1 = n2 ∈ ℤ) ∧ (v1 = v2 ∈ V)
BY
{ (RepUR ``values-for-distinct`` -2
   THEN (RWO "length-map" (-2) THENA Auto)
   THEN RepUR ``votes-from-inning mapfilter`` -2
   THEN (SplitOnHypITE -2  THENA Auto)
   THEN Reduce (-3)
   THEN Auto')⋅ }

---

Latex:



1.  V  :  Type
2.  A  :  Id  List
3.  IdDeq  \mmember{}  EqDecider(\{b:Id|  (b  \mmember{}  A)\}  )
4.  t  :  \mBbbN{}\msupplus{}
5.  f  :  (V  List)  {}\mrightarrow{}  V
6.  L  :  consensus-rcv(V;A)  List
7.  n1  :  \mBbbZ{}
8.  n2  :  \mBbbZ{}
9.  v1  :  V
10.  v2  :  V
11.  []  =  []
12.  0  \mleq{}  n1
13.  a  :  \{a:Id|  (a  \mmember{}  A)\} 
14.  0  <  n2
15.  ||values-for-distinct(IdDeq;votes-from-inning(n2  -  1;[]))||  \mleq{}  (2  *  t)
16.  True
17.  ((2  *  t)  +  1)  \mleq{}  ||values-for-distinct(IdDeq;votes-from-inning(n2  -  1;[Vote[a;n1;v1]]))||
18.  (f  values-for-distinct(IdDeq;votes-from-inning(n2  -  1;[Vote[a;n1;v1]])))  =  v2
\mvdash{}  (n1  =  n2)  \mwedge{}  (v1  =  v2)


By

(RepUR  ``values-for-distinct``  -2
  THEN  (RWO  "length-map"  (-2)  THENA  Auto)
  THEN  RepUR  ``votes-from-inning  mapfilter``  -2
  THEN  (SplitOnHypITE  -2    THENA  Auto)
  THEN  Reduce  (-3)
  THEN  Auto')\mcdot{}

---

Home Index