---

Step * 1 2 2 3 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. L1 : consensus-rcv(V;A) List
12. 0 < n1
13. ||values-for-distinct(IdDeq;votes-from-inning(n1 - 1;L1))|| ≤ (2 * t)
14. ↑null(filter(λr.n1 - 1 <z inning(r);L1))
15. ((2 * t) + 1) ≤ ||values-for-distinct(IdDeq;votes-from-inning(n1 - 1;L))||
16. (f values-for-distinct(IdDeq;votes-from-inning(n1 - 1;L))) = v1 ∈ V
17. a : {a:Id| (a ∈ A)} 
18. v : V
19. ¬↑null(filter(λr.n1 - 1 - 1 <z inning(r);L1))
20. 0 ≤ (n1 - 1)
21. 0 < n2
22. ||values-for-distinct(IdDeq;votes-from-inning(n2 - 1;L1))|| ≤ (2 * t)
23. ↑null(filter(λr.n2 - 1 <z inning(r);L1))
24. a@0 : {a:Id| (a ∈ A)} 
25. Vote[a;n1 - 1;v] = Vote[a@0;n2;v2] ∈ consensus-rcv(V;A)
26. L = (L1 @ [Vote[a;n1 - 1;v]]) ∈ (consensus-rcv(V;A) List)
⊢ (n1 = n2 ∈ ℤ) ∧ (v1 = v2 ∈ V)
BY
{ AllHyps h.(Progress
             (Unfold `consensus-rcv` h)⋅
             THEN Progress
             (RepUR ``cs-initial-rcv cs-rcv-vote`` h)⋅
             THEN MoveToHyp 0 h
             THEN RepeatFor 3 (AutoSimpHyp Auto (-1))
             THEN Try (Complete (Auto))) ⋅ }

1
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. L1 : consensus-rcv(V;A) List
12. 0 < n1
13. ||values-for-distinct(IdDeq;votes-from-inning(n1 - 1;L1))|| ≤ (2 * t)
14. ↑null(filter(λr.n1 - 1 <z inning(r);L1))
15. ((2 * t) + 1) ≤ ||values-for-distinct(IdDeq;votes-from-inning(n1 - 1;L))||
16. (f values-for-distinct(IdDeq;votes-from-inning(n1 - 1;L))) = v1 ∈ V
17. a : {a:Id| (a ∈ A)} 
18. v : V
19. ¬↑null(filter(λr.n1 - 1 - 1 <z inning(r);L1))
20. 0 ≤ (n1 - 1)
21. 0 < n2
22. ||values-for-distinct(IdDeq;votes-from-inning(n2 - 1;L1))|| ≤ (2 * t)
23. ↑null(filter(λr.n2 - 1 <z inning(r);L1))
24. a@0 : {a:Id| (a ∈ A)} 
25. L = (L1 @ [inr <a, n1 - 1, v> ]) ∈ ((V + ({b:Id| (b ∈ A)}  × ℕ × V)) List)
26. (inr <a, n1 - 1, v> ) = (inr <a@0, n2, v2> ) ∈ (V + ({b:Id| (b ∈ A)}  × ℕ × V))
27. a = a@0 ∈ {b:Id| (b ∈ A)} 
28. (n1 - 1) = n2 ∈ ℕ
29. v = v2 ∈ V
⊢ (n1 = n2 ∈ ℤ) ∧ (v1 = v2 ∈ V)

---

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.  L1  :  consensus-rcv(V;A)  List
12.  0  <  n1
13.  ||values-for-distinct(IdDeq;votes-from-inning(n1  -  1;L1))||  \mleq{}  (2  *  t)
14.  \muparrow{}null(filter(\mlambda{}r.n1  -  1  <z  inning(r);L1))
15.  ((2  *  t)  +  1)  \mleq{}  ||values-for-distinct(IdDeq;votes-from-inning(n1  -  1;L))||
16.  (f  values-for-distinct(IdDeq;votes-from-inning(n1  -  1;L)))  =  v1
17.  a  :  \{a:Id|  (a  \mmember{}  A)\} 
18.  v  :  V
19.  \mneg{}\muparrow{}null(filter(\mlambda{}r.n1  -  1  -  1  <z  inning(r);L1))
20.  0  \mleq{}  (n1  -  1)
21.  0  <  n2
22.  ||values-for-distinct(IdDeq;votes-from-inning(n2  -  1;L1))||  \mleq{}  (2  *  t)
23.  \muparrow{}null(filter(\mlambda{}r.n2  -  1  <z  inning(r);L1))
24.  a@0  :  \{a:Id|  (a  \mmember{}  A)\} 
25.  Vote[a;n1  -  1;v]  =  Vote[a@0;n2;v2]
26.  L  =  (L1  @  [Vote[a;n1  -  1;v]])
\mvdash{}  (n1  =  n2)  \mwedge{}  (v1  =  v2)


By

AllHyps  h.(Progress
                      (Unfold  `consensus-rcv`  h)\mcdot{}
                      THEN  Progress
                      (RepUR  ``cs-initial-rcv  cs-rcv-vote``  h)\mcdot{}
                      THEN  MoveToHyp  0  h
                      THEN  RepeatFor  3  (AutoSimpHyp  Auto  (-1))
                      THEN  Try  (Complete  (Auto)))  \mcdot{}

---

Home Index