---

Step * of Lemma three-cs-safety

∀[V:Type]
  ∀eq:EqDecider(V). ∀A:Id List. ∀t:ℕ+. ∀f:(V List) ─→ V.
    ((∀vs:V List. (f vs ∈ vs) supposing ||vs|| ≥ 1 )
       ⇒ (∀v:V. ∀s:ts-reachable(three-consensus-ts(V;A;t;f)).
             (three-cs-decided(V;A;t;f;s;v)
             ⇒ ((∃a∈A. (||s a|| ≥ 1 ) ∧ (hd(s a) = Init[v] ∈ consensus-rcv(V;A)))
                ∧ (∀w:V. ∀s':ts-reachable(three-consensus-ts(V;A;t;f)).
                     ((s (ts-rel(three-consensus-ts(V;A;t;f))^*) s')
                     ⇒ three-cs-decided(V;A;t;f;s';w)
                     ⇒ (v = w ∈ V))))))) supposing 
       ((∀vs:V List. ∀v:V.
           ((f vs) = v ∈ V) supposing (((t + 1) ≤ ||filter(λx.(eqof(eq) x v);vs)||) and (||vs|| = ((2 * t) + 1) ∈ ℤ))) a\000Cnd 
       (||A|| = ((3 * t) + 1) ∈ ℤ) and 
       no_repeats(Id;A))
BY
{ (InstLemma `three-cs-safety1` []
   THEN (RepeatFor 4 (ParallelLast') THEN (D 0 THENA Auto) THEN PromoteHyp (-1) (-3))
   THEN RepeatFor 2 (ParallelLast')
   THEN (D 0 THENA Auto)
   THEN (InstHyp [⌈f⌉] (-2)⋅ THENA Auto)
   THEN (D 0 THENA Auto)
   THEN (InstLemma `three-cs-safety2` [⌈V⌉;⌈eq⌉;⌈A⌉;⌈t⌉;⌈f⌉]⋅ THENA Auto)
   THEN RepeatFor 3 (ParallelLast')
   THEN Auto
   THEN Try ((D -2 THEN RepUR ``ts-type three-consensus-ts`` -3 THEN Trivial))) }

---

Latex:


\mforall{}[V:Type]
    \mforall{}eq:EqDecider(V).  \mforall{}A:Id  List.  \mforall{}t:\mBbbN{}\msupplus{}.  \mforall{}f:(V  List)  {}\mrightarrow{}  V.
        ((\mforall{}vs:V  List.  (f  vs  \mmember{}  vs)  supposing  ||vs||  \mgeq{}  1  )
              {}\mRightarrow{}  (\mforall{}v:V.  \mforall{}s:ts-reachable(three-consensus-ts(V;A;t;f)).
                          (three-cs-decided(V;A;t;f;s;v)
                          {}\mRightarrow{}  ((\mexists{}a\mmember{}A.  (||s  a||  \mgeq{}  1  )  \mwedge{}  (hd(s  a)  =  Init[v]))
                                \mwedge{}  (\mforall{}w:V.  \mforall{}s':ts-reachable(three-consensus-ts(V;A;t;f)).
                                          ((s 
                                              (ts-rel(three-consensus-ts(V;A;t;f))\^{}*) 
                                              s')
                                          {}\mRightarrow{}  three-cs-decided(V;A;t;f;s';w)
                                          {}\mRightarrow{}  (v  =  w)))))))  supposing 
              ((\mforall{}vs:V  List.  \mforall{}v:V.
                      ((f  vs)  =  v)  supposing 
                            (((t  +  1)  \mleq{}  ||filter(\mlambda{}x.(eqof(eq)  x  v);vs)||)  and 
                            (||vs||  =  ((2  *  t)  +  1))))  and 
              (||A||  =  ((3  *  t)  +  1))  and 
              no\_repeats(Id;A))


By

(InstLemma  `three-cs-safety1`  []
  THEN  (RepeatFor  4  (ParallelLast')  THEN  (D  0  THENA  Auto)  THEN  PromoteHyp  (-1)  (-3))
  THEN  RepeatFor  2  (ParallelLast')
  THEN  (D  0  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}f\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  (InstLemma  `three-cs-safety2`  [\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  3  (ParallelLast')
  THEN  Auto
  THEN  Try  ((D  -2  THEN  RepUR  ``ts-type  three-consensus-ts``  -3  THEN  Trivial)))

---

Home Index