---

Step * 1 1 1 2 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)) ~ before([pred(e)][n - ||before(pred(e))||])
BY
{ EqCD }

1
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
⊢ the_es ~ the_es

2
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
⊢ pred(e) ~ [pred(e)][n - ||before(pred(e))||]

---

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))  \msim{}  before([pred(e)][n  -  ||before(pred(e))||])


By

EqCD

---

Home Index