---

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:

---

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

---

Latex:
((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