---

Step * 2 1 of Lemma consensus-accum-num-archives


1. [V] : Type
2. A : Id List@i
3. t : ℕ+@i
4. f : (V List) ─→ V@i
5. v0 : V@i
6. IdDeq ∈ EqDecider({b:Id| (b ∈ A)} )
7. ys : consensus-rcv(V;A) List@i
8. x : V@i
9. Init[x] ∈ consensus-rcv(V;A)
10. v1 : 𝔹@i
11. v3 : ℤ@i
12. v5 : {a:Id| (a ∈ A)}  List@i
13. v7 : V List@i
14. v8 : V@i
15. consensus-accum-num-state(t;f;v0;ys) = <v1, v3, v5, v7, v8> ∈ (𝔹 × ℤ × {a:Id| (a ∈ A)}  List × V List × V)@i
16. archive-condition(V;A;t;f;v3 - 1;v8;ys) supposing ↑v1@i
17. v3 = 0 ∈ ℤ
18. filter(λr.v3 - 1 <z inning(r);ys) = [] ∈ (consensus-rcv(V;A) List)@i
19. ||v5|| = ||v7|| ∈ ℤ@i
20. zip(v5;v7) = votes-from-inning(v3 - 1;ys) ∈ (({b:Id| (b ∈ A)}  × V) List)@i
21. 0 ≤ v3@i
22. 1 ≤ v3 supposing ¬↑null(ys)@i
23. ||values-for-distinct(IdDeq;votes-from-inning(v3 - 1;ys))|| ≤ (2 * t)@i
24. filter(λr.0 <z inning(r);ys @ [Init[x]]) = [] ∈ (consensus-rcv(V;A) List)@i
25. 0 = 0 ∈ ℤ@i
26. [] = votes-from-inning(0;ys @ [Init[x]]) ∈ (({b:Id| (b ∈ A)}  × V) List)@i
27. 0 ≤ 1@i
28. 1 ≤ 1 supposing ¬↑null(ys @ [Init[x]])@i
29. ||values-for-distinct(IdDeq;votes-from-inning(0;ys @ [Init[x]]))|| ≤ (2 * t)@i
30. True
⊢ {(ys = [] ∈ (consensus-rcv(V;A) List)) ∧ (0 = 0 ∈ ℤ) ∧ (x = x ∈ V)}
BY
{ ((D 0 THEN Auto) THEN DVar `ys' THEN All Reduce THEN ThinTrivial THEN Auto')⋅ }

---

Latex:



1.  [V]  :  Type
2.  A  :  Id  List@i
3.  t  :  \mBbbN{}\msupplus{}@i
4.  f  :  (V  List)  {}\mrightarrow{}  V@i
5.  v0  :  V@i
6.  IdDeq  \mmember{}  EqDecider(\{b:Id|  (b  \mmember{}  A)\}  )
7.  ys  :  consensus-rcv(V;A)  List@i
8.  x  :  V@i
9.  Init[x]  \mmember{}  consensus-rcv(V;A)
10.  v1  :  \mBbbB{}@i
11.  v3  :  \mBbbZ{}@i
12.  v5  :  \{a:Id|  (a  \mmember{}  A)\}    List@i
13.  v7  :  V  List@i
14.  v8  :  V@i
15.  consensus-accum-num-state(t;f;v0;ys)  =  <v1,  v3,  v5,  v7,  v8>@i
16.  archive-condition(V;A;t;f;v3  -  1;v8;ys)  supposing  \muparrow{}v1@i
17.  v3  =  0
18.  filter(\mlambda{}r.v3  -  1  <z  inning(r);ys)  =  []@i
19.  ||v5||  =  ||v7||@i
20.  zip(v5;v7)  =  votes-from-inning(v3  -  1;ys)@i
21.  0  \mleq{}  v3@i
22.  1  \mleq{}  v3  supposing  \mneg{}\muparrow{}null(ys)@i
23.  ||values-for-distinct(IdDeq;votes-from-inning(v3  -  1;ys))||  \mleq{}  (2  *  t)@i
24.  filter(\mlambda{}r.0  <z  inning(r);ys  @  [Init[x]])  =  []@i
25.  0  =  0@i
26.  []  =  votes-from-inning(0;ys  @  [Init[x]])@i
27.  0  \mleq{}  1@i
28.  1  \mleq{}  1  supposing  \mneg{}\muparrow{}null(ys  @  [Init[x]])@i
29.  ||values-for-distinct(IdDeq;votes-from-inning(0;ys  @  [Init[x]]))||  \mleq{}  (2  *  t)@i
30.  True
\mvdash{}  \{(ys  =  [])  \mwedge{}  (0  =  0)  \mwedge{}  (x  =  x)\}


By

((D  0  THEN  Auto)  THEN  DVar  `ys'  THEN  All  Reduce  THEN  ThinTrivial  THEN  Auto')\mcdot{}

---

Home Index