---

Step * 1 1 1 1 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. n < ||before(pred(e))||
⊢ before(pred(e))[n] ≤loc pred(e) 
BY
{ (InstLemma `member-es-before` [⌈es⌉;⌈pred(e)⌉;⌈before(pred(e))[n]⌉]⋅ THEN Auto THEN D -2 THEN Auto)⋅ }

---

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.  n  <  ||before(pred(e))||
\mvdash{}  before(pred(e))[n]  \mleq{}loc  pred(e) 


By

(InstLemma  `member-es-before`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}pred(e)\mkleeneclose{};\mkleeneopen{}before(pred(e))[n]\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  D  -2  THEN  Auto)\mcdot{}

---

Home Index