---

Step * 2 1 2 1 1 of Lemma append-segment


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 : {0...||[u / v]||}
7. ¬(j ≤ 0)
8. k : {j...||[u / v]||}
9. i ≤ 0
10. (firstn(j - 1 - 0;v) @ firstn(k - 1 - j - 1;nth_tl(j - 1;v))) = firstn(k - 1 - 0;v) ∈ (T List)
⊢ (firstn(j - 0;[u / v]) @ firstn(k - j;nth_tl(j - 1;v))) = firstn(k - 0;[u / v]) ∈ (T List)
BY
{ Subst' firstn(j - 0;[u / v]) ~ [u / firstn(j - 1 - 0;v)] 0 }

1
.....equality..... 
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 : {0...||[u / v]||}
7. ¬(j ≤ 0)
8. k : {j...||[u / v]||}
9. i ≤ 0
10. (firstn(j - 1 - 0;v) @ firstn(k - 1 - j - 1;nth_tl(j - 1;v))) = firstn(k - 1 - 0;v) ∈ (T List)
⊢ firstn(j - 0;[u / v]) ~ [u / firstn(j - 1 - 0;v)]

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 : {0...||[u / v]||}
7. ¬(j ≤ 0)
8. k : {j...||[u / v]||}
9. i ≤ 0
10. (firstn(j - 1 - 0;v) @ firstn(k - 1 - j - 1;nth_tl(j - 1;v))) = firstn(k - 1 - 0;v) ∈ (T List)
⊢ ([u / firstn(j - 1 - 0;v)] @ firstn(k - j;nth_tl(j - 1;v))) = firstn(k - 0;[u / v]) ∈ (T List)

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  T
3.  v  :  T  List
4.  \mforall{}i:\{0...||v||\}.  \mforall{}j:\{i...||v||\}.  \mforall{}k:\{j...||v||\}.
          ((firstn(j  -  i;nth\_tl(i;v))  @  firstn(k  -  j;nth\_tl(j;v)))  =  firstn(k  -  i;nth\_tl(i;v)))
5.  i  :  \{0...||[u  /  v]||\}
6.  j  :  \{0...||[u  /  v]||\}
7.  \mneg{}(j  \mleq{}  0)
8.  k  :  \{j...||[u  /  v]||\}
9.  i  \mleq{}  0
10.  (firstn(j  -  1  -  0;v)  @  firstn(k  -  1  -  j  -  1;nth\_tl(j  -  1;v)))  =  firstn(k  -  1  -  0;v)
\mvdash{}  (firstn(j  -  0;[u  /  v])  @  firstn(k  -  j;nth\_tl(j  -  1;v)))  =  firstn(k  -  0;[u  /  v])


By

---

Latex:
Subst'  firstn(j  -  0;[u  /  v])  \msim{}  [u  /  firstn(j  -  1  -  0;v)]  0

---

Home Index