---

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:


\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

(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