Proof of Nuprl Lemma : consensus-accum-num-archives

Step * 2 3 2 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. y2 : {b:Id| (b ∈ A)} @i
9. y4 : ℕ@i
10. y5 : V@i
11. Vote[y2;y4;y5] ∈ consensus-rcv(V;A)
12. v1 : 𝔹@i
13. v3 : ℤ@i
14. v5 : {a:Id| (a ∈ A)} List@i
15. v7 : V List@i
16. v8 : V@i

17. consensus-accum-num-state(t;f;v0;ys) = <v1, v3, v5, v7, v8> ∈ (𝔹 × ℤ × {a:Id| (a ∈ A)}  List × V List × V)@i

18. archive-condition(V;A;t;f;v3 - 1;v8;ys) supposing ↑v1@i
19. (v3 - 1) ≤ y4
20. y4 ≤ (v3 - 1)
21. ||remove-repeats(IdDeq;v5 @ [y2])|| = ((2 * t) + 1) ∈ ℤ
22. filter(λr.v3 - 1 <z inning(r);ys) = [] ∈ (consensus-rcv(V;A) List)@i
23. ||v5|| = ||v7|| ∈ ℤ@i
24. zip(v5;v7) = votes-from-inning(v3 - 1;ys) ∈ (({b:Id| (b ∈ A)} × V) List)@i
25. 0 ≤ v3@i
26. 1 ≤ v3 supposing ¬↑null(ys)@i
27. ||values-for-distinct(IdDeq;votes-from-inning(v3 - 1;ys))|| ≤ (2 * t)@i
28. filter(λr.(v3 + 1) - 1 <z inning(r);ys @ [Vote[y2;y4;y5]]) = [] ∈ (consensus-rcv(V;A) List)@i
29. 0 = 0 ∈ ℤ@i
30. [] = votes-from-inning((v3 + 1) - 1;ys @ [Vote[y2;y4;y5]]) ∈ (({b:Id| (b ∈ A)} × V) List)@i
31. 0 ≤ (v3 + 1)@i
32. 1 ≤ (v3 + 1) supposing ¬↑null(ys @ [Vote[y2;y4;y5]])@i
33. ||values-for-distinct(IdDeq;votes-from-inning((v3 + 1) - 1;ys @ [Vote[y2;y4;y5]]))|| ≤ (2 * t)@i
34. True
35. 0 < (v3 + 1) - 1
36. ||values-for-distinct(IdDeq;votes-from-inning((v3 + 1) - 1 - 1;ys))|| ≤ (2 * t)
37. ↑null(filter(λr.(v3 + 1) - 1 - 1 <z inning(r);ys))

⊢ ((y4 = ((v3 + 1) - 1) ∈ ℤ) ∧ ((f values-for-distinct(IdDeq;zip(v5 @ [y2];v7 @ [y5]))) = y5 ∈ V))

∨ ((((2 * t) + 1) ≤ ||values-for-distinct(IdDeq;votes-from-inning((v3 + 1) - 1 - 1;ys @ [Vote[y2;y4;y5]]))||)

  ∧ ((f values-for-distinct(IdDeq;votes-from-inning((v3 + 1) - 1 - 1;ys @ [Vote[y2;y4;y5]])))
    = (f values-for-distinct(IdDeq;zip(v5 @ [y2];v7 @ [y5])))
    ∈ V))
BY

{ Assert ⌈votes-from-inning(v3 - 1;ys @ [Vote[y2;y4;y5]]) = zip(v5 @ [y2];v7 @ [y5]) ∈ (({b:Id| (b ∈ A)}  × V) List)⌉⋅ }

1
.....assertion.....
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. y2 : {b:Id| (b ∈ A)} @i
9. y4 : ℕ@i
10. y5 : V@i
11. Vote[y2;y4;y5] ∈ consensus-rcv(V;A)
12. v1 : 𝔹@i
13. v3 : ℤ@i
14. v5 : {a:Id| (a ∈ A)} List@i
15. v7 : V List@i
16. v8 : V@i

17. consensus-accum-num-state(t;f;v0;ys) = <v1, v3, v5, v7, v8> ∈ (𝔹 × ℤ × {a:Id| (a ∈ A)}  List × V List × V)@i

⊢ votes-from-inning(v3 - 1;ys @ [Vote[y2;y4;y5]]) = zip(v5 @ [y2];v7 @ [y5]) ∈ (({b:Id| (b ∈ A)}  × V) List)

