---

Step * of Lemma existse-before-iff

∀es:EO. ∀e':E.
  ∀[P:{e:E| loc(e) = loc(e') ∈ Id}  ⟶ ℙ]. (∃e<e'.P[e] ⇐⇒ (¬↑first(e')) c∧ (P[pred(e')] ∨ ∃e<pred(e').P[e]))
BY
{ (Auto THEN (All (Unfold `existse-before`)) THEN ExRepD) }

1
1. es : EO@i'
2. e' : E@i
3. P : {e:E| loc(e) = loc(e') ∈ Id}  ⟶ ℙ
4. e : E@i
5. (e <loc e')@i
6. P[e]@i
⊢ ¬↑first(e')

2
1. es : EO@i'
2. e' : E@i
3. [P] : {e:E| loc(e) = loc(e') ∈ Id}  ⟶ ℙ
4. e : E@i
5. (e <loc e')@i
6. P[e]@i
⊢ P[pred(e')] ∨ (∃e:E. ((e <loc pred(e')) c∧ P[e]))

3
1. es : EO@i'
2. e' : E@i
3. [P] : {e:E| loc(e) = loc(e') ∈ Id}  ⟶ ℙ
4. ¬↑first(e')@i
5. P[pred(e')] ∨ (∃e:E. ((e <loc pred(e')) c∧ P[e]))@i
⊢ ∃e:E. ((e <loc e') c∧ P[e])

---

Latex:

---

Latex:
\mforall{}es:EO.  \mforall{}e':E.
    \mforall{}[P:\{e:E|  loc(e)  =  loc(e')\}    {}\mrightarrow{}  \mBbbP{}]
        (\mexists{}e<e'.P[e]  \mLeftarrow{}{}\mRightarrow{}  (\mneg{}\muparrow{}first(e'))  c\mwedge{}  (P[pred(e')]  \mvee{}  \mexists{}e<pred(e').P[e]))


By

---

Latex:
(Auto  THEN  (All  (Unfold  `existse-before`))  THEN  ExRepD)

---

Home Index