---

Step * of Lemma es-minimal-event

∀es:EO
  ∀[P:E ⟶ ℙ]. ((∀e:E. Dec(P[e])) ⇒ (∀e:E. (P[e] ⇒ (∃m:E. (m ≤loc e  ∧ P[m] ∧ (∀e':E. ((e' <loc m) ⇒ (¬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) ⇒ P[k] ⇒ (∃m:E. (m ≤loc k  ∧ P[m] ∧ (∀e':E. ((e' <loc m) ⇒ (¬P[e']))))))@i
⊢ P[j] ⇒ (∃m:E. (m ≤loc j  ∧ P[m] ∧ (∀e':E. ((e' <loc m) ⇒ (¬P[e'])))))

---

Latex:

---

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


By

---

Latex:
(CausalInd  THENA  Auto)

---

Home Index