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:
\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
(CausalInd THENA Auto)
Home
Index