---

Step * 1 of Lemma es-search-back_wf


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

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. x : E@i
7. (x <loc a)@i
8. x = pred(a) ∈ E@i
9. True@i
⊢ es-rank(es;x) < es-rank(es;a)

---

Latex:



1.  es  :  EO
2.  T  :  Type
3.  e  :  E
4.  f  :  \{e':E|  e'  \mleq{}loc  e  \}    {}\mrightarrow{}  (T  +  Top)
5.  a  :  \{e':E|  e'  \mleq{}loc  e  \}  @i
6.  \muparrow{}isl(es-pred?(es;a))@i
\mvdash{}  es-rank(es;outl(es-pred?(es;a)))  <  es-rank(es;a)


By

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

---

Home Index