---

Step * of Lemma nth_tl-es-open-interval

∀[es:EO]. ∀[e1,e2:E]. ∀[n:ℕ||(e1, e2)||].
  nth_tl(n + 1;(e1, e2)) = ((e1, e2)[n], e2) ∈ (E List) supposing loc(e1) = loc(e2) ∈ Id
BY
{ ((UnivCD THENA Auto)
   THEN (Assert ⌈∀n:ℕ. (n < ||(e1, e2)|| ⇒ (nth_tl(n + 1;(e1, e2)) = ((e1, e2)[n], e2) ∈ (E List)))⌉⋅
   THENM (BHyp -1  THEN Auto)
   )
   THEN Thin (-2)
   THEN InductionOnNat
   THEN Auto) }

1
1. es : EO
2. e1 : E
3. e2 : E
4. loc(e1) = loc(e2) ∈ Id
5. n : ℤ
6. 0 < ||(e1, e2)||@i
⊢ nth_tl(0 + 1;(e1, e2)) = ((e1, e2)[0], e2) ∈ (E List)

2
1. es : EO
2. e1 : E
3. e2 : E
4. loc(e1) = loc(e2) ∈ Id
5. n : ℤ
6. 0 < n
7. n - 1 < ||(e1, e2)|| ⇒ (nth_tl((n - 1) + 1;(e1, e2)) = ((e1, e2)[n - 1], e2) ∈ (E List))
8. n < ||(e1, e2)||@i
⊢ nth_tl(n + 1;(e1, e2)) = ((e1, e2)[n], e2) ∈ (E List)

---

Latex:


\mforall{}[es:EO].  \mforall{}[e1,e2:E].  \mforall{}[n:\mBbbN{}||(e1,  e2)||].
    nth\_tl(n  +  1;(e1,  e2))  =  ((e1,  e2)[n],  e2)  supposing  loc(e1)  =  loc(e2)


By

((UnivCD  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  (n  <  ||(e1,  e2)||  {}\mRightarrow{}  (nth\_tl(n  +  1;(e1,  e2))  =  ((e1,  e2)[n],  e2)))\mkleeneclose{}\mcdot{}
  THENM  (BHyp  -1    THEN  Auto)
  )
  THEN  Thin  (-2)
  THEN  InductionOnNat
  THEN  Auto)

---

Home Index