---

Step * 1 of Lemma es-pred-exists-between2


1. es : EO@i'
2. e1 : E@i
3. e2 : E@i
4. (e1 <loc e2)@i
5. e : {e:E| ¬↑first(e)} 
6. e1 = pred(e) ∈ E
7. e1 = pred(e) ∈ E
8. loc(pred(e2)) = loc(e2) ∈ Id
9. (pred(e2) < e2)
10. ∀e':E. (e' < e2) ⇒ ((e' = pred(e2) ∈ E) ∨ (e' < pred(e2))) supposing loc(e') = loc(e2) ∈ Id
11. e1 = pred(e2) ∈ E
⊢ e ≤loc e2 
BY
{ ((HypSubst' (-5) (-1) THENA Auto) THEN FLemma `es-pred-one-one` [-1] THEN Auto) }

---

Latex:



1.  es  :  EO@i'
2.  e1  :  E@i
3.  e2  :  E@i
4.  (e1  <loc  e2)@i
5.  e  :  \{e:E|  \mneg{}\muparrow{}first(e)\} 
6.  e1  =  pred(e)
7.  e1  =  pred(e)
8.  loc(pred(e2))  =  loc(e2)
9.  (pred(e2)  <  e2)
10.  \mforall{}e':E.  (e'  <  e2)  {}\mRightarrow{}  ((e'  =  pred(e2))  \mvee{}  (e'  <  pred(e2)))  supposing  loc(e')  =  loc(e2)
11.  e1  =  pred(e2)
\mvdash{}  e  \mleq{}loc  e2 


By

((HypSubst'  (-5)  (-1)  THENA  Auto)  THEN  FLemma  `es-pred-one-one`  [-1]  THEN  Auto)

---

Home Index