2
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. y2 : {b:Id| (b ∈ A)} @i
9. y4 : ℕ@i
10. y5 : V@i
11. Vote[y2;y4;y5] ∈ consensus-rcv(V;A)
12. v1 : 𝔹@i
13. v3 : ℤ@i
14. v5 : {a:Id| (a ∈ A)} List@i
15. v7 : V List@i
16. v8 : V@i

17. consensus-accum-num-state(t;f;v0;ys) = <v1, v3, v5, v7, v8> ∈ (𝔹 × ℤ × {a:Id| (a ∈ A)}  List × V List × V)@i

38. votes-from-inning(v3 - 1;ys @ [Vote[y2;y4;y5]]) = zip(v5 @ [y2];v7 @ [y5]) ∈ (({b:Id| (b ∈ A)}  × V) List)

⊢ ((y4 = ((v3 + 1) - 1) ∈ ℤ) ∧ ((f values-for-distinct(IdDeq;zip(v5 @ [y2];v7 @ [y5]))) = y5 ∈ V))

∨ ((((2 * t) + 1) ≤ ||values-for-distinct(IdDeq;votes-from-inning((v3 + 1) - 1 - 1;ys @ [Vote[y2;y4;y5]]))||)

  ∧ ((f values-for-distinct(IdDeq;votes-from-inning((v3 + 1) - 1 - 1;ys @ [Vote[y2;y4;y5]])))
    = (f values-for-distinct(IdDeq;zip(v5 @ [y2];v7 @ [y5])))
    ∈ V))

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. y2 : \{b:Id| (b \mmember{} A)\} @i 9. y4 : \mBbbN{}@i 10. y5 : V@i 11. Vote[y2;y4;y5] \mmember{} consensus-rcv(V;A) 12. v1 : \mBbbB{}@i 13. v3 : \mBbbZ{}@i 14. v5 : \{a:Id| (a \mmember{} A)\} List@i 15. v7 : V List@i 16. v8 : V@i 17. consensus-accum-num-state(t;f;v0;ys) = <v1, v3, v5, v7, v8>@i 18. archive-condition(V;A;t;f;v3 - 1;v8;ys) supposing \muparrow{}v1@i 19. (v3 - 1) \mleq{} y4 20. y4 \mleq{} (v3 - 1) 21. ||remove-repeats(IdDeq;v5 @ [y2])|| = ((2 * t) + 1) 22. filter(\mlambda{}r.v3 - 1 <z inning(r);ys) = []@i 23. ||v5|| = ||v7||@i 24. zip(v5;v7) = votes-from-inning(v3 - 1;ys)@i 25. 0 \mleq{} v3@i 26. 1 \mleq{} v3 supposing \mneg{}\muparrow{}null(ys)@i 27. ||values-for-distinct(IdDeq;votes-from-inning(v3 - 1;ys))|| \mleq{} (2 * t)@i 28. filter(\mlambda{}r.(v3 + 1) - 1 <z inning(r);ys @ [Vote[y2;y4;y5]]) = []@i 29. 0 = 0@i 30. [] = votes-from-inning((v3 + 1) - 1;ys @ [Vote[y2;y4;y5]])@i 31. 0 \mleq{} (v3 + 1)@i 32. 1 \mleq{} (v3 + 1) supposing \mneg{}\muparrow{}null(ys @ [Vote[y2;y4;y5]])@i 33. ||values-for-distinct(IdDeq;votes-from-inning((v3 + 1) - 1;ys @ [Vote[y2;y4;y5]]))|| \mleq{} (2 * t)@i 34. True 35. 0 < (v3 + 1) - 1 36. ||values-for-distinct(IdDeq;votes-from-inning((v3 + 1) - 1 - 1;ys))|| \mleq{} (2 * t) 37. \muparrow{}null(filter(\mlambda{}r.(v3 + 1) - 1 - 1 <z inning(r);ys)) \mvdash{} ((y4 = ((v3 + 1) - 1)) \mwedge{} ((f values-for-distinct(IdDeq;zip(v5 @ [y2];v7 @ [y5]))) = y5)) \mvee{} ((((2 * t) + 1) \mleq{} ||values-for-distinct(IdDeq;votes-from-inning((v3 + 1) - 1 - 1;ys @ [Vote[y2;y4;y5]]))||) \mwedge{} ((f values-for-distinct(IdDeq;votes-from-inning((v3 + 1) - 1 - 1;ys @ [Vote[y2;y4;y5]]))) = (f values-for-distinct(IdDeq;zip(v5 @ [y2];v7 @ [y5]))))) By Assert \mkleeneopen{}votes-from-inning(v3 - 1;ys @ [Vote[y2;y4;y5]]) = zip(v5 @ [y2];v7 @ [y5])\mkleeneclose{}\mcdot{} Home Index