---

Step * 1 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. r : consensus-rcv(V;A)
13. L = (L1 @ [r]) ∈ (consensus-rcv(V;A) List)
14. ((L1 = [] ∈ (consensus-rcv(V;A) List))
∧ (((r = Init[v1] ∈ consensus-rcv(V;A)) ∧ (n1 = 0 ∈ ℤ))
  ∨ ((0 ≤ n1) ∧ (∃a:{a:Id| (a ∈ A)} . (r = Vote[a;n1;v1] ∈ consensus-rcv(V;A))))))
∨ ((0 < n1
  ∧ (||values-for-distinct(IdDeq;votes-from-inning(n1 - 1;L1))|| ≤ (2 * t))
  ∧ (↑null(filter(λr.n1 - 1 <z inning(r);L1))))
  ∧ ((∃a:{a:Id| (a ∈ A)} . (r = Vote[a;n1;v1] ∈ consensus-rcv(V;A)))
    ∨ ((((2 * t) + 1) ≤ ||values-for-distinct(IdDeq;votes-from-inning(n1 - 1;L))||)
      ∧ ((f values-for-distinct(IdDeq;votes-from-inning(n1 - 1;L))) = v1 ∈ V))))
15. ((L1 = [] ∈ (consensus-rcv(V;A) List))
∧ (((r = Init[v2] ∈ consensus-rcv(V;A)) ∧ (n2 = 0 ∈ ℤ))
  ∨ ((0 ≤ n2) ∧ (∃a:{a:Id| (a ∈ A)} . (r = Vote[a;n2;v2] ∈ consensus-rcv(V;A))))))
∨ ((0 < n2
  ∧ (||values-for-distinct(IdDeq;votes-from-inning(n2 - 1;L1))|| ≤ (2 * t))
  ∧ (↑null(filter(λr.n2 - 1 <z inning(r);L1))))
  ∧ ((∃a:{a:Id| (a ∈ A)} . (r = Vote[a;n2;v2] ∈ consensus-rcv(V;A)))
    ∨ ((((2 * t) + 1) ≤ ||values-for-distinct(IdDeq;votes-from-inning(n2 - 1;L1 @ [r]))||)
      ∧ ((f values-for-distinct(IdDeq;votes-from-inning(n2 - 1;L1 @ [r]))) = v2 ∈ V))))
