---

Step * 1 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. 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)
BY
{ (BLemma `es-rank_property` THEN Auto) }

---

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


By

(BLemma  `es-rank\_property`  THEN  Auto)

---

Home Index