---

Step * 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
    ((∀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
BY
{ Assert ⌈three-cs-decided(V;A;t;f;s';v)⌉⋅ }

1
.....assertion..... 
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)
⊢ three-cs-decided(V;A;t;f;s';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
    ((∀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)
19. three-cs-decided(V;A;t;f;s';v)
⊢ 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.  \mexists{}W:\{a:Id|  (a  \mmember{}  A)\}    List  List
        ((\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)\}\000C  ;ws)))
        \mwedge{}  three-intersection(A;W))
8.  f  :  (V  List)  {}\mrightarrow{}  V
9.  \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))
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  \mmember{}  \{a:Id|  (a  \mmember{}  A)\}    {}\mrightarrow{}  (consensus-rcv(V;A)  List)
15.  s'  \mmember{}  \{a:Id|  (a  \mmember{}  A)\}    {}\mrightarrow{}  (consensus-rcv(V;A)  List)
16.  s  rel\_star(ts-type(three-consensus-ts(V;A;t;f));  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)
\mvdash{}  v  =  w


By

Assert  \mkleeneopen{}three-cs-decided(V;A;t;f;s';v)\mkleeneclose{}\mcdot{}

---

Home Index