Step
*
1
1
2
2
1
1
of Lemma
es-local-pred_wf2
1. Info : Type@i'
2. es : EO+(Info)@i'
3. e : E@i
4. ∀e1:E
((e1 < e)
⇒ (∀P:{e':E| (e' <loc e1)} ─→ 𝔹
(last(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 pred(e))
7. ¬↑first(e)
8. last(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')))}))
9. (last(P) pred(e))
= (last(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')))})))
⊢ ((∃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')))}))) ⊆r ((∃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
{ (Unfold `or` 0 THEN BLemma `subtype_rel_union` THEN Auto THEN SubtypeReasoning THEN Auto) }
1
1. Info : Type@i'
2. es : EO+(Info)@i'
3. e : E@i
4. ∀e1:E
((e1 < e)
⇒ (∀P:{e':E| (e' <loc e1)} ─→ 𝔹
(last(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 pred(e))
7. ¬↑first(e)
8. last(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')))}))
9. (last(P) pred(e))
= (last(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')))})))
10. e' : E@i
11. (e' <loc pred(e))@i
12. ↑(P e')@i
13. ∀e'':E. ((e' <loc e'') ⇒ (e'' <loc pred(e)) ⇒ (¬↑(P e'')))@i
14. e'' : E@i
15. (e' <loc e'')@i
16. (e'' <loc e)@i
⊢ ¬↑(P e'')
2
1. Info : Type@i'
2. es : EO+(Info)@i'
3. e : E@i
4. ∀e1:E
((e1 < e)
⇒ (∀P:{e':E| (e' <loc e1)} ─→ 𝔹
(last(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 pred(e))
7. ¬↑first(e)
8. last(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')))}))
9. (last(P) pred(e))
= (last(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')))})))
10. ∃e':{E| ((e' <loc e) ∧ (↑(P e')))}@i
⊢ ↓∃e':{E| ((e' <loc pred(e)) ∧ (↑(P e')))}
Latex:
Latex:
1. Info : Type@i'
2. es : EO+(Info)@i'
3. e : E@i
4. \mforall{}e1:E
((e1 < e)
{}\mRightarrow{} (\mforall{}P:\{e':E| (e' <loc e1)\} {}\mrightarrow{} \mBbbB{}
(last(P) e1 \mmember{} (\mexists{}e':\{E| ((e' <loc e1)
\mwedge{} (\muparrow{}(P e'))
\mwedge{} (\mforall{}e'':E. ((e' <loc e'') {}\mRightarrow{} (e'' <loc e1) {}\mRightarrow{} (\mneg{}\muparrow{}(P e'')))))\})
\mvee{} (\mneg{}(\mexists{}e':\{E| ((e' <loc e1) \mwedge{} (\muparrow{}(P e')))\})))))
5. P : \{e':E| (e' <loc e)\} {}\mrightarrow{} \mBbbB{}@i
6. \mneg{}\muparrow{}(P pred(e))
7. \mneg{}\muparrow{}first(e)
8. last(P) pred(e) \mmember{} (\mexists{}e':\{E| ((e' <loc pred(e))
\mwedge{} (\muparrow{}(P e'))
\mwedge{} (\mforall{}e'':E. ((e' <loc e'') {}\mRightarrow{} (e'' <loc pred(e)) {}\mRightarrow{} (\mneg{}\muparrow{}(P e'')))))\})
\mvee{} (\mneg{}(\mexists{}e':\{E| ((e' <loc pred(e)) \mwedge{} (\muparrow{}(P e')))\}))
9. (last(P) pred(e)) = (last(P) pred(e))
\mvdash{} ((\mexists{}e':\{E| ((e' <loc pred(e))
\mwedge{} (\muparrow{}(P e'))
\mwedge{} (\mforall{}e'':E. ((e' <loc e'') {}\mRightarrow{} (e'' <loc pred(e)) {}\mRightarrow{} (\mneg{}\muparrow{}(P e'')))))\})
\mvee{} (\mneg{}(\mexists{}e':\{E| ((e' <loc pred(e)) \mwedge{} (\muparrow{}(P e')))\}))) \msubseteq{}r ((\mexists{}e':\{E| ((e' <loc e)
\mwedge{} (\muparrow{}(P e'))
\mwedge{} (\mforall{}e'':E
((e' <loc e'')
{}\mRightarrow{} (e'' <loc e)
{}\mRightarrow{} (\mneg{}\muparrow{}(P e'')))))\})
\mvee{} (\mneg{}(\mexists{}e':\{E| ((e' <loc e) \mwedge{} (\muparrow{}(P e')))\})))
By
Latex:
(Unfold `or` 0 THEN BLemma `subtype\_rel\_union` THEN Auto THEN SubtypeReasoning THEN Auto)
Home
Index