---

Step * 1 2 2 2 of Lemma append_overlapping_sublists

.....falsecase..... 
1. T : Type
2. L1 : T List
3. L2 : T List
4. L : T List
5. x : T
6. ∀[i,j:ℕ].  (¬(L[i] = L[j] ∈ T)) supposing ((¬(i = j ∈ ℕ)) and j < ||L|| and i < ||L||)
7. f1 : ℕ||L1 @ [x]|| ⟶ ℕ||L||
8. increasing(f1;||L1 @ [x]||)
9. ∀j:ℕ||L1 @ [x]||. (L1 @ [x][j] = L[f1 j] ∈ T)
10. f : ℕ||L2|| + 1 ⟶ ℕ||L||
11. increasing(f;||L2|| + 1)
12. ∀j:ℕ||L2|| + 1. ([x / L2][j] = L[f j] ∈ T)
13. ||L1 @ [x / L2]|| = (||L1|| + ||L2|| + 1) ∈ ℤ
14. ||[]|| ≥ 0 
15. increasing(λi.if i ≤z ||L1|| then f1 i else f (i - ||L1||) fi ;||L1 @ [x / L2]||)
16. j : ℕ||L1 @ [x / L2]||
17. ||L1 @ [x]|| = (||L1|| + 1) ∈ ℤ
18. ||L1|| < j
⊢ L1 @ [x / L2][j] = L[f (j - ||L1||)] ∈ T
BY
{ (RWO "select_append_back" 0 THEN Try (QuickAuto)) }

1
.....wf..... 
1. T : Type
2. L1 : T List
3. L2 : T List
4. L : T List
5. x : T
6. ∀[i,j:ℕ].  (¬(L[i] = L[j] ∈ T)) supposing ((¬(i = j ∈ ℕ)) and j < ||L|| and i < ||L||)
7. f1 : ℕ||L1 @ [x]|| ⟶ ℕ||L||
8. increasing(f1;||L1 @ [x]||)
9. ∀j:ℕ||L1 @ [x]||. (L1 @ [x][j] = L[f1 j] ∈ T)
10. f : ℕ||L2|| + 1 ⟶ ℕ||L||
11. increasing(f;||L2|| + 1)
12. ∀j:ℕ||L2|| + 1. ([x / L2][j] = L[f j] ∈ T)
13. ||L1 @ [x / L2]|| = (||L1|| + ||L2|| + 1) ∈ ℤ
14. ||[]|| ≥ 0 
15. increasing(λi.if i ≤z ||L1|| then f1 i else f (i - ||L1||) fi ;||L1 @ [x / L2]||)
16. j : ℕ||L1 @ [x / L2]||
17. ||L1 @ [x]|| = (||L1|| + 1) ∈ ℤ
18. ||L1|| < j
⊢ L[f (j - ||L1||)] = L[f (j - ||L1||)] ∈ T

2
1. T : Type
2. L1 : T List
3. L2 : T List
4. L : T List
5. x : T
6. ∀[i,j:ℕ].  (¬(L[i] = L[j] ∈ T)) supposing ((¬(i = j ∈ ℕ)) and j < ||L|| and i < ||L||)
7. f1 : ℕ||L1 @ [x]|| ⟶ ℕ||L||
8. increasing(f1;||L1 @ [x]||)
9. ∀j:ℕ||L1 @ [x]||. (L1 @ [x][j] = L[f1 j] ∈ T)
10. f : ℕ||L2|| + 1 ⟶ ℕ||L||
11. increasing(f;||L2|| + 1)
12. ∀j:ℕ||L2|| + 1. ([x / L2][j] = L[f j] ∈ T)
13. ||L1 @ [x / L2]|| = (||L1|| + ||L2|| + 1) ∈ ℤ
14. ||[]|| ≥ 0 
15. increasing(λi.if i ≤z ||L1|| then f1 i else f (i - ||L1||) fi ;||L1 @ [x / L2]||)
16. j : ℕ||L1 @ [x / L2]||
17. ||L1 @ [x]|| = (||L1|| + 1) ∈ ℤ
18. ||L1|| < j
⊢ [x / L2][j - ||L1||] = L[f (j - ||L1||)] ∈ T

---

Latex:

---

Latex:
.....falsecase..... 
1.  T  :  Type
2.  L1  :  T  List
3.  L2  :  T  List
4.  L  :  T  List
5.  x  :  T
6.  \mforall{}[i,j:\mBbbN{}].    (\mneg{}(L[i]  =  L[j]))  supposing  ((\mneg{}(i  =  j))  and  j  <  ||L||  and  i  <  ||L||)
7.  f1  :  \mBbbN{}||L1  @  [x]||  {}\mrightarrow{}  \mBbbN{}||L||
8.  increasing(f1;||L1  @  [x]||)
9.  \mforall{}j:\mBbbN{}||L1  @  [x]||.  (L1  @  [x][j]  =  L[f1  j])
10.  f  :  \mBbbN{}||L2||  +  1  {}\mrightarrow{}  \mBbbN{}||L||
11.  increasing(f;||L2||  +  1)
12.  \mforall{}j:\mBbbN{}||L2||  +  1.  ([x  /  L2][j]  =  L[f  j])
13.  ||L1  @  [x  /  L2]||  =  (||L1||  +  ||L2||  +  1)
14.  ||[]||  \mgeq{}  0 
15.  increasing(\mlambda{}i.if  i  \mleq{}z  ||L1||  then  f1  i  else  f  (i  -  ||L1||)  fi  ;||L1  @  [x  /  L2]||)
16.  j  :  \mBbbN{}||L1  @  [x  /  L2]||
17.  ||L1  @  [x]||  =  (||L1||  +  1)
18.  ||L1||  <  j
\mvdash{}  L1  @  [x  /  L2][j]  =  L[f  (j  -  ||L1||)]


By

---

Latex:
(RWO  "select\_append\_back"  0  THEN  Try  (QuickAuto))

---

Home Index