---

Step * 1 of Lemma es-minimal-event


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'])))))
BY
{ ((InstLemma `decidable__existse-before` [⌈es⌉;⌈j⌉;⌈P⌉]⋅ THENA (Auto THEN D 0 THEN Auto)) THEN D -1) }

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
7. ∃e<j.P[e]
⊢ P[j] ⇒ (∃m:E. (m ≤loc j  ∧ P[m] ∧ (∀e':E. ((e' <loc m) ⇒ (¬P[e'])))))

2
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
7. ¬∃e<j.P[e]
⊢ P[j] ⇒ (∃m:E. (m ≤loc j  ∧ P[m] ∧ (∀e':E. ((e' <loc m) ⇒ (¬P[e'])))))

---

Latex:



1.  es  :  EO@i'
2.  [P]  :  E  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}e:E.  Dec(P[e])@i
4.  WellFnd\{i\}(E;x,y.(x  <  y))
5.  j  :  E@i
6.  \mforall{}k:E.  ((k  <  j)  {}\mRightarrow{}  P[k]  {}\mRightarrow{}  (\mexists{}m:E.  (m  \mleq{}loc  k    \mwedge{}  P[m]  \mwedge{}  (\mforall{}e':E.  ((e'  <loc  m)  {}\mRightarrow{}  (\mneg{}P[e']))))))@i
\mvdash{}  P[j]  {}\mRightarrow{}  (\mexists{}m:E.  (m  \mleq{}loc  j    \mwedge{}  P[m]  \mwedge{}  (\mforall{}e':E.  ((e'  <loc  m)  {}\mRightarrow{}  (\mneg{}P[e'])))))


By

((InstLemma  `decidable\_\_existse-before`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{}]\mcdot{}  THENA  (Auto  THEN  D  0  THEN  Auto))  THEN  D  -1)

---

Home Index