Step
*
2
of Lemma
implies-es-pred
1. the_es : EO
2. Trans(E;e,e'.(e <loc e'))
3. SWellFounded((e <loc e'))
4. ∀e,e':E. (loc(e) = loc(e') ∈ Id ⇐⇒ (e <loc e') ∨ (e = e' ∈ E) ∨ (e' <loc e))
5. ∀e:E. (↑first(e) ⇐⇒ ∀e':E. (¬(e' <loc e)))
6. ∀e:E. (pred(e) <loc e) ∧ (∀e':E. (¬((pred(e) <loc e') ∧ (e' <loc e)))) supposing ¬↑first(e)
7. Trans(E;e,e'.(e < e'))
8. SWellFounded((e < e'))
9. ∀e,e':E. ((e <loc e') ⇒ (e < e'))
10. e : E
11. e' : E
12. (e <loc e')
13. ∀e1:E. (¬((e <loc e1) c∧ (e1 <loc e')))
14. ¬↑first(e')
⊢ e = pred(e') ∈ E
BY
{ ((InstHyp [e'] 6)⋅ THENA Auto) }
1
1. the_es : EO
2. Trans(E;e,e'.(e <loc e'))
3. SWellFounded((e <loc e'))
4. ∀e,e':E. (loc(e) = loc(e') ∈ Id ⇐⇒ (e <loc e') ∨ (e = e' ∈ E) ∨ (e' <loc e))
5. ∀e:E. (↑first(e) ⇐⇒ ∀e':E. (¬(e' <loc e)))
6. ∀e:E. (pred(e) <loc e) ∧ (∀e':E. (¬((pred(e) <loc e') ∧ (e' <loc e)))) supposing ¬↑first(e)
7. Trans(E;e,e'.(e < e'))
8. SWellFounded((e < e'))
9. ∀e,e':E. ((e <loc e') ⇒ (e < e'))
10. e : E
11. e' : E
12. (e <loc e')
13. ∀e1:E. (¬((e <loc e1) c∧ (e1 <loc e')))
14. ¬↑first(e')
15. (pred(e') <loc e') ∧ (∀e'@0:E. (¬((pred(e') <loc e'@0) ∧ (e'@0 <loc e'))))
⊢ e = pred(e') ∈ E
Latex:
1. the$_{es}$ : EO
2. Trans(E;e,e'.(e <loc e'))
3. SWellFounded((e <loc e'))
4. \mforall{}e,e':E. (loc(e) = loc(e') \mLeftarrow{}{}\mRightarrow{} (e <loc e') \mvee{} (e = e') \mvee{} (e' <loc e))
5. \mforall{}e:E. (\muparrow{}first(e) \mLeftarrow{}{}\mRightarrow{} \mforall{}e':E. (\mneg{}(e' <loc e)))
6. \mforall{}e:E. (pred(e) <loc e) \mwedge{} (\mforall{}e':E. (\mneg{}((pred(e) <loc e') \mwedge{} (e' <loc e)))) supposing \mneg{}\muparrow{}first(e)
7. Trans(E;e,e'.(e < e'))
8. SWellFounded((e < e'))
9. \mforall{}e,e':E. ((e <loc e') {}\mRightarrow{} (e < e'))
10. e : E
11. e' : E
12. (e <loc e')
13. \mforall{}e1:E. (\mneg{}((e <loc e1) c\mwedge{} (e1 <loc e')))
14. \mneg{}\muparrow{}first(e')
\mvdash{} e = pred(e')
By
((InstHyp [e'] 6)\mcdot{} THENA Auto)
Home
Index