---

Step * of Lemma implies-es-pred2

∀[es:EO]. ∀[e,e':E].  (e' = pred(e) ∈ E) supposing ((e' <loc e) and pred(e) ≤loc e'  and (¬↑first(e)))
BY
{ (((Auto
     THEN BLemma `implies-es-pred`
     THEN Auto
     THEN (InstESAxiom ⌈es⌉ [⌈e⌉] 5)⋅
     THEN Auto
     THEN (InstHyp [⌈e1⌉] (-1))⋅)
    THENA Auto
    )
   THEN ParallelLast
   THEN ParallelLast) }

1
1. es : EO
2. e : E
3. e' : E
4. ¬↑first(e)
5. pred(e) ≤loc e' 
6. (e' <loc e)
7. (e' <loc e)
8. e1 : E@i
9. (pred(e) <loc e)
10. ∀e':E. (¬((pred(e) <loc e') ∧ (e' <loc e)))
11. (e1 <loc e)@i
12. (e' <loc e1)@i
⊢ (pred(e) <loc e1)

---

Latex:


\mforall{}[es:EO].  \mforall{}[e,e':E].    (e'  =  pred(e))  supposing  ((e'  <loc  e)  and  pred(e)  \mleq{}loc  e'    and  (\mneg{}\muparrow{}first(e)))


By

(((Auto
      THEN  BLemma  `implies-es-pred`
      THEN  Auto
      THEN  (InstESAxiom  \mkleeneopen{}es\mkleeneclose{}  [\mkleeneopen{}e\mkleeneclose{}]  5)\mcdot{}
      THEN  Auto
      THEN  (InstHyp  [\mkleeneopen{}e1\mkleeneclose{}]  (-1))\mcdot{})
    THENA  Auto
    )
  THEN  ParallelLast
  THEN  ParallelLast)

---

Home Index