---

Step * 1 2 1 of Lemma es-maximal-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)
     ⇒ ((∃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
7. ¬P[j]
8. ¬↑first(j)
⊢ (∃m:E. (m ≤loc j  ∧ P[m] ∧ (∀e':E. ((m <loc e') ⇒ e' ≤loc j  ⇒ (¬P[e']))))) ∨ (∀e':E. (e' ≤loc j  ⇒ (¬P[e'])))
BY
{ ((InstHyp [⌈pred(j)⌉] (-3)⋅ THENA Auto) THEN RepeatFor 2 (ParallelLast) THEN 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
7. ¬P[j]
8. ¬↑first(j)
9. m : E
10. m ≤loc pred(j) 
11. P[m]
12. ∀e':E. ((m <loc e') ⇒ e' ≤loc pred(j)  ⇒ (¬P[e']))
13. m ≤loc j 
14. P[m]
15. e' : E@i
16. (m <loc e')@i
17. e' ≤loc j @i
⊢ ¬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)
     ⇒ ((∃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
7. ¬P[j]
8. ¬↑first(j)
9. ∀e':E. (e' ≤loc pred(j)  ⇒ (¬P[e']))
10. e' : E@i
11. e' ≤loc pred(j)  ⇒ (¬P[e'])
12. e' ≤loc j @i
⊢ ¬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{}  ((\mexists{}m:E.  (m  \mleq{}loc  k    \mwedge{}  P[m]  \mwedge{}  (\mforall{}e':E.  ((m  <loc  e')  {}\mRightarrow{}  e'  \mleq{}loc  k    {}\mRightarrow{}  (\mneg{}P[e'])))))
                \mvee{}  (\mforall{}e':E.  (e'  \mleq{}loc  k    {}\mRightarrow{}  (\mneg{}P[e'])))))@i
7.  \mneg{}P[j]
8.  \mneg{}\muparrow{}first(j)
\mvdash{}  (\mexists{}m:E.  (m  \mleq{}loc  j    \mwedge{}  P[m]  \mwedge{}  (\mforall{}e':E.  ((m  <loc  e')  {}\mRightarrow{}  e'  \mleq{}loc  j    {}\mRightarrow{}  (\mneg{}P[e'])))))
\mvee{}  (\mforall{}e':E.  (e'  \mleq{}loc  j    {}\mRightarrow{}  (\mneg{}P[e'])))


By

((InstHyp  [\mkleeneopen{}pred(j)\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)  THEN  RepeatFor  2  (ParallelLast)  THEN  Auto)

---

Home Index