---

Step * 1 2 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)
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)))
BY
{ (AssertBY ||[]|| ≥ 0  (Reduce 0 THEN Auto)
   THEN InstConcl [λi.if i ≤z ||L1|| then f1 i else f (i - ||L1||) fi ]
   THEN Reduce 0
   THEN Auto) }

1
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 
⊢ increasing(λi.if i ≤z ||L1|| then f1 i else f (i - ||L1||) fi ;||L1 @ [x / L2]||)

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]||
⊢ L1 @ [x / L2][j] = L[if j ≤z ||L1|| then f1 j else f (j - ||L1||) fi ] ∈ 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])
13.  ||L1  @  [x  /  L2]||  =  (||L1||  +  ||L2||  +  1)
\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:
(AssertBY  ||[]||  \mgeq{}  0    (Reduce  0  THEN  Auto)
  THEN  InstConcl  [\mlambda{}i.if  i  \mleq{}z  ||L1||  then  f1  i  else  f  (i  -  ||L1||)  fi  ]
  THEN  Reduce  0
  THEN  Auto)

---

Home Index