---

Step * of Lemma es-pred-exists-between2

∀es:EO. ∀e1,e2:E.  ((e1 <loc e2) ⇒ (∃e:{e:E| ¬↑first(e)} . ((e1 = pred(e) ∈ E) ∧ e ≤loc e2 )))
BY
{ (Auto
   THEN (FLemma `es-pred-exists-between` [-1] THENA Auto)
   THEN ExRepD
   THEN InstConcl [⌈e⌉]⋅
   THEN Auto
   THEN InstLemma `es-pred_property` [⌈es⌉;⌈e2⌉]⋅
   THEN Auto
   THEN (InstHyp [⌈e1⌉] (-1)⋅ THENA Auto)
   THEN D (-1)) }

1
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 

2
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 ≤loc e2 

---

Latex:


\mforall{}es:EO.  \mforall{}e1,e2:E.    ((e1  <loc  e2)  {}\mRightarrow{}  (\mexists{}e:\{e:E|  \mneg{}\muparrow{}first(e)\}  .  ((e1  =  pred(e))  \mwedge{}  e  \mleq{}loc  e2  )))


By

(Auto
  THEN  (FLemma  `es-pred-exists-between`  [-1]  THENA  Auto)
  THEN  ExRepD
  THEN  InstConcl  [\mkleeneopen{}e\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  InstLemma  `es-pred\_property`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}e1\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  D  (-1))

---

Home Index