---

Step * 1 of Lemma nth_tl-es-before


1. es : EO
2. e : E@i
3. ∀e1:E
     ((e1 < e) ⇒ (∀n:ℕ||before(e1)||. (nth_tl(n;before(e1)) = filter(λa.before(e1)[n] ≤loc a;before(e1)) ∈ (E List))))
4. n : ℕ||before(e)||@i
⊢ nth_tl(n;before(e)) = filter(λa.before(e)[n] ≤loc a;before(e)) ∈ (E List)
BY
{ (RecUnfold `es-before` 0
   THEN OldAutoSplit
   THEN (InstHyp [⌈pred(e)⌉] 3⋅ THENA Auto)
   THEN Thin 3
   THEN (RWO "filter_append_sq" 0 THENA Auto)
   THEN (RWO "nth_tl-append" 0 THENA Auto)
   THEN OldAutoSplit) }

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. 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)

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
⊢ 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)

---

Latex:



1.  es  :  EO
2.  e  :  E@i
3.  \mforall{}e1:E
          ((e1  <  e)
          {}\mRightarrow{}  (\mforall{}n:\mBbbN{}||before(e1)||.  (nth\_tl(n;before(e1))  =  filter(\mlambda{}a.before(e1)[n]  \mleq{}loc  a;before(e1)))))
4.  n  :  \mBbbN{}||before(e)||@i
\mvdash{}  nth\_tl(n;before(e))  =  filter(\mlambda{}a.before(e)[n]  \mleq{}loc  a;before(e))


By

(RecUnfold  `es-before`  0
  THEN  OldAutoSplit
  THEN  (InstHyp  [\mkleeneopen{}pred(e)\mkleeneclose{}]  3\mcdot{}  THENA  Auto)
  THEN  Thin  3
  THEN  (RWO  "filter\_append\_sq"  0  THENA  Auto)
  THEN  (RWO  "nth\_tl-append"  0  THENA  Auto)
  THEN  OldAutoSplit)

---

Home Index