---

Step * 4 1 2 1 1 of Lemma select_concat

.....equality..... 
1. T : Type
2. u : T List
3. v : T List List
4. ∀n:ℕ||concat(v)||
     ∃m:ℕ||v||
      ((||concat(firstn(m;v))|| ≤ n)
      c∧ n - ||concat(firstn(m;v))|| < ||v[m]||
      c∧ (concat(v)[n] = v[m][n - ||concat(firstn(m;v))||] ∈ T))
5. n : ℕ||u @ concat(v)||
6. ¬n < ||u||
7. m : ℕ||v||
8. ||concat(firstn(m;v))|| ≤ (n - ||u||)
9. n - ||u|| - ||concat(firstn(m;v))|| < ||v[m]||
10. concat(v)[n - ||u||] = v[m][n - ||u|| - ||concat(firstn(m;v))||] ∈ T
⊢ firstn(m + 1;[u / v]) ~ [u / firstn(m;v)]
BY
{ (((RW (AddrC [1] (RecUnfoldC `firstn`)) 0) THEN Reduce 0 THEN SplitOnConclITE) THENA Auto) }

1
.....truecase..... 
1. T : Type
2. u : T List
3. v : T List List
4. ∀n:ℕ||concat(v)||
     ∃m:ℕ||v||
      ((||concat(firstn(m;v))|| ≤ n)
      c∧ n - ||concat(firstn(m;v))|| < ||v[m]||
      c∧ (concat(v)[n] = v[m][n - ||concat(firstn(m;v))||] ∈ T))
5. n : ℕ||u @ concat(v)||
6. ¬n < ||u||
7. m : ℕ||v||
8. ||concat(firstn(m;v))|| ≤ (n - ||u||)
9. n - ||u|| - ||concat(firstn(m;v))|| < ||v[m]||
10. concat(v)[n - ||u||] = v[m][n - ||u|| - ||concat(firstn(m;v))||] ∈ T
11. 0 < m + 1
⊢ [u / firstn((m + 1) - 1;v)] ~ [u / firstn(m;v)]

2
.....falsecase..... 
1. T : Type
2. u : T List
3. v : T List List
4. ∀n:ℕ||concat(v)||
     ∃m:ℕ||v||
      ((||concat(firstn(m;v))|| ≤ n)
      c∧ n - ||concat(firstn(m;v))|| < ||v[m]||
      c∧ (concat(v)[n] = v[m][n - ||concat(firstn(m;v))||] ∈ T))
5. n : ℕ||u @ concat(v)||
6. ¬n < ||u||
7. m : ℕ||v||
8. ||concat(firstn(m;v))|| ≤ (n - ||u||)
9. n - ||u|| - ||concat(firstn(m;v))|| < ||v[m]||
10. concat(v)[n - ||u||] = v[m][n - ||u|| - ||concat(firstn(m;v))||] ∈ T
11. (m + 1) ≤ 0
⊢ [] ~ [u / firstn(m;v)]

---

Latex:

---

Latex:
.....equality..... 
1.  T  :  Type
2.  u  :  T  List
3.  v  :  T  List  List
4.  \mforall{}n:\mBbbN{}||concat(v)||
          \mexists{}m:\mBbbN{}||v||
            ((||concat(firstn(m;v))||  \mleq{}  n)
            c\mwedge{}  n  -  ||concat(firstn(m;v))||  <  ||v[m]||
            c\mwedge{}  (concat(v)[n]  =  v[m][n  -  ||concat(firstn(m;v))||]))
5.  n  :  \mBbbN{}||u  @  concat(v)||
6.  \mneg{}n  <  ||u||
7.  m  :  \mBbbN{}||v||
8.  ||concat(firstn(m;v))||  \mleq{}  (n  -  ||u||)
9.  n  -  ||u||  -  ||concat(firstn(m;v))||  <  ||v[m]||
10.  concat(v)[n  -  ||u||]  =  v[m][n  -  ||u||  -  ||concat(firstn(m;v))||]
\mvdash{}  firstn(m  +  1;[u  /  v])  \msim{}  [u  /  firstn(m;v)]


By

---

Latex:
(((RW  (AddrC  [1]  (RecUnfoldC  `firstn`))  0)  THEN  Reduce  0  THEN  SplitOnConclITE)  THENA  Auto)

---

Home Index