---

Step * of Lemma es-search-back_wf

∀[es:EO]. ∀[T:Type]. ∀[e:E]. ∀[f:{e':E| e' ≤loc e }  ⟶ (T + Top)].  (es-search-back(es;x.f[x];e) ∈ T + Top)
BY
{ (ProveWfLemma
   THEN InstLemma `gensearch_wf` [⌜{e':E| e' ≤loc e } ⌝;⌜T⌝;⌜λe.es-rank(es;e)⌝;⌜λx.f[x]⌝;⌜λe.es-pred?(es;e)⌝;⌜e⌝]⋅
   THEN Auto
   THEN All Reduce) }

1
1. es : EO
2. T : Type
3. e : E
4. f : {e':E| e' ≤loc e }  ⟶ (T + Top)
5. a : {e':E| e' ≤loc e } @i
6. ↑isl(es-pred?(es;a))@i
⊢ es-rank(es;outl(es-pred?(es;a))) < es-rank(es;a)

---

Latex:

---

Latex:
\mforall{}[es:EO].  \mforall{}[T:Type].  \mforall{}[e:E].  \mforall{}[f:\{e':E|  e'  \mleq{}loc  e  \}    {}\mrightarrow{}  (T  +  Top)].
    (es-search-back(es;x.f[x];e)  \mmember{}  T  +  Top)


By

---

Latex:
(ProveWfLemma
  THEN  InstLemma  `gensearch\_wf`  [\mkleeneopen{}\{e':E|  e'  \mleq{}loc  e  \}  \mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mlambda{}e.es-rank(es;e)\mkleeneclose{};\mkleeneopen{}\mlambda{}x.f[x]\mkleeneclose{};
  \mkleeneopen{}\mlambda{}e.es-pred?(es;e)\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  All  Reduce)

---

Home Index