---

Step * 1 of Lemma append_overlapping_sublists


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)
⊢ ∃f:ℕ||L1 @ [x / L2]|| ⟶ ℕ||L||
   (increasing(f;||L1 @ [x / L2]||) ∧ (∀j:ℕ||L1 @ [x / L2]||. (L1 @ [x / L2][j] = L[f j] ∈ T)))
BY
{ Assert ||L1 @ [x / L2]|| = (||L1|| + ||L2|| + 1) ∈ ℤ   }

1
.....assertion..... 
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)
⊢ ||L1 @ [x / L2]|| = (||L1|| + ||L2|| + 1) ∈ ℤ

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) ∈ ℤ
⊢ ∃f:ℕ||L1 @ [x / L2]|| ⟶ ℕ||L||
   (increasing(f;||L1 @ [x / L2]||) ∧ (∀j:ℕ||L1 @ [x / L2]||. (L1 @ [x / L2][j] = L[f j] ∈ T)))

---

Latex:

---

Latex:

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])
\mvdash{}  \mexists{}f:\mBbbN{}||L1  @  [x  /  L2]||  {}\mrightarrow{}  \mBbbN{}||L||
      (increasing(f;||L1  @  [x  /  L2]||)  \mwedge{}  (\mforall{}j:\mBbbN{}||L1  @  [x  /  L2]||.  (L1  @  [x  /  L2][j]  =  L[f  j])))


By

---

Latex:
Assert  ||L1  @  [x  /  L2]||  =  (||L1||  +  ||L2||  +  1) 

---

Home Index