---

Step * of Lemma three-cs-int-safety

∀A:Id List. ∀t:ℕ+.
  (∀v:ℤ. ∀s:ts-reachable(three-consensus-ts(ℤ;A;t;λL.strict-majority-or-max(L))).
     (three-cs-decided(ℤ;A;t;λL.strict-majority-or-max(L);s;v)
     ⇒ ((∃a∈A. (||s a|| ≥ 1 ) ∧ (hd(s a) = Init[v] ∈ consensus-rcv(ℤ;A)))
        ∧ (∀w:ℤ. ∀s':ts-reachable(three-consensus-ts(ℤ;A;t;λL.strict-majority-or-max(L))).
             ((s (ts-rel(three-consensus-ts(ℤ;A;t;λL.strict-majority-or-max(L)))^*) s')
             ⇒ three-cs-decided(ℤ;A;t;λL.strict-majority-or-max(L);s';w)
             ⇒ (v = w ∈ ℤ)))))) supposing 
     ((||A|| = ((3 * t) + 1) ∈ ℤ) and 
     no_repeats(Id;A))
BY
{ ((InstLemma `three-cs-safety` [⌈ℤ⌉;⌈IntDeq⌉]⋅ THENA Auto)
   THEN RepeatFor 2 (ParallelLast')
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN (InstLemma `strict-majority-or-max-property` [⌈t⌉]⋅ THENA Auto)
   THEN (InstHyp [⌈λL.strict-majority-or-max(L)⌉] (-4)⋅
         THENA (Auto THEN RepUR ``int-deq eqof`` -1 THEN Reduce 0 THEN Auto)
         )
   THEN Try (Trivial)) }

---

Latex:


\mforall{}A:Id  List.  \mforall{}t:\mBbbN{}\msupplus{}.
    (\mforall{}v:\mBbbZ{}.  \mforall{}s:ts-reachable(three-consensus-ts(\mBbbZ{};A;t;\mlambda{}L.strict-majority-or-max(L))).
          (three-cs-decided(\mBbbZ{};A;t;\mlambda{}L.strict-majority-or-max(L);s;v)
          {}\mRightarrow{}  ((\mexists{}a\mmember{}A.  (||s  a||  \mgeq{}  1  )  \mwedge{}  (hd(s  a)  =  Init[v]))
                \mwedge{}  (\mforall{}w:\mBbbZ{}.  \mforall{}s':ts-reachable(three-consensus-ts(\mBbbZ{};A;t;\mlambda{}L.strict-majority-or-max(L))).
                          ((s 
                              (ts-rel(three-consensus-ts(\mBbbZ{};A;t;\mlambda{}L.strict-majority-or-max(L)))\^{}*) 
                              s')
                          {}\mRightarrow{}  three-cs-decided(\mBbbZ{};A;t;\mlambda{}L.strict-majority-or-max(L);s';w)
                          {}\mRightarrow{}  (v  =  w))))))  supposing 
          ((||A||  =  ((3  *  t)  +  1))  and 
          no\_repeats(Id;A))


By

((InstLemma  `three-cs-safety`  [\mkleeneopen{}\mBbbZ{}\mkleeneclose{};\mkleeneopen{}IntDeq\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast')
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (InstLemma  `strict-majority-or-max-property`  [\mkleeneopen{}t\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}L.strict-majority-or-max(L)\mkleeneclose{}]  (-4)\mcdot{}
              THENA  (Auto  THEN  RepUR  ``int-deq  eqof``  -1  THEN  Reduce  0  THEN  Auto)
              )
  THEN  Try  (Trivial))

---

Home Index