---

Step * of Lemma consensus-state3-cases

∀[V:Type]
  ∀x:consensus-state3(V)
    (((x = INITIAL ∈ consensus-state3(V)) ∨ (x = WITHDRAWN ∈ consensus-state3(V)))
    ∨ (∃v:V. ((x = CONSIDERING[v] ∈ consensus-state3(V)) ∨ (x = COMMITED[v] ∈ consensus-state3(V)))))
BY
{ (Auto
   THEN D -1
   THEN Try ((Fold `cs-commited` 0 THEN OrRight THEN Auto))
   THEN D -1
   THEN Try ((Fold `cs-considering` 0 THEN OrRight THEN Auto))
   THEN AutoBoolCase ⌈y1⌉⋅) }

---

Latex:


\mforall{}[V:Type]
    \mforall{}x:consensus-state3(V)
        (((x  =  INITIAL)  \mvee{}  (x  =  WITHDRAWN))  \mvee{}  (\mexists{}v:V.  ((x  =  CONSIDERING[v])  \mvee{}  (x  =  COMMITED[v]))))


By

(Auto
  THEN  D  -1
  THEN  Try  ((Fold  `cs-commited`  0  THEN  OrRight  THEN  Auto))
  THEN  D  -1
  THEN  Try  ((Fold  `cs-considering`  0  THEN  OrRight  THEN  Auto))
  THEN  AutoBoolCase  \mkleeneopen{}y1\mkleeneclose{}\mcdot{})

---

Home Index