---

Step * of Lemma prior-val-all-events

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[e:E].  prior(E)(e) = pred(e) ∈ E supposing ¬↑first(e)
BY
{ (Auto
   THEN (RepUR ``eclass-val in-eclass es-prior-interface`` 0
         THEN RepUR ``can-apply do-apply es-all-events local-pred-class`` 0
         )
   THEN RecUnfold `es-local-pred` 0
   THEN Reduce 0
   THEN AutoBoolCase ⌜first(e)⌝⋅) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].    prior(E)(e)  =  pred(e)  supposing  \mneg{}\muparrow{}first(e)


By

---

Latex:
(Auto
  THEN  (RepUR  ``eclass-val  in-eclass  es-prior-interface``  0
              THEN  RepUR  ``can-apply  do-apply  es-all-events  local-pred-class``  0
              )
  THEN  RecUnfold  `es-local-pred`  0
  THEN  Reduce  0
  THEN  AutoBoolCase  \mkleeneopen{}first(e)\mkleeneclose{}\mcdot{})

---

Home Index