Step
*
1
2
1
1
2
1
2
of Lemma
three-cs-safety1
1. V : Type
2. eq : EqDecider(V)
3. A : Id List
4. t : ℕ+
5. no_repeats(Id;A)
6. ||A|| = ((3 * t) + 1) ∈ ℤ
7. W : {a:Id| (a ∈ A)} List List
8. ∀ws:{a:Id| (a ∈ A)} List. ((ws ∈ W) ⇐⇒ (||ws|| = ((2 * t) + 1) ∈ ℤ) ∧ no_repeats({a:Id| (a ∈ A)} ;ws))
9. three-intersection(A;W)
10. f : (V List) ─→ V
11. ∀vs:V List. ∀v:V.
((||vs|| = ((2 * t) + 1) ∈ ℤ) ⇒ ((t + 1) ≤ ||filter(λx.(eqof(eq) x v);vs)||) ⇒ ((f vs) = v ∈ V))
12. v : V
13. w : V
14. s : ts-type(three-consensus-ts(V;A;t;f))
15. ts-init(three-consensus-ts(V;A;t;f)) (ts-rel(three-consensus-ts(V;A;t;f))^*) s
16. ∀i:ℤ. ∀ws:{a:Id| (a ∈ A)} List. ∀x:V.
(no_repeats({a:Id| (a ∈ A)} ;ws)
⇒ (||ws|| = ((2 * t) + 1) ∈ ℤ)
⇒ (∀a∈ws.∃L:consensus-rcv(V;A) List. (L ≤ s a ∧ archive-condition(V;A;t;f;i;x;L)))
⇒ (∀j:ℤ
(i < j
⇒ (∀b:{a:Id| (a ∈ A)}
((b ∈ ws)
⇒ (∀z:V. ∀L:consensus-rcv(V;A) List.
(L ≤ s b ⇒ archive-condition(V;A;t;f;j;z;L) ⇒ (z = x ∈ V))))))))
17. s ∈ {a:Id| (a ∈ A)} ─→ (consensus-rcv(V;A) List)
18. i : ℤ
19. w1 : {a:Id| (a ∈ A)} List
20. no_repeats({a:Id| (a ∈ A)} ;w1)
21. ||w1|| = ((2 * t) + 1) ∈ ℤ
22. ∀a:{a:Id| (a ∈ A)} . ((a ∈ w1) ⇒ (∃L:consensus-rcv(V;A) List. (L ≤ s a ∧ archive-condition(V;A;t;f;i;w;L))))
23. i1 : ℤ
24. ws : {a:Id| (a ∈ A)} List
25. no_repeats({a:Id| (a ∈ A)} ;ws)
26. ||ws|| = ((2 * t) + 1) ∈ ℤ
27. ∀a:{a:Id| (a ∈ A)} . ((a ∈ ws) ⇒ (∃L:consensus-rcv(V;A) List. (L ≤ s a ∧ archive-condition(V;A;t;f;i1;v;L))))
28. a : {a:Id| (a ∈ A)}
29. (a ∈ ws)
30. (a ∈ w1)
31. L : consensus-rcv(V;A) List
32. L ≤ s a
33. archive-condition(V;A;t;f;i1;v;L)
34. L1 : consensus-rcv(V;A) List
35. L1 ≤ s a
36. archive-condition(V;A;t;f;i;w;L1)
37. L ≤ L1
⊢ v = w ∈ V
BY
{ (Decide ||L|| < ||L1|| THENA Auto) }
1
1. V : Type
2. eq : EqDecider(V)
3. A : Id List
4. t : ℕ+
5. no_repeats(Id;A)
6. ||A|| = ((3 * t) + 1) ∈ ℤ
7. W : {a:Id| (a ∈ A)} List List
8. ∀ws:{a:Id| (a ∈ A)} List. ((ws ∈ W) ⇐⇒ (||ws|| = ((2 * t) + 1) ∈ ℤ) ∧ no_repeats({a:Id| (a ∈ A)} ;ws))
9. three-intersection(A;W)
10. f : (V List) ─→ V
11. ∀vs:V List. ∀v:V.
((||vs|| = ((2 * t) + 1) ∈ ℤ) ⇒ ((t + 1) ≤ ||filter(λx.(eqof(eq) x v);vs)||) ⇒ ((f vs) = v ∈ V))
12. v : V
13. w : V
14. s : ts-type(three-consensus-ts(V;A;t;f))
15. ts-init(three-consensus-ts(V;A;t;f)) (ts-rel(three-consensus-ts(V;A;t;f))^*) s
16. ∀i:ℤ. ∀ws:{a:Id| (a ∈ A)} List. ∀x:V.
(no_repeats({a:Id| (a ∈ A)} ;ws)
⇒ (||ws|| = ((2 * t) + 1) ∈ ℤ)
⇒ (∀a∈ws.∃L:consensus-rcv(V;A) List. (L ≤ s a ∧ archive-condition(V;A;t;f;i;x;L)))
⇒ (∀j:ℤ
(i < j
⇒ (∀b:{a:Id| (a ∈ A)}
((b ∈ ws)
⇒ (∀z:V. ∀L:consensus-rcv(V;A) List.
(L ≤ s b ⇒ archive-condition(V;A;t;f;j;z;L) ⇒ (z = x ∈ V))))))))
17. s ∈ {a:Id| (a ∈ A)} ─→ (consensus-rcv(V;A) List)
18. i : ℤ
19. w1 : {a:Id| (a ∈ A)} List
20. no_repeats({a:Id| (a ∈ A)} ;w1)
21. ||w1|| = ((2 * t) + 1) ∈ ℤ
22. ∀a:{a:Id| (a ∈ A)} . ((a ∈ w1) ⇒ (∃L:consensus-rcv(V;A) List. (L ≤ s a ∧ archive-condition(V;A;t;f;i;w;L))))
23. i1 : ℤ
24. ws : {a:Id| (a ∈ A)} List
25. no_repeats({a:Id| (a ∈ A)} ;ws)
26. ||ws|| = ((2 * t) + 1) ∈ ℤ
27. ∀a:{a:Id| (a ∈ A)} . ((a ∈ ws) ⇒ (∃L:consensus-rcv(V;A) List. (L ≤ s a ∧ archive-condition(V;A;t;f;i1;v;L))))
28. a : {a:Id| (a ∈ A)}
29. (a ∈ ws)
30. (a ∈ w1)
31. L : consensus-rcv(V;A) List
32. L ≤ s a
33. archive-condition(V;A;t;f;i1;v;L)
34. L1 : consensus-rcv(V;A) List
35. L1 ≤ s a
36. archive-condition(V;A;t;f;i;w;L1)
37. L ≤ L1
38. ||L|| < ||L1||
⊢ v = w ∈ V
2
1. V : Type
2. eq : EqDecider(V)
3. A : Id List
4. t : ℕ+
5. no_repeats(Id;A)
6. ||A|| = ((3 * t) + 1) ∈ ℤ
7. W : {a:Id| (a ∈ A)} List List
8. ∀ws:{a:Id| (a ∈ A)} List. ((ws ∈ W) ⇐⇒ (||ws|| = ((2 * t) + 1) ∈ ℤ) ∧ no_repeats({a:Id| (a ∈ A)} ;ws))
9. three-intersection(A;W)
10. f : (V List) ─→ V
11. ∀vs:V List. ∀v:V.
((||vs|| = ((2 * t) + 1) ∈ ℤ) ⇒ ((t + 1) ≤ ||filter(λx.(eqof(eq) x v);vs)||) ⇒ ((f vs) = v ∈ V))
12. v : V
13. w : V
14. s : ts-type(three-consensus-ts(V;A;t;f))
15. ts-init(three-consensus-ts(V;A;t;f)) (ts-rel(three-consensus-ts(V;A;t;f))^*) s
16. ∀i:ℤ. ∀ws:{a:Id| (a ∈ A)} List. ∀x:V.
(no_repeats({a:Id| (a ∈ A)} ;ws)
⇒ (||ws|| = ((2 * t) + 1) ∈ ℤ)
⇒ (∀a∈ws.∃L:consensus-rcv(V;A) List. (L ≤ s a ∧ archive-condition(V;A;t;f;i;x;L)))
⇒ (∀j:ℤ
(i < j
⇒ (∀b:{a:Id| (a ∈ A)}
((b ∈ ws)
⇒ (∀z:V. ∀L:consensus-rcv(V;A) List.
(L ≤ s b ⇒ archive-condition(V;A;t;f;j;z;L) ⇒ (z = x ∈ V))))))))
17. s ∈ {a:Id| (a ∈ A)} ─→ (consensus-rcv(V;A) List)
18. i : ℤ
19. w1 : {a:Id| (a ∈ A)} List
20. no_repeats({a:Id| (a ∈ A)} ;w1)
21. ||w1|| = ((2 * t) + 1) ∈ ℤ
22. ∀a:{a:Id| (a ∈ A)} . ((a ∈ w1) ⇒ (∃L:consensus-rcv(V;A) List. (L ≤ s a ∧ archive-condition(V;A;t;f;i;w;L))))
23. i1 : ℤ
24. ws : {a:Id| (a ∈ A)} List
25. no_repeats({a:Id| (a ∈ A)} ;ws)
26. ||ws|| = ((2 * t) + 1) ∈ ℤ
27. ∀a:{a:Id| (a ∈ A)} . ((a ∈ ws) ⇒ (∃L:consensus-rcv(V;A) List. (L ≤ s a ∧ archive-condition(V;A;t;f;i1;v;L))))
28. a : {a:Id| (a ∈ A)}
29. (a ∈ ws)
30. (a ∈ w1)
31. L : consensus-rcv(V;A) List
32. L ≤ s a
33. archive-condition(V;A;t;f;i1;v;L)
34. L1 : consensus-rcv(V;A) List
35. L1 ≤ s a
36. archive-condition(V;A;t;f;i;w;L1)
37. L ≤ L1
38. ¬||L|| < ||L1||
⊢ v = w ∈ V
Latex:
1. V : Type
2. eq : EqDecider(V)
3. A : Id List
4. t : \mBbbN{}\msupplus{}
5. no\_repeats(Id;A)
6. ||A|| = ((3 * t) + 1)
7. W : \{a:Id| (a \mmember{} A)\} List List
8. \mforall{}ws:\{a:Id| (a \mmember{} A)\} List. ((ws \mmember{} W) \mLeftarrow{}{}\mRightarrow{} (||ws|| = ((2 * t) + 1)) \mwedge{} no\_repeats(\{a:Id| (a \mmember{} A)\} ;w\000Cs))
9. three-intersection(A;W)
10. f : (V List) {}\mrightarrow{} V
11. \mforall{}vs:V List. \mforall{}v:V.
((||vs|| = ((2 * t) + 1)) {}\mRightarrow{} ((t + 1) \mleq{} ||filter(\mlambda{}x.(eqof(eq) x v);vs)||) {}\mRightarrow{} ((f vs) = v))
12. v : V
13. w : V
14. s : ts-type(three-consensus-ts(V;A;t;f))
15. ts-init(three-consensus-ts(V;A;t;f))
(ts-rel(three-consensus-ts(V;A;t;f))\^{}*)
s
16. \mforall{}i:\mBbbZ{}. \mforall{}ws:\{a:Id| (a \mmember{} A)\} List. \mforall{}x:V.
(no\_repeats(\{a:Id| (a \mmember{} A)\} ;ws)
{}\mRightarrow{} (||ws|| = ((2 * t) + 1))
{}\mRightarrow{} (\mforall{}a\mmember{}ws.\mexists{}L:consensus-rcv(V;A) List. (L \mleq{} s a \mwedge{} archive-condition(V;A;t;f;i;x;L)))
{}\mRightarrow{} (\mforall{}j:\mBbbZ{}
(i < j
{}\mRightarrow{} (\mforall{}b:\{a:Id| (a \mmember{} A)\}
((b \mmember{} ws)
{}\mRightarrow{} (\mforall{}z:V. \mforall{}L:consensus-rcv(V;A) List.
(L \mleq{} s b {}\mRightarrow{} archive-condition(V;A;t;f;j;z;L) {}\mRightarrow{} (z = x))))))))
17. s \mmember{} \{a:Id| (a \mmember{} A)\} {}\mrightarrow{} (consensus-rcv(V;A) List)
18. i : \mBbbZ{}
19. w1 : \{a:Id| (a \mmember{} A)\} List
20. no\_repeats(\{a:Id| (a \mmember{} A)\} ;w1)
21. ||w1|| = ((2 * t) + 1)
22. \mforall{}a:\{a:Id| (a \mmember{} A)\}
((a \mmember{} w1) {}\mRightarrow{} (\mexists{}L:consensus-rcv(V;A) List. (L \mleq{} s a \mwedge{} archive-condition(V;A;t;f;i;w;L))))
23. i1 : \mBbbZ{}
24. ws : \{a:Id| (a \mmember{} A)\} List
25. no\_repeats(\{a:Id| (a \mmember{} A)\} ;ws)
26. ||ws|| = ((2 * t) + 1)
27. \mforall{}a:\{a:Id| (a \mmember{} A)\}
((a \mmember{} ws) {}\mRightarrow{} (\mexists{}L:consensus-rcv(V;A) List. (L \mleq{} s a \mwedge{} archive-condition(V;A;t;f;i1;v;L))))
28. a : \{a:Id| (a \mmember{} A)\}
29. (a \mmember{} ws)
30. (a \mmember{} w1)
31. L : consensus-rcv(V;A) List
32. L \mleq{} s a
33. archive-condition(V;A;t;f;i1;v;L)
34. L1 : consensus-rcv(V;A) List
35. L1 \mleq{} s a
36. archive-condition(V;A;t;f;i;w;L1)
37. L \mleq{} L1
\mvdash{} v = w
By
(Decide ||L|| < ||L1|| THENA Auto)
Home
Index