Step
*
2
1
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')
15. (pred(e') <loc e') ∧ (∀e'@0:E. (¬((pred(e') <loc e'@0) ∧ (e'@0 <loc e'))))
16. ¬(pred(e') <loc e)
⊢ e = pred(e') ∈ E
BY
{ (((InstHyp [e; pred(e')] 4)⋅ THENA Auto) THEN (D (-1)) THEN (Thin (-1)) THEN (D (-1))) }
1
.....antecedent.....
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'))))
16. ¬(pred(e') <loc e)
⊢ loc(e) = loc(pred(e')) ∈ Id
2
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'))))
16. ¬(pred(e') <loc e)
17. (e <loc pred(e')) ∨ (e = pred(e') ∈ E) ∨ (pred(e') <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')
15. (pred(e') <loc e') \mwedge{} (\mforall{}e'@0:E. (\mneg{}((pred(e') <loc e'@0) \mwedge{} (e'@0 <loc e'))))
16. \mneg{}(pred(e') <loc e)
\mvdash{} e = pred(e')
By
(((InstHyp [e; pred(e')] 4)\mcdot{} THENA Auto) THEN (D (-1)) THEN (Thin (-1)) THEN (D (-1)))
Home
Index