Step
*
1
2
1
of Lemma
es-last-event_wf
1. es : EO
2. e : E@i
3. ¬↑first(e)
4. ∀e1:E
((e1 < e)
⇒ (∀P:{e':E| e' ≤loc e1 } ─→ 𝔹
(es-last-event(es;P;e1) ∈ (∃e':{E| (e' ≤loc e1
∧ (↑(P e'))
∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc e1 ⇒ (¬↑(P e'')))))})
∨ (¬(∃e':{E| (e' ≤loc e1 ∧ (↑(P e')))})))))
5. P : {e':E| e' ≤loc e } ─→ 𝔹@i
6. ¬↑(P e)
7. es-last-event(es;P;pred(e)) ∈ (∃e':{E| (e' ≤loc pred(e)
∧ (↑(P e'))
∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc pred(e) ⇒ (¬↑(P e'')))))})
∨ (¬(∃e':{E| (e' ≤loc pred(e) ∧ (↑(P e')))}))
8. loc(pred(e)) = loc(e) ∈ Id
9. (pred(e) < e)
10. ∀e':E. (e' < e) ⇒ ((e' = pred(e) ∈ E) ∨ (e' < pred(e))) supposing loc(e') = loc(e) ∈ Id
11. (pred(e) <loc e)
⊢ es-last-event(es;P;pred(e)) ∈ (∃e':{E| (e' ≤loc e
∧ (↑(P e'))
∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc e ⇒ (¬↑(P e'')))))})
∨ (¬(∃e':{E| (e' ≤loc e ∧ (↑(P e')))}))
BY
{ ((DoSubsume THEN Auto)
THEN Try ((DVarSets THEN RepD))
THEN Repeat ((MemTypeCD THEN Auto))
THEN Try (Complete (((BLemma `es-le_weakening` THEN Auto)
THEN Using [`b',⌈pred(e)⌉] (BLemma `es-le-trans2`)⋅
THEN Auto)))
THEN Try (Complete ((D (-1) THEN Try (Complete (Auto)) THEN Try (Complete ((BackThruSomeHyp THEN Auto))))))
THEN Try (Complete ((D (-2) THEN Auto))))⋅ }
1
1. es : EO
2. e : E@i
3. ¬↑first(e)
4. ∀e1:E
((e1 < e)
⇒ (∀P:{e':E| e' ≤loc e1 } ─→ 𝔹
(es-last-event(es;P;e1) ∈ (∃e':{E| (e' ≤loc e1
∧ (↑(P e'))
∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc e1 ⇒ (¬↑(P e'')))))})
∨ (¬(∃e':{E| (e' ≤loc e1 ∧ (↑(P e')))})))))
5. P : {e':E| e' ≤loc e } ─→ 𝔹@i
6. ¬↑(P e)
7. es-last-event(es;P;pred(e)) ∈ (∃e':{E| (e' ≤loc pred(e)
∧ (↑(P e'))
∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc pred(e) ⇒ (¬↑(P e'')))))})
∨ (¬(∃e':{E| (e' ≤loc pred(e) ∧ (↑(P e')))}))
8. loc(pred(e)) = loc(e) ∈ Id
9. (pred(e) < e)
10. ∀e':E. (e' < e) ⇒ ((e' = pred(e) ∈ E) ∨ (e' < pred(e))) supposing loc(e') = loc(e) ∈ Id
11. (pred(e) <loc e)
12. es-last-event(es;P;pred(e))
= es-last-event(es;P;pred(e))
∈ ((∃e':{E| (e' ≤loc pred(e) ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc pred(e) ⇒ (¬↑(P e'')))))})
∨ (¬(∃e':{E| (e' ≤loc pred(e) ∧ (↑(P e')))})))
13. x : ∃e':{E| (e' ≤loc pred(e)
∧ (↑(P e'))
∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc pred(e) ⇒ (¬↑(P e'')))))} + (¬(∃e':{E| (e' ≤loc pred(e)
∧ (↑(P e')))}))@i
⊢ x ∈ ∃e':{E| (e' ≤loc e ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc e ⇒ (¬↑(P e'')))))} + (¬(∃e':{E
(e' ≤loc e
∧ (↑(P e')))}))
Latex:
1. es : EO
2. e : E@i
3. \mneg{}\muparrow{}first(e)
4. \mforall{}e1:E
((e1 < e)
{}\mRightarrow{} (\mforall{}P:\{e':E| e' \mleq{}loc e1 \} {}\mrightarrow{} \mBbbB{}
(es-last-event(es;P;e1) \mmember{} (\mexists{}e':\{E| (e' \mleq{}loc e1
\mwedge{} (\muparrow{}(P e'))
\mwedge{} (\mforall{}e'':E
((e' <loc e'')
{}\mRightarrow{} e'' \mleq{}loc e1
{}\mRightarrow{} (\mneg{}\muparrow{}(P e'')))))\})
\mvee{} (\mneg{}(\mexists{}e':\{E| (e' \mleq{}loc e1 \mwedge{} (\muparrow{}(P e')))\})))))
5. P : \{e':E| e' \mleq{}loc e \} {}\mrightarrow{} \mBbbB{}@i
6. \mneg{}\muparrow{}(P e)
7. es-last-event(es;P;pred(e)) \mmember{} (\mexists{}e':\{E| (e' \mleq{}loc pred(e)
\mwedge{} (\muparrow{}(P e'))
\mwedge{} (\mforall{}e'':E
((e' <loc e'')
{}\mRightarrow{} e'' \mleq{}loc pred(e)
{}\mRightarrow{} (\mneg{}\muparrow{}(P e'')))))\})
\mvee{} (\mneg{}(\mexists{}e':\{E| (e' \mleq{}loc pred(e) \mwedge{} (\muparrow{}(P e')))\}))
8. loc(pred(e)) = loc(e)
9. (pred(e) < e)
10. \mforall{}e':E. (e' < e) {}\mRightarrow{} ((e' = pred(e)) \mvee{} (e' < pred(e))) supposing loc(e') = loc(e)
11. (pred(e) <loc e)
\mvdash{} es-last-event(es;P;pred(e)) \mmember{} (\mexists{}e':\{E| (e' \mleq{}loc e
\mwedge{} (\muparrow{}(P e'))
\mwedge{} (\mforall{}e'':E
((e' <loc e'') {}\mRightarrow{} e'' \mleq{}loc e {}\mRightarrow{} (\mneg{}\muparrow{}(P e'')))))\})
\mvee{} (\mneg{}(\mexists{}e':\{E| (e' \mleq{}loc e \mwedge{} (\muparrow{}(P e')))\}))
By
((DoSubsume THEN Auto)
THEN Try ((DVarSets THEN RepD))
THEN Repeat ((MemTypeCD THEN Auto))
THEN Try (Complete (((BLemma `es-le\_weakening` THEN Auto)
THEN Using [`b',\mkleeneopen{}pred(e)\mkleeneclose{}] (BLemma `es-le-trans2`)\mcdot{}
THEN Auto)))
THEN Try (Complete ((D (-1)
THEN Try (Complete (Auto))
THEN Try (Complete ((BackThruSomeHyp THEN Auto))))))
THEN Try (Complete ((D (-2) THEN Auto))))\mcdot{}
Home
Index