---

Step * of Lemma append-segment

∀T:Type. ∀as:T List. ∀i:{0...||as||}. ∀j:{i...||as||}. ∀k:{j...||as||}.
  (((as[i..j-]) @ (as[j..k-])) = (as[i..k-]) ∈ (T List))
BY
{ (Unfold `segment` 0 THEN InductionOnList THEN (UnivCD THENA Auto)) }

1
1. T : Type
2. i : {0...||[]||}
3. j : {i...||[]||}
4. k : {j...||[]||}
⊢ (firstn(j - i;nth_tl(i;[])) @ firstn(k - j;nth_tl(j;[]))) = firstn(k - i;nth_tl(i;[])) ∈ (T List)

2
1. T : Type
2. u : T
3. v : T List
4. ∀i:{0...||v||}. ∀j:{i...||v||}. ∀k:{j...||v||}.
     ((firstn(j - i;nth_tl(i;v)) @ firstn(k - j;nth_tl(j;v))) = firstn(k - i;nth_tl(i;v)) ∈ (T List))
5. i : {0...||[u / v]||}
6. j : {i...||[u / v]||}
7. k : {j...||[u / v]||}
⊢ (firstn(j - i;nth_tl(i;[u / v])) @ firstn(k - j;nth_tl(j;[u / v]))) = firstn(k - i;nth_tl(i;[u / v])) ∈ (T List)

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}as:T  List.  \mforall{}i:\{0...||as||\}.  \mforall{}j:\{i...||as||\}.  \mforall{}k:\{j...||as||\}.
    (((as[i..j\msupminus{}])  @  (as[j..k\msupminus{}]))  =  (as[i..k\msupminus{}]))


By

---

Latex:
(Unfold  `segment`  0  THEN  InductionOnList  THEN  (UnivCD  THENA  Auto))

---

Home Index