---

Step * 1 2 1 of Lemma nth_tl-es-before


1. es : EO
2. e : E@i
3. n : ℕ||before(e)||@i
4. ¬↑first(e)
5. ∀n:ℕ||before(pred(e))||
     (nth_tl(n;before(pred(e))) = filter(λa.before(pred(e))[n] ≤loc a;before(pred(e))) ∈ (E List))
6. ||before(pred(e))|| ≤ n
7. n = ||before(pred(e))|| ∈ ℤ
⊢ nth_tl(n - ||before(pred(e))||;[pred(e)])
= (filter(λa.before(pred(e)) @ [pred(e)][n] ≤loc a;before(pred(e)))
  @ if before(pred(e)) @ [pred(e)][n] ≤loc pred(e) then [pred(e)] else [] fi )
∈ (E List)
BY
{ ((RWO "select_append_back" 0 THENA (Auto THEN Auto'))⋅ THEN Subst' n - ||before(pred(e))|| ~ 0 0 THEN Auto) }

1
1. es : EO
2. e : E@i
3. n : ℕ||before(e)||@i
4. ¬↑first(e)
5. ∀n:ℕ||before(pred(e))||
     (nth_tl(n;before(pred(e))) = filter(λa.before(pred(e))[n] ≤loc a;before(pred(e))) ∈ (E List))
6. ||before(pred(e))|| ≤ n
7. n = ||before(pred(e))|| ∈ ℤ
⊢ (n - ||before(pred(e))||) = 0 ∈ ℤ

2
1. es : EO
2. e : E@i
3. n : ℕ||before(e)||@i
4. ¬↑first(e)
5. ∀n:ℕ||before(pred(e))||
     (nth_tl(n;before(pred(e))) = filter(λa.before(pred(e))[n] ≤loc a;before(pred(e))) ∈ (E List))
6. ||before(pred(e))|| ≤ n
7. n = ||before(pred(e))|| ∈ ℤ
⊢ nth_tl(0;[pred(e)])
= (filter(λa.[pred(e)][0] ≤loc a;before(pred(e))) @ if [pred(e)][0] ≤loc pred(e) then [pred(e)] else [] fi )
∈ (E List)

---

Latex:



1.  es  :  EO
2.  e  :  E@i
3.  n  :  \mBbbN{}||before(e)||@i
4.  \mneg{}\muparrow{}first(e)
5.  \mforall{}n:\mBbbN{}||before(pred(e))||
          (nth\_tl(n;before(pred(e)))  =  filter(\mlambda{}a.before(pred(e))[n]  \mleq{}loc  a;before(pred(e))))
6.  ||before(pred(e))||  \mleq{}  n
7.  n  =  ||before(pred(e))||
\mvdash{}  nth\_tl(n  -  ||before(pred(e))||;[pred(e)])
=  (filter(\mlambda{}a.before(pred(e))  @  [pred(e)][n]  \mleq{}loc  a;before(pred(e)))
    @  if  before(pred(e))  @  [pred(e)][n]  \mleq{}loc  pred(e)  then  [pred(e)]  else  []  fi  )


By

((RWO  "select\_append\_back"  0  THENA  (Auto  THEN  Auto'))\mcdot{}
  THEN  Subst'  n  -  ||before(pred(e))||  \msim{}  0  0
  THEN  Auto)

---

Home Index