---

Step * 1 of Lemma es-loc-pred-plus


1. es : EO
2. ∀n:ℕ. ∀x,y:E.  ((λx,y. ((¬↑first(y)) c∧ (x = pred(y) ∈ E))^n x y) ⇒ (loc(x) = loc(y) ∈ Id))
⊢ ∀[x,y:E].  loc(x) = loc(y) ∈ Id supposing ∃n:ℕ+. (λx,y. ((¬↑first(y)) c∧ (x = pred(y) ∈ E))^n x y)
BY
{ (((Auto THEN ExRepD THEN (InstHyp [⌈n⌉] 2)⋅) THENA Auto) THEN (BHyp (-1)) THEN Auto) }

---

Latex:



1.  es  :  EO
2.  \mforall{}n:\mBbbN{}.  \mforall{}x,y:E.    ((rel\_exp(E;  \mlambda{}x,y.  ((\mneg{}\muparrow{}first(y))  c\mwedge{}  (x  =  pred(y)));  n)  x  y)  {}\mRightarrow{}  (loc(x)  =  loc(y)))
\mvdash{}  \mforall{}[x,y:E].    loc(x)  =  loc(y)  supposing  \mexists{}n:\mBbbN{}\msupplus{}.  (rel\_exp(E;  \mlambda{}x,y.  ((\mneg{}\muparrow{}first(y))  c\mwedge{}  (x  =  pred(y)));  n)  \000Cx  y)


By

(((Auto  THEN  ExRepD  THEN  (InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  2)\mcdot{})  THENA  Auto)  THEN  (BHyp  (-1))  THEN  Auto)

---

Home Index