---

Step * 1 2 1 2 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. ||before(pred(e))|| ≤ n
7. n = ||before(pred(e))|| ∈ ℤ
8. pred(e) ≤loc pred(e) 
⊢ (∀x∈before(pred(e)).¬↑((λa.pred(e) ≤loc a) x))
BY
{ (RepUR ``so_apply`` 0 THEN (BLemma `l_all_iff` THENM Reduce 0) THEN Auto THEN RWO "assert-es-ble" 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))|| ∈ ℤ
8. pred(e) ≤loc pred(e) 
9. x : E@i
10. (x ∈ before(pred(e)))@i
⊢ ¬pred(e) ≤loc x 

---

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))||
8.  pred(e)  \mleq{}loc  pred(e) 
\mvdash{}  (\mforall{}x\mmember{}before(pred(e)).\mneg{}\muparrow{}((\mlambda{}a.pred(e)  \mleq{}loc  a)  x))


By

(RepUR  ``so\_apply``  0
  THEN  (BLemma  `l\_all\_iff`  THENM  Reduce  0)
  THEN  Auto
  THEN  RWO  "assert-es-ble"  0
  THEN  Auto)

---

Home Index