---

Step * of Lemma archive-condition-one-one

∀[V:Type]. ∀[A:Id List]. ∀[t:ℕ+]. ∀[f:(V List) ⟶ V]. ∀[L:consensus-rcv(V;A) List]. ∀[n1,n2:ℤ]. ∀[v1,v2:V].
  ({(n1 = n2 ∈ ℤ) ∧ (v1 = v2 ∈ V)}) supposing 
     (archive-condition(V;A;t;f;n2;v2;L) and 
     archive-condition(V;A;t;f;n1;v1;L))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN (Assert IdDeq ∈ EqDecider({b:Id| (b ∈ A)} ) BY
               Auto)
   THEN (Auto THEN D -2 THEN ExRepD)
   THEN RenameVar `L1' (-5)
   THEN HypSubst' (-3) (-1)
   THEN (D -1 THEN ExRepD)
   THEN RenameVar `r2' (-3)
   THEN RenameVar `L2' (-4)
   THEN AutoSimpHyp Auto (-2)
   THEN (RevHypSubst' (-4) (-1) THENA Auto)
   THEN ThinVar `L2'
   THEN (RevHypSubst' (-3) (-1) THENA Auto)
   THEN ThinVar `r2'
   THEN Thin (-2)) }

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))
∧ (((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)

---

Latex:

---

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


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (Assert  IdDeq  \mmember{}  EqDecider(\{b:Id|  (b  \mmember{}  A)\}  )  BY
                          Auto)
  THEN  (Auto  THEN  D  -2  THEN  ExRepD)
  THEN  RenameVar  `L1'  (-5)
  THEN  HypSubst'  (-3)  (-1)
  THEN  (D  -1  THEN  ExRepD)
  THEN  RenameVar  `r2'  (-3)
  THEN  RenameVar  `L2'  (-4)
  THEN  AutoSimpHyp  Auto  (-2)
  THEN  (RevHypSubst'  (-4)  (-1)  THENA  Auto)
  THEN  ThinVar  `L2'
  THEN  (RevHypSubst'  (-3)  (-1)  THENA  Auto)
  THEN  ThinVar  `r2'
  THEN  Thin  (-2))

---

Home Index