---

Step * 1 2 1 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-reachable(three-consensus-ts(V;A;t;f))
15. s ∈ {a:Id| (a ∈ A)}  ⟶ (consensus-rcv(V;A) List)
16. three-cs-decided(V;A;t;f;s;w)
17. three-cs-decided(V;A;t;f;s;v)
18. two-intersection(A;W)
⊢ v = w ∈ V
BY
{ (D -5
   THEN Assert ⌜∀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))))))))⌝⋅
   ) }

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
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. s ∈ {a:Id| (a ∈ A)}  ⟶ (consensus-rcv(V;A) List)
17. three-cs-decided(V;A;t;f;s;w)
18. three-cs-decided(V;A;t;f;s;v)
19. two-intersection(A;W)
⊢ ∀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))))))))

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. s ∈ {a:Id| (a ∈ A)}  ⟶ (consensus-rcv(V;A) List)
17. three-cs-decided(V;A;t;f;s;w)
18. three-cs-decided(V;A;t;f;s;v)
19. two-intersection(A;W)
20. ∀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))))))))
⊢ v = w ∈ V

---

Latex:

---

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-reachable(three-consensus-ts(V;A;t;f))
15.  s  \mmember{}  \{a:Id|  (a  \mmember{}  A)\}    {}\mrightarrow{}  (consensus-rcv(V;A)  List)
16.  three-cs-decided(V;A;t;f;s;w)
17.  three-cs-decided(V;A;t;f;s;v)
18.  two-intersection(A;W)
\mvdash{}  v  =  w


By

---

Latex:
(D  -5
  THEN  Assert  \mkleeneopen{}\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))))))))\mkleeneclose{}\mcdot{}
  )

---

Home Index