---

Step * 1 2 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) ∈ ℤ
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
BY
{ ((AssertBY ||L1 @ [x]|| = (||L1|| + 1) ∈ ℤ        ((RWO "length_append" 0 THEN Reduce 0) THEN Auto')
    THEN SplitOnConclITE
    )
   THENA Auto
   ) }

1
.....truecase..... 
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. j ≤ ||L1||
⊢ L1 @ [x / L2][j] = L[f1 j] ∈ T

2
.....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

---

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)
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]||
\mvdash{}  L1  @  [x  /  L2][j]  =  L[if  j  \mleq{}z  ||L1||  then  f1  j  else  f  (j  -  ||L1||)  fi  ]


By

---

Latex:
((AssertBY  ||L1  @  [x]||  =  (||L1||  +  1)              ((RWO  "length\_append"  0  THEN  Reduce  0)  THEN  Auto')
    THEN  SplitOnConclITE
    )
  THENA  Auto
  )

---

Home Index