Step
*
1
1
2
1
2
1
2
1
1
2
1
1
1
2
2
1
1
1
1
3
1
1
1
3
1
1
1
1
1
1
2
1
1
2
1
2
2
1
1
of Lemma
consensus-reachable
1. V : Type
2. ∀v1,v2:V. Dec(v1 = v2 ∈ V)@i
3. {∃v,v':V. (¬(v = v' ∈ V))}@i
4. A : Id List@i
5. W : {a:Id| (a ∈ A)} List List@i
6. three-intersection(A;W)@i
7. two-intersection(A;W)
8. one-intersection(A;W)
9. ws : {a:Id| (a ∈ A)} List@i
10. (ws ∈ W)@i
11. 0 < ||ws||
12. i : ℤ
13. x : ConsensusState
14. ∀a:{a:Id| (a ∈ A)} . ((a ∈ ws) ⇒ ((Inning(x;a) = i ∈ ℤ) ∧ (¬(i ∈ fpf-domain(Estimate(x;a))))))
15. v : V
16. state x may consider v in inning i
17. n : ℤ@i
18. ¬(A[n - 1] ∈ firstn(n - 1;A))
19. 0 < n@i
20. x ((λx,y. CR(in ws)[x, y] )^*) (λa.if a ∈b firstn(n - 1;A)) ∧b a ∈b ws) then <i, Estimate(x;a) ⊕ i : v> else x a fi \000C)@i
21. n - 1 < ||A||
22. (A[n - 1] ∈ ws)
23. ¬(A[n - 1] ∈ firstn(n - 1;A))
24. z : ConsensusState@i
25. (λa.if a ∈b firstn(n - 1;A)) ∧b a ∈b ws) then <i, Estimate(x;a) ⊕ i : v> else x a fi ) = z ∈ ConsensusState@i
26. (A[n - 1] ∈ ws)
27. Z : {a:Id| (a ∈ A)} ─→ (ℤ × j:ℤ fp-> V)@i
28. (λb.if b = A[n - 1] ∧b tt then <i, Estimate(z;b) ⊕ i : v> else z b fi ) = Z ∈ ConsensusState@i
29. (A[n - 1] ∈ ws)
30. ∀b:{a:Id| (a ∈ A)}
((¬(b = A[n - 1] ∈ Id)) ⇒ ((Inning(Z;b) = Inning(z;b) ∈ ℤ) ∧ (Estimate(Z;b) = Estimate(z;b) ∈ i:ℤ fp-> V)))
31. <i, Estimate(z;A[n - 1]) ⊕ i : v> = (Z A[n - 1]) ∈ (ℤ × j:ℤ fp-> V)
32. i = Inning(z;A[n - 1]) ∈ ℤ
33. ¬(Inning(z;A[n - 1]) ∈ fpf-domain(Estimate(z;A[n - 1])))
34. w1 : {a:Id| (a ∈ A)} List
35. (w1 ∈ W)
36. ∀b:{a:Id| (a ∈ A)} . ((b ∈ w1) ⇒ (i ≤ Inning(x;b)))
37. ∀ws':{a:Id| (a ∈ A)} List. ((ws' ∈ W) ⇒ (¬in state x, ws' blocks w1 from archiving v in inning i))
38. ws' : {a:Id| (a ∈ A)} List@i
39. (ws' ∈ W)@i
40. j : ℤ@i
41. 0 ≤ j@i
42. j < i@i
43. v' : V@i
44. ¬(v' = v ∈ V)@i
45. ∀b:{a:Id| (a ∈ A)}
(((b ∈ w1) ∧ (b ∈ ws'))
⇒ ((↑j ∈ dom(Estimate(λa.if a ∈b firstn(n - 1;A)) ∧b a ∈b ws) then <i, Estimate(x;a) ⊕ i : v> else x a fi ;b)))
∧ (Estimate(λa.if a ∈b firstn(n - 1;A)) ∧b a ∈b ws) then <i, Estimate(x;a) ⊕ i : v> else x a fi ;b)(j)
= v'
∈ V)
∧ (∀k:ℤ
(((j < k ∧ k < i)
∧ (↑k ∈ dom(Estimate(λa.if a ∈b firstn(n - 1;A)) ∧b a ∈b ws)
then <i, Estimate(x;a) ⊕ i : v>
else x a
fi ;b))))
⇒ (Estimate(λa.if a ∈b firstn(n - 1;A)) ∧b a ∈b ws) then <i, Estimate(x;a) ⊕ i : v> else x a fi ;b)(k)
= v'
∈ V)))))@i
46. b : {a:Id| (a ∈ A)} @i
47. (b ∈ w1)@i
48. (b ∈ ws')@i
49. ↑j ∈ dom(Estimate(λa.if a ∈b firstn(n - 1;A)) ∧b a ∈b ws) then <i, Estimate(x;a) ⊕ i : v> else x a fi ;b))
50. ↑j ∈ dom(Estimate(x;b))
⊢ (snd(if b ∈b firstn(n - 1;A)) ∧b b ∈b ws) then <i, Estimate(x;b) ⊕ i : v> else x b fi )(j) = v' ∈ V)
⇒ (Estimate(x;b)(j) = v' ∈ V)
BY
{ ((AutoBoolCase ⌈b ∈b firstn(n - 1;A))⌉⋅ THENA Auto)
THEN (AutoBoolCase ⌈b ∈b ws)⌉⋅ THENA Auto)
THEN Try ((Fold `cs-estimate` 0 THEN Auto))) }
1
1. V : Type
2. ∀v1,v2:V. Dec(v1 = v2 ∈ V)@i
3. {∃v,v':V. (¬(v = v' ∈ V))}@i
4. A : Id List@i
5. W : {a:Id| (a ∈ A)} List List@i
6. three-intersection(A;W)@i
7. two-intersection(A;W)
8. one-intersection(A;W)
9. ws : {a:Id| (a ∈ A)} List@i
10. (ws ∈ W)@i
11. 0 < ||ws||
12. i : ℤ
13. x : ConsensusState
14. ∀a:{a:Id| (a ∈ A)} . ((a ∈ ws) ⇒ ((Inning(x;a) = i ∈ ℤ) ∧ (¬(i ∈ fpf-domain(Estimate(x;a))))))
15. v : V
16. state x may consider v in inning i
17. n : ℤ@i
18. ¬(A[n - 1] ∈ firstn(n - 1;A))
19. 0 < n@i
20. x ((λx,y. CR(in ws)[x, y] )^*) (λa.if a ∈b firstn(n - 1;A)) ∧b a ∈b ws) then <i, Estimate(x;a) ⊕ i : v> else x a fi \000C)@i
21. n - 1 < ||A||
22. (A[n - 1] ∈ ws)
23. ¬(A[n - 1] ∈ firstn(n - 1;A))
24. z : ConsensusState@i
25. (λa.if a ∈b firstn(n - 1;A)) ∧b a ∈b ws) then <i, Estimate(x;a) ⊕ i : v> else x a fi ) = z ∈ ConsensusState@i
26. (A[n - 1] ∈ ws)
27. Z : {a:Id| (a ∈ A)} ─→ (ℤ × j:ℤ fp-> V)@i
28. (λb.if b = A[n - 1] ∧b tt then <i, Estimate(z;b) ⊕ i : v> else z b fi ) = Z ∈ ConsensusState@i
29. (A[n - 1] ∈ ws)
30. ∀b:{a:Id| (a ∈ A)}
((¬(b = A[n - 1] ∈ Id)) ⇒ ((Inning(Z;b) = Inning(z;b) ∈ ℤ) ∧ (Estimate(Z;b) = Estimate(z;b) ∈ i:ℤ fp-> V)))
31. <i, Estimate(z;A[n - 1]) ⊕ i : v> = (Z A[n - 1]) ∈ (ℤ × j:ℤ fp-> V)
32. i = Inning(z;A[n - 1]) ∈ ℤ
33. ¬(Inning(z;A[n - 1]) ∈ fpf-domain(Estimate(z;A[n - 1])))
34. w1 : {a:Id| (a ∈ A)} List
35. (w1 ∈ W)
36. ∀b:{a:Id| (a ∈ A)} . ((b ∈ w1) ⇒ (i ≤ Inning(x;b)))
37. ∀ws':{a:Id| (a ∈ A)} List. ((ws' ∈ W) ⇒ (¬in state x, ws' blocks w1 from archiving v in inning i))
38. ws' : {a:Id| (a ∈ A)} List@i
39. (ws' ∈ W)@i
40. j : ℤ@i
41. 0 ≤ j@i
42. j < i@i
43. v' : V@i
44. ¬(v' = v ∈ V)@i
45. ∀b:{a:Id| (a ∈ A)}
(((b ∈ w1) ∧ (b ∈ ws'))
⇒ ((↑j ∈ dom(Estimate(λa.if a ∈b firstn(n - 1;A)) ∧b a ∈b ws) then <i, Estimate(x;a) ⊕ i : v> else x a fi ;b)))
∧ (Estimate(λa.if a ∈b firstn(n - 1;A)) ∧b a ∈b ws) then <i, Estimate(x;a) ⊕ i : v> else x a fi ;b)(j)
= v'
∈ V)
∧ (∀k:ℤ
(((j < k ∧ k < i)
∧ (↑k ∈ dom(Estimate(λa.if a ∈b firstn(n - 1;A)) ∧b a ∈b ws)
then <i, Estimate(x;a) ⊕ i : v>
else x a
fi ;b))))
⇒ (Estimate(λa.if a ∈b firstn(n - 1;A)) ∧b a ∈b ws) then <i, Estimate(x;a) ⊕ i : v> else x a fi ;b)(k)
= v'
∈ V)))))@i
46. b : {a:Id| (a ∈ A)} @i
47. (b ∈ w1)@i
48. (b ∈ ws')@i
49. ↑j ∈ dom(Estimate(λa.if a ∈b firstn(n - 1;A)) ∧b a ∈b ws) then <i, Estimate(x;a) ⊕ i : v> else x a fi ;b))
50. ↑j ∈ dom(Estimate(x;b))
51. (b ∈ firstn(n - 1;A))
52. (b ∈ ws)
⊢ (Estimate(x;b) ⊕ i : v(j) = v' ∈ V) ⇒ (Estimate(x;b)(j) = v' ∈ V)
Latex:
1. V : Type
2. \mforall{}v1,v2:V. Dec(v1 = v2)@i
3. \{\mexists{}v,v':V. (\mneg{}(v = v'))\}@i
4. A : Id List@i
5. W : \{a:Id| (a \mmember{} A)\} List List@i
6. three-intersection(A;W)@i
7. two-intersection(A;W)
8. one-intersection(A;W)
9. ws : \{a:Id| (a \mmember{} A)\} List@i
10. (ws \mmember{} W)@i
11. 0 < ||ws||
12. i : \mBbbZ{}
13. x : ConsensusState
14. \mforall{}a:\{a:Id| (a \mmember{} A)\} . ((a \mmember{} ws) {}\mRightarrow{} ((Inning(x;a) = i) \mwedge{} (\mneg{}(i \mmember{} fpf-domain(Estimate(x;a))))))
15. v : V
16. state x may consider v in inning i
17. n : \mBbbZ{}@i
18. \mneg{}(A[n - 1] \mmember{} firstn(n - 1;A))
19. 0 < n@i
20. x
rel\_star(ConsensusState; \mlambda{}x,y. CR(in ws)[x, y] )
(\mlambda{}a.if a \mmember{}\msubb{} firstn(n - 1;A)) \mwedge{}\msubb{} a \mmember{}\msubb{} ws) then <i, Estimate(x;a) \moplus{} i : v> else x a fi )@i
21. n - 1 < ||A||
22. (A[n - 1] \mmember{} ws)
23. \mneg{}(A[n - 1] \mmember{} firstn(n - 1;A))
24. z : ConsensusState@i
25. (\mlambda{}a.if a \mmember{}\msubb{} firstn(n - 1;A)) \mwedge{}\msubb{} a \mmember{}\msubb{} ws) then <i, Estimate(x;a) \moplus{} i : v> else x a fi ) = z@i
26. (A[n - 1] \mmember{} ws)
27. Z : \{a:Id| (a \mmember{} A)\} {}\mrightarrow{} (\mBbbZ{} \mtimes{} j:\mBbbZ{} fp-> V)@i
28. (\mlambda{}b.if b = A[n - 1] \mwedge{}\msubb{} tt then <i, Estimate(z;b) \moplus{} i : v> else z b fi ) = Z@i
29. (A[n - 1] \mmember{} ws)
30. \mforall{}b:\{a:Id| (a \mmember{} A)\}
((\mneg{}(b = A[n - 1])) {}\mRightarrow{} ((Inning(Z;b) = Inning(z;b)) \mwedge{} (Estimate(Z;b) = Estimate(z;b))))
31. <i, Estimate(z;A[n - 1]) \moplus{} i : v> = (Z A[n - 1])
32. i = Inning(z;A[n - 1])
33. \mneg{}(Inning(z;A[n - 1]) \mmember{} fpf-domain(Estimate(z;A[n - 1])))
34. w1 : \{a:Id| (a \mmember{} A)\} List
35. (w1 \mmember{} W)
36. \mforall{}b:\{a:Id| (a \mmember{} A)\} . ((b \mmember{} w1) {}\mRightarrow{} (i \mleq{} Inning(x;b)))
37. \mforall{}ws':\{a:Id| (a \mmember{} A)\} List
((ws' \mmember{} W) {}\mRightarrow{} (\mneg{}in state x, ws' blocks w1 from archiving v in inning i))
38. ws' : \{a:Id| (a \mmember{} A)\} List@i
39. (ws' \mmember{} W)@i
40. j : \mBbbZ{}@i
41. 0 \mleq{} j@i
42. j < i@i
43. v' : V@i
44. \mneg{}(v' = v)@i
45. \mforall{}b:\{a:Id| (a \mmember{} A)\}
(((b \mmember{} w1) \mwedge{} (b \mmember{} ws'))
{}\mRightarrow{} ((\muparrow{}j \mmember{} dom(Estimate(\mlambda{}a.if a \mmember{}\msubb{} firstn(n - 1;A)) \mwedge{}\msubb{} a \mmember{}\msubb{} ws)
then <i, Estimate(x;a) \moplus{} i : v>
else x a
fi ;b)))
\mwedge{} (Estimate(\mlambda{}a.if a \mmember{}\msubb{} firstn(n - 1;A)) \mwedge{}\msubb{} a \mmember{}\msubb{} ws)
then <i, Estimate(x;a) \moplus{} i : v>
else x a
fi ;b)(j)
= v')
\mwedge{} (\mforall{}k:\mBbbZ{}
(((j < k \mwedge{} k < i)
\mwedge{} (\muparrow{}k \mmember{} dom(Estimate(\mlambda{}a.if a \mmember{}\msubb{} firstn(n - 1;A)) \mwedge{}\msubb{} a \mmember{}\msubb{} ws)
then <i, Estimate(x;a) \moplus{} i : v>
else x a
fi ;b))))
{}\mRightarrow{} (Estimate(\mlambda{}a.if a \mmember{}\msubb{} firstn(n - 1;A)) \mwedge{}\msubb{} a \mmember{}\msubb{} ws)
then <i, Estimate(x;a) \moplus{} i : v>
else x a
fi ;b)(k)
= v')))))@i
46. b : \{a:Id| (a \mmember{} A)\} @i
47. (b \mmember{} w1)@i
48. (b \mmember{} ws')@i
49. \muparrow{}j \mmember{} dom(Estimate(\mlambda{}a.if a \mmember{}\msubb{} firstn(n - 1;A)) \mwedge{}\msubb{} a \mmember{}\msubb{} ws)
then <i, Estimate(x;a) \moplus{} i : v>
else x a
fi ;b))
50. \muparrow{}j \mmember{} dom(Estimate(x;b))
\mvdash{} (snd(if b \mmember{}\msubb{} firstn(n - 1;A)) \mwedge{}\msubb{} b \mmember{}\msubb{} ws) then <i, Estimate(x;b) \moplus{} i : v> else x b fi )(j) = v')
{}\mRightarrow{} (Estimate(x;b)(j) = v')
By
((AutoBoolCase \mkleeneopen{}b \mmember{}\msubb{} firstn(n - 1;A))\mkleeneclose{}\mcdot{} THENA Auto)
THEN (AutoBoolCase \mkleeneopen{}b \mmember{}\msubb{} ws)\mkleeneclose{}\mcdot{} THENA Auto)
THEN Try ((Fold `cs-estimate` 0 THEN Auto)))
Home
Index