---

Step * of Lemma es-maximal-event

∀es:EO
  ∀[P:E ⟶ ℙ]
    ((∀e:E. Dec(P[e]))
    ⇒ (∀e:E
          ((∃m:E. (m ≤loc e  ∧ P[m] ∧ (∀e':E. ((m <loc e') ⇒ e' ≤loc e  ⇒ (¬P[e'])))))
          ∨ (∀e':E. (e' ≤loc e  ⇒ (¬P[e']))))))
BY
{ (CausalInd THENA Auto) }

1
1. es : EO@i'
2. [P] : E ⟶ ℙ
3. ∀e:E. Dec(P[e])@i
4. WellFnd{i}(E;x,y.(x < y))
5. j : E@i
6. ∀k:E
     ((k < j)
     ⇒ ((∃m:E. (m ≤loc k  ∧ P[m] ∧ (∀e':E. ((m <loc e') ⇒ e' ≤loc k  ⇒ (¬P[e'])))))
        ∨ (∀e':E. (e' ≤loc k  ⇒ (¬P[e'])))))@i
⊢ (∃m:E. (m ≤loc j  ∧ P[m] ∧ (∀e':E. ((m <loc e') ⇒ e' ≤loc j  ⇒ (¬P[e']))))) ∨ (∀e':E. (e' ≤loc j  ⇒ (¬P[e'])))

---

Latex:

---

Latex:
\mforall{}es:EO
    \mforall{}[P:E  {}\mrightarrow{}  \mBbbP{}]
        ((\mforall{}e:E.  Dec(P[e]))
        {}\mRightarrow{}  (\mforall{}e:E
                    ((\mexists{}m:E.  (m  \mleq{}loc  e    \mwedge{}  P[m]  \mwedge{}  (\mforall{}e':E.  ((m  <loc  e')  {}\mRightarrow{}  e'  \mleq{}loc  e    {}\mRightarrow{}  (\mneg{}P[e'])))))
                    \mvee{}  (\mforall{}e':E.  (e'  \mleq{}loc  e    {}\mRightarrow{}  (\mneg{}P[e']))))))


By

---

Latex:
(CausalInd  THENA  Auto)

---

Home Index