---

Step * 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])))
⊢ firstn(n;before(pred(e))) ~ before(before(pred(e)) @ [pred(e)][n])
BY
{ ((RWO "select-append" 0 THENA Auto) THEN OldAutoSplit) }

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
⊢ firstn(n;before(pred(e))) ~ before([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])))
\mvdash{}  firstn(n;before(pred(e)))  \msim{}  before(before(pred(e))  @  [pred(e)][n])


By

((RWO  "select-append"  0  THENA  Auto)  THEN  OldAutoSplit)

---

Home Index