---

Step * of Lemma test-es-first-reasoning

∀es:EO. ∀e1,e2:E.  (e1 ≤loc e2  ⇒ (¬↑first(e1)) ⇒ (¬↑first(e2)))
BY
{ Auto }

---

Latex:


\mforall{}es:EO.  \mforall{}e1,e2:E.    (e1  \mleq{}loc  e2    {}\mRightarrow{}  (\mneg{}\muparrow{}first(e1))  {}\mRightarrow{}  (\mneg{}\muparrow{}first(e2)))


By

Auto

---

Home Index