Step
*
of Lemma
three-cs-safety1
∀[V:Type]. ∀[eq:EqDecider(V)]. ∀[A:Id List]. ∀[t:ℕ+].
(∀[f:(V List) ─→ V]
∀[v,w:V]. ∀[s,s':ts-reachable(three-consensus-ts(V;A;t;f))].
(v = w ∈ V) supposing
(three-cs-decided(V;A;t;f;s';w) and
three-cs-decided(V;A;t;f;s;v) and
(s (ts-rel(three-consensus-ts(V;A;t;f))^*) s'))
supposing ∀vs:V List. ∀v:V.
((||vs|| = ((2 * t) + 1) ∈ ℤ)
⇒ ((t + 1) ≤ ||filter(λx.(eqof(eq) x v);vs)||)
⇒ ((f vs) = v ∈ V))) supposing
((||A|| = ((3 * t) + 1) ∈ ℤ) and
no_repeats(Id;A))
BY
{ ((RepeatFor 6 ((D 0 THENA Auto)) THEN (InstLemma `three-intersecting-wait-set-exists` [⌈t⌉;⌈A⌉]⋅ THENA Auto))
THEN RepeatFor 6 ((D 0 THENA Auto))
THEN (Assert s ∈ {a:Id| (a ∈ A)} ─→ (consensus-rcv(V;A) List) BY
(DVar `s' THEN RepUR ``ts-type three-consensus-ts`` -3 THEN Auto))
THEN (Assert s' ∈ {a:Id| (a ∈ A)} ─→ (consensus-rcv(V;A) List) BY
(DVar `s\'' THEN RepUR ``ts-type three-consensus-ts`` -3 THEN Auto))
THEN 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
((∀ws:{a:Id| (a ∈ A)} List. ((ws ∈ W)
⇐⇒ (||ws|| = ((2 * t) + 1) ∈ ℤ) ∧ no_repeats({a:Id| (a ∈ A)} ;ws)))
∧ three-intersection(A;W))
8. f : (V List) ─→ V
9. ∀vs:V List. ∀v:V. ((||vs|| = ((2 * t) + 1) ∈ ℤ)
⇒ ((t + 1) ≤ ||filter(λx.(eqof(eq) x v);vs)||)
⇒ ((f vs) = v ∈ V))
10. v : V
11. w : V
12. s : ts-reachable(three-consensus-ts(V;A;t;f))
13. s' : ts-reachable(three-consensus-ts(V;A;t;f))
14. s ∈ {a:Id| (a ∈ A)} ─→ (consensus-rcv(V;A) List)
15. s' ∈ {a:Id| (a ∈ A)} ─→ (consensus-rcv(V;A) List)
16. s (ts-rel(three-consensus-ts(V;A;t;f))^*) s'
17. three-cs-decided(V;A;t;f;s;v)
18. three-cs-decided(V;A;t;f;s';w)
⊢ v = w ∈ V
Latex:
\mforall{}[V:Type]. \mforall{}[eq:EqDecider(V)]. \mforall{}[A:Id List]. \mforall{}[t:\mBbbN{}\msupplus{}].
(\mforall{}[f:(V List) {}\mrightarrow{} V]
\mforall{}[v,w:V]. \mforall{}[s,s':ts-reachable(three-consensus-ts(V;A;t;f))].
(v = w) supposing
(three-cs-decided(V;A;t;f;s';w) and
three-cs-decided(V;A;t;f;s;v) and
(s (ts-rel(three-consensus-ts(V;A;t;f))\^{}*) s'))
supposing \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))) supposing
((||A|| = ((3 * t) + 1)) and
no\_repeats(Id;A))
By
((RepeatFor 6 ((D 0 THENA Auto))
THEN (InstLemma `three-intersecting-wait-set-exists` [\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{} THENA Auto)
)
THEN RepeatFor 6 ((D 0 THENA Auto))
THEN (Assert s \mmember{} \{a:Id| (a \mmember{} A)\} {}\mrightarrow{} (consensus-rcv(V;A) List) BY
(DVar `s' THEN RepUR ``ts-type three-consensus-ts`` -3 THEN Auto))
THEN (Assert s' \mmember{} \{a:Id| (a \mmember{} A)\} {}\mrightarrow{} (consensus-rcv(V;A) List) BY
(DVar `s\mbackslash{}'' THEN RepUR ``ts-type three-consensus-ts`` -3 THEN Auto))
THEN Auto)
Home
Index