Step
*
1
2
1
1
2
1
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. three-cs-decided(V;A;t;f;s;w)
19. three-cs-decided(V;A;t;f;s;v)
20. two-intersection(A;W)
⊢ v = w ∈ V
BY
{ (D -3
THEN D -2
THEN (ExRepD
THEN (Unfold `two-intersection` -1
THEN (RWW "l_all_iff" (-1) THENA Auto)
THEN InstHyp [⌈ws⌉;⌈w1⌉] (-1)⋅
THEN Auto)
)
THEN (ExRepD
THEN Thin (-4)
THEN ExRepD
THEN AllHyps h.((RWO "l_all_iff" h THENA Auto) THEN (InstHyp [⌈a⌉] h⋅ THENA Auto) THEN RepeatFor 2 (D -1))
THEN (FLemma `common_iseg_compat` [-2;-5] THENA Auto)
THEN D -1)⋅) }
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. L1 ≤ L
⊢ 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
⊢ 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. three-cs-decided(V;A;t;f;s;w)
19. three-cs-decided(V;A;t;f;s;v)
20. two-intersection(A;W)
\mvdash{} v = w
By
(D -3
THEN D -2
THEN (ExRepD
THEN (Unfold `two-intersection` -1
THEN (RWW "l\_all\_iff" (-1) THENA Auto)
THEN InstHyp [\mkleeneopen{}ws\mkleeneclose{};\mkleeneopen{}w1\mkleeneclose{}] (-1)\mcdot{}
THEN Auto)
)
THEN (ExRepD
THEN Thin (-4)
THEN ExRepD
THEN AllHyps h.((RWO "l\_all\_iff" h THENA Auto)
THEN (InstHyp [\mkleeneopen{}a\mkleeneclose{}] h\mcdot{} THENA Auto)
THEN RepeatFor 2 (D -1))
THEN (FLemma `common\_iseg\_compat` [-2;-5] THENA Auto)
THEN D -1)\mcdot{})
Home
Index