---

Step * of Lemma consensus-state4-exclusive-cases

∀[V:Type]
  ∀A:Id List. ∀s:ConsensusState. ∀a:{a:Id| (a ∈ A)} . ∀i:ℤ.
    ((by state s, a passed inning i without archiving a value
     ∧ (¬in state s, a has not completed inning i)
     ∧ (∀v:V. (¬by state s, a archived v in inning i)))
    ∨ (in state s, a has not completed inning i
      ∧ (¬by state s, a passed inning i without archiving a value)
      ∧ (∀v:V. (¬by state s, a archived v in inning i)))
    ∨ (∃v:V
        (by state s, a archived v in inning i
        ∧ (¬by state s, a passed inning i without archiving a value)
        ∧ (¬in state s, a has not completed inning i)
        ∧ (∀v':V. ¬by state s, a archived v' in inning i supposing ¬(v' = v ∈ V)))))
BY
{ (InstLemma `consensus-state4-cases` []
   THEN RepeatFor 6 (ParallelLast')
   THEN RepeatFor 2 (Try (ParallelLast))
   THEN Auto) }

---

Latex:


\mforall{}[V:Type]
    \mforall{}A:Id  List.  \mforall{}s:ConsensusState.  \mforall{}a:\{a:Id|  (a  \mmember{}  A)\}  .  \mforall{}i:\mBbbZ{}.
        ((by  state  s,  a  passed  inning  i  without  archiving  a  value
          \mwedge{}  (\mneg{}in  state  s,  a  has  not  completed  inning  i)
          \mwedge{}  (\mforall{}v:V.  (\mneg{}by  state  s,  a  archived  v  in  inning  i)))
        \mvee{}  (in  state  s,  a  has  not  completed  inning  i
            \mwedge{}  (\mneg{}by  state  s,  a  passed  inning  i  without  archiving  a  value)
            \mwedge{}  (\mforall{}v:V.  (\mneg{}by  state  s,  a  archived  v  in  inning  i)))
        \mvee{}  (\mexists{}v:V
                (by  state  s,  a  archived  v  in  inning  i
                \mwedge{}  (\mneg{}by  state  s,  a  passed  inning  i  without  archiving  a  value)
                \mwedge{}  (\mneg{}in  state  s,  a  has  not  completed  inning  i)
                \mwedge{}  (\mforall{}v':V.  \mneg{}by  state  s,  a  archived  v'  in  inning  i  supposing  \mneg{}(v'  =  v)))))


By

(InstLemma  `consensus-state4-cases`  []
  THEN  RepeatFor  6  (ParallelLast')
  THEN  RepeatFor  2  (Try  (ParallelLast))
  THEN  Auto)

---

Home Index