---

Step * 1 of Lemma isl-es-search-back


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'])))
BY
{ ((GenConclAtAddr [1;1;1;1;1] THENA Auto) THEN D -2 THEN Reduce 0) }

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
6. x : T@i
7. f[e] = (inl x) ∈ (T + Top)@i
⊢ True ⇐⇒ ∃e':E. (e' ≤loc e  c∧ (↑isl(f[e'])))

2
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
6. y : Top@i
7. f[e] = (inr y ) ∈ (T + Top)@i
⊢ ↑isl(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:



1.  es  :  EO@i'
2.  [T]  :  Type
3.  e  :  E@i
4.  \mforall{}e1:E
          ((e1  <  e)
          {}\mRightarrow{}  (\mforall{}f:\{e':E|  e'  \mleq{}loc  e1  \}    {}\mrightarrow{}  (T  +  Top)
                      (\muparrow{}isl(es-search-back(es;x.f[x];e1))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}e':E.  (e'  \mleq{}loc  e1    c\mwedge{}  (\muparrow{}isl(f[e']))))))
5.  f  :  \{e':E|  e'  \mleq{}loc  e  \}    {}\mrightarrow{}  (T  +  Top)@i
\mvdash{}  \muparrow{}isl(if  isl(f[e])  then  f[e]
    if  first(e)  then  inr  \mcdot{} 
    else  es-search-back(es;x.f[x];pred(e))
    fi  )
\mLeftarrow{}{}\mRightarrow{}  \mexists{}e':E.  (e'  \mleq{}loc  e    c\mwedge{}  (\muparrow{}isl(f[e'])))


By

((GenConclAtAddr  [1;1;1;1;1]  THENA  Auto)  THEN  D  -2  THEN  Reduce  0)

---

Home Index