---

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

∀es:EO
  ∀[T:Type]
    ∀e:E. ∀f:{e':E| e' ≤loc e }  ─→ (T + Top).
      (↑can-apply(λe.es-search-back(es;x.f[x];e);e) ⇐⇒ ∃e'≤e.↑can-apply(λx.f[x];e'))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN (Unfold `can-apply` 0 THEN Reduce 0)
   THEN (InstLemma `isl-es-search-back` [⌈es⌉;⌈T⌉]⋅ THENA Auto)) }

1
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']))

---

Latex:


\mforall{}es:EO
    \mforall{}[T:Type]
        \mforall{}e:E.  \mforall{}f:\{e':E|  e'  \mleq{}loc  e  \}    {}\mrightarrow{}  (T  +  Top).
            (\muparrow{}can-apply(\mlambda{}e.es-search-back(es;x.f[x];e);e)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}e'\mleq{}e.\muparrow{}can-apply(\mlambda{}x.f[x];e'))


By

(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (Unfold  `can-apply`  0  THEN  Reduce  0)
  THEN  (InstLemma  `isl-es-search-back`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index