---

Step * of Lemma consensus-event-cases

∀[V:Type]
  ∀A:Id List. ∀e:consensus-event(V;A).
    ((e = NextInning ∈ consensus-event(V;A))
    ∨ (∃v:V. (e = Archive(v) ∈ consensus-event(V;A)))
    ∨ (∃b:{a:Id| (a ∈ A)} . ∃i:ℕ. ∃z:ℕi × V?. (e = consensus-message(b;i;z) ∈ consensus-event(V;A))))
BY
{ ((Auto THEN D -1)
   THENL [(OrLeft
           THEN Subst' inl x ~ NextInning 0
           THEN Try (Complete (Auto))
           THEN Unfold `inning-event` 0
           THEN Auto
           THEN (D -1 THEN Unfold `it` 0)
           THEN Auto
           THEN Fold `it` 0
           THEN Auto)
         ; (OrRight
            THEN D -1
            THEN Try ((Fold `archive-event` 0 THEN Auto THEN OrLeft THEN Auto))
            THEN RepeatFor 2 (D -1)
            THEN Fold `consensus-message` 0
            THEN Auto
            THEN OrRight
            THEN Auto)]
) }

---

Latex:


\mforall{}[V:Type]
    \mforall{}A:Id  List.  \mforall{}e:consensus-event(V;A).
        ((e  =  NextInning)
        \mvee{}  (\mexists{}v:V.  (e  =  Archive(v)))
        \mvee{}  (\mexists{}b:\{a:Id|  (a  \mmember{}  A)\}  .  \mexists{}i:\mBbbN{}.  \mexists{}z:\mBbbN{}i  \mtimes{}  V?.  (e  =  consensus-message(b;i;z))))


By

((Auto  THEN  D  -1)
  THENL  [(OrLeft
                  THEN  Subst'  inl  x  \msim{}  NextInning  0
                  THEN  Try  (Complete  (Auto))
                  THEN  Unfold  `inning-event`  0
                  THEN  Auto
                  THEN  (D  -1  THEN  Unfold  `it`  0)
                  THEN  Auto
                  THEN  Fold  `it`  0
                  THEN  Auto)
              ;  (OrRight
                    THEN  D  -1
                    THEN  Try  ((Fold  `archive-event`  0  THEN  Auto  THEN  OrLeft  THEN  Auto))
                    THEN  RepeatFor  2  (D  -1)
                    THEN  Fold  `consensus-message`  0
                    THEN  Auto
                    THEN  OrRight
                    THEN  Auto)]
)

---

Home Index