---

Step * of Lemma es-search-back-cases

∀[es:EO]. ∀[e:E]. ∀[f:{e':E| e' ≤loc e }  ─→ (Top + Top)].
  (es-search-back(es;x.f[x];e) ~ if isl(f[e]) then f[e]
  if first(e) then inr ⋅ 
  else es-search-back(es;x.f[x];pred(e))
  fi )
BY
{ ((UnivCD THENA Auto)
   THEN RW (AddrC [1] UnfoldTopAbC) 0
   THEN RecUnfold `gensearch` 0
   THEN Reduce 0
   THEN Fold `es-search-back` 0
   THEN (GenConclAtAddr [1;1] THENA Auto)
   THEN D -2
   THEN Reduce 0
   THEN Try (Trivial)
   THEN Unfold `es-pred?` 0
   THEN AutoSplit) }

---

Latex:


\mforall{}[es:EO].  \mforall{}[e:E].  \mforall{}[f:\{e':E|  e'  \mleq{}loc  e  \}    {}\mrightarrow{}  (Top  +  Top)].
    (es-search-back(es;x.f[x];e)  \msim{}  if  isl(f[e])  then  f[e]
    if  first(e)  then  inr  \mcdot{} 
    else  es-search-back(es;x.f[x];pred(e))
    fi  )


By

((UnivCD  THENA  Auto)
  THEN  RW  (AddrC  [1]  UnfoldTopAbC)  0
  THEN  RecUnfold  `gensearch`  0
  THEN  Reduce  0
  THEN  Fold  `es-search-back`  0
  THEN  (GenConclAtAddr  [1;1]  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0
  THEN  Try  (Trivial)
  THEN  Unfold  `es-pred?`  0
  THEN  AutoSplit)

---

Home Index