---

Step * of Lemma archive-condition-innings

∀[V:Type]. ∀[A:Id List]. ∀[t:ℕ+]. ∀[f:(V List) ─→ V]. ∀[L1,L2:consensus-rcv(V;A) List]. ∀[n1,n2:ℤ]. ∀[v1,v2:V].
  (n1 < n2) supposing (archive-condition(V;A;t;f;n2;v2;L2) and L1 < L2 and archive-condition(V;A;t;f;n1;v1;L1))
BY
{ (Auto THEN D -1 THEN ExRepD THEN SplitOrHyps) }

1
1. V : Type
2. A : Id List
3. t : ℕ+
4. f : (V List) ─→ V
5. L1 : consensus-rcv(V;A) List
6. L2 : consensus-rcv(V;A) List
7. n1 : ℤ
8. n2 : ℤ
9. v1 : V
10. v2 : V
11. archive-condition(V;A;t;f;n1;v1;L1)
12. L1 < L2
13. L' : consensus-rcv(V;A) List
14. r : consensus-rcv(V;A)
15. L2 = (L' @ [r]) ∈ (consensus-rcv(V;A) List)
16. (L' = [] ∈ (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)))))
⊢ n1 < n2

2
1. V : Type
2. A : Id List
3. t : ℕ+
4. f : (V List) ─→ V
5. L1 : consensus-rcv(V;A) List
6. L2 : consensus-rcv(V;A) List
7. n1 : ℤ
8. n2 : ℤ
9. v1 : V
10. v2 : V
11. archive-condition(V;A;t;f;n1;v1;L1)
12. L1 < L2
13. L' : consensus-rcv(V;A) List
14. r : consensus-rcv(V;A)
15. L2 = (L' @ [r]) ∈ (consensus-rcv(V;A) List)
16. (0 < n2
∧ (||values-for-distinct(IdDeq;votes-from-inning(n2 - 1;L'))|| ≤ (2 * t))
∧ (↑null(filter(λr.n2 - 1 <z inning(r);L'))))
∧ ((∃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;L2))||)
    ∧ ((f values-for-distinct(IdDeq;votes-from-inning(n2 - 1;L2))) = v2 ∈ V)))
⊢ n1 < n2

---

Latex:


\mforall{}[V:Type].  \mforall{}[A:Id  List].  \mforall{}[t:\mBbbN{}\msupplus{}].  \mforall{}[f:(V  List)  {}\mrightarrow{}  V].  \mforall{}[L1,L2:consensus-rcv(V;A)  List].  \mforall{}[n1,n2:\mBbbZ{}].
\mforall{}[v1,v2:V].
    (n1  <  n2)  supposing 
          (archive-condition(V;A;t;f;n2;v2;L2)  and 
          L1  <  L2  and 
          archive-condition(V;A;t;f;n1;v1;L1))


By

(Auto  THEN  D  -1  THEN  ExRepD  THEN  SplitOrHyps)

---

Home Index