Step
*
1
1
1
1
of Lemma
firstn-before
1. the_es : EO@i'
2. e : E@i
3. ∀e1:E. ((e1 < e)
⇒ (∀n:ℕ. (n < ||before(e1)||
⇒ (firstn(n;before(e1)) ~ before(before(e1)[n])))))
4. n : ℕ@i
5. ¬↑first(e)
6. n < ||before(pred(e))|| + 1@i
7. ∀n:ℕ. (n < ||before(pred(e))||
⇒ (firstn(n;before(pred(e))) ~ before(before(pred(e))[n])))
8. ||before(pred(e))|| ≤ n
⊢ ||before(pred(e))|| ≤ n
BY
{ Auto' }
Latex:
1. the$_{es}$ : EO@i'
2. e : E@i
3. \mforall{}e1:E
((e1 < e) {}\mRightarrow{} (\mforall{}n:\mBbbN{}. (n < ||before(e1)|| {}\mRightarrow{} (firstn(n;before(e1)) \msim{} before(before(e1)[n])))))
4. n : \mBbbN{}@i
5. \mneg{}\muparrow{}first(e)
6. n < ||before(pred(e))|| + 1@i
7. \mforall{}n:\mBbbN{}. (n < ||before(pred(e))|| {}\mRightarrow{} (firstn(n;before(pred(e))) \msim{} before(before(pred(e))[n])))
8. ||before(pred(e))|| \mleq{} n
\mvdash{} ||before(pred(e))|| \mleq{} n
By
Auto'
Home
Index