---

Step * of Lemma es-next

∀es:EO. ∀e,a:E.  ((a <loc e) ⇒ (∃b:E. ((¬↑first(b)) c∧ ((a = pred(b) ∈ E) ∧ b ≤loc e ))))
BY
{ ((((D 0 THENA Auto) THEN LocLessInd THEN Auto THEN (RWO "es-locl-iff" (-1))) THENA Auto)
   THEN (D (-1))
   THEN (D (-1))) }

1
1. es : EO@i'
2. WellFnd{i}(E;x,y.(x <loc y))
3. j : E@i
4. ∀k:E. ((k <loc j) ⇒ (∀a:E. ((a <loc k) ⇒ (∃b:E. ((¬↑first(b)) c∧ ((a = pred(b) ∈ E) ∧ b ≤loc k ))))))@i
5. a : E@i
6. ¬↑first(j)
7. a = pred(j) ∈ E
⊢ ∃b:E. ((¬↑first(b)) c∧ ((a = pred(b) ∈ E) ∧ b ≤loc j ))

2
1. es : EO@i'
2. WellFnd{i}(E;x,y.(x <loc y))
3. j : E@i
4. ∀k:E. ((k <loc j) ⇒ (∀a:E. ((a <loc k) ⇒ (∃b:E. ((¬↑first(b)) c∧ ((a = pred(b) ∈ E) ∧ b ≤loc k ))))))@i
5. a : E@i
6. ¬↑first(j)
7. (a <loc pred(j))
⊢ ∃b:E. ((¬↑first(b)) c∧ ((a = pred(b) ∈ E) ∧ b ≤loc j ))

---

Latex:

---

Latex:
\mforall{}es:EO.  \mforall{}e,a:E.    ((a  <loc  e)  {}\mRightarrow{}  (\mexists{}b:E.  ((\mneg{}\muparrow{}first(b))  c\mwedge{}  ((a  =  pred(b))  \mwedge{}  b  \mleq{}loc  e  ))))


By

---

Latex:
((((D  0  THENA  Auto)  THEN  LocLessInd  THEN  Auto  THEN  (RWO  "es-locl-iff"  (-1)))  THENA  Auto)
  THEN  (D  (-1))
  THEN  (D  (-1)))

---

Home Index