⊢ (n1 = n2 ∈ ℤ) ∧ (v1 = v2 ∈ V)
BY
{ (FoldTop `guard` 0 THEN D -2 THEN 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. r : consensus-rcv(V;A)
13. L = (L1 @ [r]) ∈ (consensus-rcv(V;A) List)
14. L1 = [] ∈ (consensus-rcv(V;A) List)
15. ((r = Init[v1] ∈ consensus-rcv(V;A)) ∧ (n1 = 0 ∈ ℤ))
∨ ((0 ≤ n1) ∧ (∃a:{a:Id| (a ∈ A)} . (r = Vote[a;n1;v1] ∈ consensus-rcv(V;A))))
16. ((L1 = [] ∈ (consensus-rcv(V;A) List))
∧ (((r = Init[v2] ∈ consensus-rcv(V;A)) ∧ (n2 = 0 ∈ ℤ))
  ∨ ((0 ≤ n2) ∧ (∃a:{a:Id| (a ∈ A)} . (r = Vote[a;n2;v2] ∈ consensus-rcv(V;A))))))
∨ ((0 < n2
  ∧ (||values-for-distinct(IdDeq;votes-from-inning(n2 - 1;L1))|| ≤ (2 * t))
  ∧ (↑null(filter(λr.n2 - 1 <z inning(r);L1))))
  ∧ ((∃a:{a:Id| (a ∈ A)} . (r = Vote[a;n2;v2] ∈ consensus-rcv(V;A)))
    ∨ ((((2 * t) + 1) ≤ ||values-for-distinct(IdDeq;votes-from-inning(n2 - 1;L1 @ [r]))||)
      ∧ ((f values-for-distinct(IdDeq;votes-from-inning(n2 - 1;L1 @ [r]))) = v2 ∈ V))))
⊢ {(n1 = n2 ∈ ℤ) ∧ (v1 = v2 ∈ V)}

2
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. r : consensus-rcv(V;A)
13. L = (L1 @ [r]) ∈ (consensus-rcv(V;A) List)
14. 0 < n1
15. ||values-for-distinct(IdDeq;votes-from-inning(n1 - 1;L1))|| ≤ (2 * t)
16. ↑null(filter(λr.n1 - 1 <z inning(r);L1))
17. (∃a:{a:Id| (a ∈ A)} . (r = Vote[a;n1;v1] ∈ consensus-rcv(V;A)))
∨ ((((2 * t) + 1) ≤ ||values-for-distinct(IdDeq;votes-from-inning(n1 - 1;L))||)
  ∧ ((f values-for-distinct(IdDeq;votes-from-inning(n1 - 1;L))) = v1 ∈ V))
18. ((L1 = [] ∈ (consensus-rcv(V;A) List))
∧ (((r = Init[v2] ∈ consensus-rcv(V;A)) ∧ (n2 = 0 ∈ ℤ))
  ∨ ((0 ≤ n2) ∧ (∃a:{a:Id| (a ∈ A)} . (r = Vote[a;n2;v2] ∈ consensus-rcv(V;A))))))
∨ ((0 < n2
  ∧ (||values-for-distinct(IdDeq;votes-from-inning(n2 - 1;L1))|| ≤ (2 * t))
  ∧ (↑null(filter(λr.n2 - 1 <z inning(r);L1))))
  ∧ ((∃a:{a:Id| (a ∈ A)} . (r = Vote[a;n2;v2] ∈ consensus-rcv(V;A)))
    ∨ ((((2 * t) + 1) ≤ ||values-for-distinct(IdDeq;votes-from-inning(n2 - 1;L1 @ [r]))||)
      ∧ ((f values-for-distinct(IdDeq;votes-from-inning(n2 - 1;L1 @ [r]))) = 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.  r  :  consensus-rcv(V;A)
13.  L  =  (L1  @  [r])
14.  ((L1  =  [])
\mwedge{}  (((r  =  Init[v1])  \mwedge{}  (n1  =  0))  \mvee{}  ((0  \mleq{}  n1)  \mwedge{}  (\mexists{}a:\{a:Id|  (a  \mmember{}  A)\}  .  (r  =  Vote[a;n1;v1])))))
\mvee{}  ((0  <  n1
    \mwedge{}  (||values-for-distinct(IdDeq;votes-from-inning(n1  -  1;L1))||  \mleq{}  (2  *  t))
    \mwedge{}  (\muparrow{}null(filter(\mlambda{}r.n1  -  1  <z  inning(r);L1))))
    \mwedge{}  ((\mexists{}a:\{a:Id|  (a  \mmember{}  A)\}  .  (r  =  Vote[a;n1;v1]))
        \mvee{}  ((((2  *  t)  +  1)  \mleq{}  ||values-for-distinct(IdDeq;votes-from-inning(n1  -  1;L))||)
            \mwedge{}  ((f  values-for-distinct(IdDeq;votes-from-inning(n1  -  1;L)))  =  v1))))
15.  ((L1  =  [])
\mwedge{}  (((r  =  Init[v2])  \mwedge{}  (n2  =  0))  \mvee{}  ((0  \mleq{}  n2)  \mwedge{}  (\mexists{}a:\{a:Id|  (a  \mmember{}  A)\}  .  (r  =  Vote[a;n2;v2])))))
\mvee{}  ((0  <  n2
    \mwedge{}  (||values-for-distinct(IdDeq;votes-from-inning(n2  -  1;L1))||  \mleq{}  (2  *  t))
    \mwedge{}  (\muparrow{}null(filter(\mlambda{}r.n2  -  1  <z  inning(r);L1))))
    \mwedge{}  ((\mexists{}a:\{a:Id|  (a  \mmember{}  A)\}  .  (r  =  Vote[a;n2;v2]))
        \mvee{}  ((((2  *  t)  +  1)  \mleq{}  ||values-for-distinct(IdDeq;votes-from-inning(n2  -  1;L1  @  [r]))||)
            \mwedge{}  ((f  values-for-distinct(IdDeq;votes-from-inning(n2  -  1;L1  @  [r])))  =  v2))))
\mvdash{}  (n1  =  n2)  \mwedge{}  (v1  =  v2)


By

(FoldTop  `guard`  0  THEN  D  -2  THEN  Auto)

---

Home Index