---

Step * of Lemma isl-es-search-back

∀es:EO. ∀[T:Type]. ∀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
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN Unfold `existse-le` 0
   THEN CausalInd'
   THEN (D 0 THENA Auto)
   THEN (RWO "es-search-back-cases" 0 THENA Auto)) }

1
1. es : EO@i'
2. [T] : Type
3. e : E@i
4. ∀e1:E
     ((e1 < e)
     ⇒ (∀f:{e':E| e' ≤loc e1 }  ─→ (T + Top)
           (↑isl(es-search-back(es;x.f[x];e1)) ⇐⇒ ∃e':E. (e' ≤loc e1  c∧ (↑isl(f[e']))))))
5. f : {e':E| e' ≤loc e }  ─→ (T + Top)@i
⊢ ↑isl(if isl(f[e]) then f[e]
  if first(e) then inr ⋅ 
  else es-search-back(es;x.f[x];pred(e))
  fi )
⇐⇒ ∃e':E. (e' ≤loc e  c∧ (↑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{}isl(es-search-back(es;x.f[x];e))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}e'\mleq{}e.\muparrow{}isl(f[e']))


By

(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  Unfold  `existse-le`  0
  THEN  CausalInd'
  THEN  (D  0  THENA  Auto)
  THEN  (RWO  "es-search-back-cases"  0  THENA  Auto))

---

Home Index