---

Step * 1 1 1 of Lemma decidable__archive-condition


1. [V] : Type
2. v0 : V@i
3. A : Id List@i
4. t : ℕ+@i
5. f : (V List) ─→ V@i
6. L : consensus-rcv(V;A) List@i
7. v1 : 𝔹@i
8. v3 : ℤ@i
9. v5 : {a:Id| (a ∈ A)}  List@i
10. v7 : V List@i
11. v8 : V@i
12. consensus-accum-num-state(t;f;v0;L) = <v1, v3, v5, v7, v8> ∈ (𝔹 × ℤ × {a:Id| (a ∈ A)}  List × V List × V)@i
13. ∀n:ℕ. ∀v@0:V.  (archive-condition(V;A;t;f;n;v@0;L) ⇐⇒ (↑v1) ∧ ((n + 1) = v3 ∈ ℤ) ∧ (v@0 = v8 ∈ V))@i
14. let b,i,as,vs,v = consensus-accum-num-state(t;f;v0;L) in (filter(λr.i - 1 <z inning(r);L)
                                                             = []
                                                             ∈ (consensus-rcv(V;A) List))
∧ (||as|| = ||vs|| ∈ ℤ)
∧ (zip(as;vs) = votes-from-inning(i - 1;L) ∈ (({b:Id| (b ∈ A)}  × V) List))
∧ (0 ≤ i)
∧ 1 ≤ i supposing ¬↑null(L)
∧ (||values-for-distinct(IdDeq;votes-from-inning(i - 1;L))|| ≤ (2 * t))
⊢ (¬↑null(L)) ⇒ (1 ≤ v3)
BY
{ At ⌈Type⌉ (HypSubst' (-3) (-1))⋅ }

1
.....wf..... 
1. V : Type
2. v0 : V@i
3. A : Id List@i
4. t : ℕ+@i
5. f : (V List) ─→ V@i
6. L : consensus-rcv(V;A) List@i
7. v1 : 𝔹@i
8. v3 : ℤ@i
9. v5 : {a:Id| (a ∈ A)}  List@i
10. v7 : V List@i
11. v8 : V@i
12. consensus-accum-num-state(t;f;v0;L) = <v1, v3, v5, v7, v8> ∈ (𝔹 × ℤ × {a:Id| (a ∈ A)}  List × V List × V)@i
13. ∀n:ℕ. ∀v@0:V.  (archive-condition(V;A;t;f;n;v@0;L) ⇐⇒ (↑v1) ∧ ((n + 1) = v3 ∈ ℤ) ∧ (v@0 = v8 ∈ V))@i
14. let b,i,as,vs,v = consensus-accum-num-state(t;f;v0;L) in (filter(λr.i - 1 <z inning(r);L)
                                                             = []
                                                             ∈ (consensus-rcv(V;A) List))
∧ (||as|| = ||vs|| ∈ ℤ)
∧ (zip(as;vs) = votes-from-inning(i - 1;L) ∈ (({b:Id| (b ∈ A)}  × V) List))
∧ (0 ≤ i)
∧ 1 ≤ i supposing ¬↑null(L)
∧ (||values-for-distinct(IdDeq;votes-from-inning(i - 1;L))|| ≤ (2 * t))
15. z : 𝔹 × ℤ × {a:Id| (a ∈ A)}  List × V List × V
⊢ let b,i,as,vs,v = z in (filter(λr.i - 1 <z inning(r);L) = [] ∈ (consensus-rcv(V;A) List))
  ∧ (||as|| = ||vs|| ∈ ℤ)
  ∧ (zip(as;vs) = votes-from-inning(i - 1;L) ∈ (({b:Id| (b ∈ A)}  × V) List))
  ∧ (0 ≤ i)
  ∧ 1 ≤ i supposing ¬↑null(L)
  ∧ (||values-for-distinct(IdDeq;votes-from-inning(i - 1;L))|| ≤ (2 * t)) ∈ Type

2
1. [V] : Type
2. v0 : V@i
3. A : Id List@i
4. t : ℕ+@i
5. f : (V List) ─→ V@i
6. L : consensus-rcv(V;A) List@i
7. v1 : 𝔹@i
8. v3 : ℤ@i
9. v5 : {a:Id| (a ∈ A)}  List@i
10. v7 : V List@i
11. v8 : V@i
12. consensus-accum-num-state(t;f;v0;L) = <v1, v3, v5, v7, v8> ∈ (𝔹 × ℤ × {a:Id| (a ∈ A)}  List × V List × V)@i
13. ∀n:ℕ. ∀v@0:V.  (archive-condition(V;A;t;f;n;v@0;L) ⇐⇒ (↑v1) ∧ ((n + 1) = v3 ∈ ℤ) ∧ (v@0 = v8 ∈ V))@i
14. let b,i,as,vs,v = <v1, v3, v5, v7, v8> in (filter(λr.i - 1 <z inning(r);L) = [] ∈ (consensus-rcv(V;A) List))
∧ (||as|| = ||vs|| ∈ ℤ)
∧ (zip(as;vs) = votes-from-inning(i - 1;L) ∈ (({b:Id| (b ∈ A)}  × V) List))
∧ (0 ≤ i)
∧ 1 ≤ i supposing ¬↑null(L)
∧ (||values-for-distinct(IdDeq;votes-from-inning(i - 1;L))|| ≤ (2 * t))
⊢ (¬↑null(L)) ⇒ (1 ≤ v3)

---

Latex:



1.  [V]  :  Type
2.  v0  :  V@i
3.  A  :  Id  List@i
4.  t  :  \mBbbN{}\msupplus{}@i
5.  f  :  (V  List)  {}\mrightarrow{}  V@i
6.  L  :  consensus-rcv(V;A)  List@i
7.  v1  :  \mBbbB{}@i
8.  v3  :  \mBbbZ{}@i
9.  v5  :  \{a:Id|  (a  \mmember{}  A)\}    List@i
10.  v7  :  V  List@i
11.  v8  :  V@i
12.  consensus-accum-num-state(t;f;v0;L)  =  <v1,  v3,  v5,  v7,  v8>@i
13.  \mforall{}n:\mBbbN{}.  \mforall{}v@0:V.    (archive-condition(V;A;t;f;n;v@0;L)  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}v1)  \mwedge{}  ((n  +  1)  =  v3)  \mwedge{}  (v@0  =  v8))@i
14.  let  b,i,as,vs,v  =  consensus-accum-num-state(t;f;v0;L)  in  (filter(\mlambda{}r.i  -  1  <z  inning(r);L)  =  [])
\mwedge{}  (||as||  =  ||vs||)
\mwedge{}  (zip(as;vs)  =  votes-from-inning(i  -  1;L))
\mwedge{}  (0  \mleq{}  i)
\mwedge{}  1  \mleq{}  i  supposing  \mneg{}\muparrow{}null(L)
\mwedge{}  (||values-for-distinct(IdDeq;votes-from-inning(i  -  1;L))||  \mleq{}  (2  *  t))
\mvdash{}  (\mneg{}\muparrow{}null(L))  {}\mRightarrow{}  (1  \mleq{}  v3)


By

At  \mkleeneopen{}Type\mkleeneclose{}  (HypSubst'  (-3)  (-1))\mcdot{}

---

Home Index