---

Step * 1 of Lemma can-apply-es-search-back


1. es : EO@i'
2. [T] : Type
3. ∀e:E. ∀f:{e':E| e' ≤loc e }  ─→ (T + Top).  (↑isl(es-search-back(es;x.f[x];e)) ⇐⇒ ∃e'≤e.↑isl(f[e']))
⊢ ∀e:E. ∀f:{e':E| e' ≤loc e }  ─→ (T + Top).  (↑isl(es-search-back(es;x.f[x];e)) ⇐⇒ ∃e'≤e.↑isl(f[e']))
BY
{ Trivial }

---

Latex:



1.  es  :  EO@i'
2.  [T]  :  Type
3.  \mforall{}e:E.  \mforall{}f:\{e':E|  e'  \mleq{}loc  e  \}    {}\mrightarrow{}  (T  +  Top).
          (\muparrow{}isl(es-search-back(es;x.f[x];e))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}e'\mleq{}e.\muparrow{}isl(f[e']))
\mvdash{}  \mforall{}e:E.  \mforall{}f:\{e':E|  e'  \mleq{}loc  e  \}    {}\mrightarrow{}  (T  +  Top).
        (\muparrow{}isl(es-search-back(es;x.f[x];e))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}e'\mleq{}e.\muparrow{}isl(f[e']))


By

Trivial

---

Home Index