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

Step * 4 1 of Lemma consensus-accum-num-property2

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. v1 : 𝔹@i
12. v3 : ℤ@i
13. v5 : {a:Id| (a ∈ A)} List@i
14. v7 : V List@i
15. v8 : V@i

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

17. (v3 - 1) ≤ y4
18. y4 ≤ (v3 - 1)
19. ||remove-repeats(IdDeq;v5 @ [y2])|| = ((2 * t) + 1) ∈ ℤ
20. (((2 * t) + 1) ≤ ||remove-repeats(IdDeq;map(λp.(fst(p));votes-from-inning(v3 - 2;ys)))||) supposing
       ((votes-from-inning(v3 - 1;ys) = [] ∈ (({b:Id| (b ∈ A)}  × V) List)) and
       1 < v3)@i
21. 1 < v3 + 1
22. votes-from-inning((v3 + 1) - 1;ys) = [] ∈ (({b:Id| (b ∈ A)}  × V) List)
23. votes-from-inning((v3 + 1) - 1;[Vote[y2;y4;y5]]) = [] ∈ (({b:Id| (b ∈ A)}  × V) List)
24. filter(λr.v3 - 1 <z inning(r);ys) = [] ∈ (consensus-rcv(V;A) List)
25. ||v5|| = ||v7|| ∈ ℤ
26. zip(v5;v7) = votes-from-inning(v3 - 1;ys) ∈ (({b:Id| (b ∈ A)}  × V) List)
27. 0 ≤ v3
28. 1 ≤ v3 supposing ¬↑null(ys)
29. ||values-for-distinct(IdDeq;votes-from-inning(v3 - 1;ys))|| ≤ (2 * t)

⊢ ((2 * t) + 1) ≤ ||remove-repeats(IdDeq;map(λp.(fst(p));votes-from-inning((v3 + 1) - 2;ys @ [Vote[y2;y4;y5]])))||

BY
{ (Unfold `votes-from-inning` 0

   THEN ((RWO "mapfilter-append" 0 THENA Auto) THEN Fold `votes-from-inning` 0 THEN (RWO "map_append_sq" 0 THENA Auto))

) }

1
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. v1 : 𝔹@i
12. v3 : ℤ@i
13. v5 : {a:Id| (a ∈ A)} List@i
14. v7 : V List@i
15. v8 : V@i

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

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. v1 : \mBbbB{}@i 12. v3 : \mBbbZ{}@i 13. v5 : \{a:Id| (a \mmember{} A)\} List@i 14. v7 : V List@i 15. v8 : V@i 16. consensus-accum-num-state(t;f;v0;ys) = <v1, v3, v5, v7, v8>@i 17. (v3 - 1) \mleq{} y4 18. y4 \mleq{} (v3 - 1) 19. ||remove-repeats(IdDeq;v5 @ [y2])|| = ((2 * t) + 1) 20. (((2 * t) + 1) \mleq{} ||remove-repeats(IdDeq;map(\mlambda{}p.(fst(p));votes-from-inning(v3 - 2;ys)))||) supposing ((votes-from-inning(v3 - 1;ys) = []) and 1 < v3)@i 21. 1 < v3 + 1 22. votes-from-inning((v3 + 1) - 1;ys) = [] 23. votes-from-inning((v3 + 1) - 1;[Vote[y2;y4;y5]]) = [] 24. filter(\mlambda{}r.v3 - 1 <z inning(r);ys) = [] 25. ||v5|| = ||v7|| 26. zip(v5;v7) = votes-from-inning(v3 - 1;ys) 27. 0 \mleq{} v3 28. 1 \mleq{} v3 supposing \mneg{}\muparrow{}null(ys) 29. ||values-for-distinct(IdDeq;votes-from-inning(v3 - 1;ys))|| \mleq{} (2 * t) \mvdash{} ((2 * t) + 1) \mleq{} ||remove-repeats(IdDeq;map(\mlambda{}p.(fst(p));votes-from-inning((v3 + 1) - 2;ys @ [Vote[y2;y4;y5]])))|| By (Unfold `votes-from-inning` 0 THEN ((RWO "mapfilter-append" 0 THENA Auto) THEN Fold `votes-from-inning` 0 THEN (RWO "map\_append\_sq" 0 THENA Auto)) ) Home Index