---

Step * 2 of Lemma sublist_append


1. [T] : Type
2. L1 : T List
3. L2 : T List
4. L1' : T List
5. L2' : T List
6. f1 : ℕ||L1|| ⟶ ℕ||L1'||
7. increasing(f1;||L1||)
8. ∀j:ℕ||L1||. (L1[j] = L1'[f1 j] ∈ T)
9. f : ℕ||L2|| ⟶ ℕ||L2'||
10. increasing(f;||L2||)
11. ∀j:ℕ||L2||. (L2[j] = L2'[f j] ∈ T)
⊢ increasing(λi.if i <z ||L1|| then f1 i else (f (i - ||L1||)) + ||L1'|| fi ;||L1 @ L2||)
∧ (∀j:ℕ||L1 @ L2||. (L1 @ L2[j] = L1' @ L2'[(λi.if i <z ||L1|| then f1 i else (f (i - ||L1||)) + ||L1'|| fi ) j] ∈ T))
BY
{ (TACTIC:RepUR ``increasing`` 0 THEN RWO "length-append" 0 THEN Auto' THEN Repeat (AutoSplit) THEN Auto') }

1
1. T : Type
2. L1 : T List
3. L2 : T List
4. L1' : T List
5. L2' : T List
6. f1 : ℕ||L1|| ⟶ ℕ||L1'||
7. increasing(f1;||L1||)
8. ∀j:ℕ||L1||. (L1[j] = L1'[f1 j] ∈ T)
9. f : ℕ||L2|| ⟶ ℕ||L2'||
10. increasing(f;||L2||)
11. ∀j:ℕ||L2||. (L2[j] = L2'[f j] ∈ T)
12. i : ℕ(||L1|| + ||L2||) - 1
13. ¬i < ||L1||
⊢ (f (i - ||L1||)) + ||L1'|| < (f ((i + 1) - ||L1||)) + ||L1'||

2
1. T : Type
2. L1 : T List
3. L2 : T List
4. L1' : T List
5. L2' : T List
6. f1 : ℕ||L1|| ⟶ ℕ||L1'||
7. increasing(f1;||L1||)
8. ∀j:ℕ||L1||. (L1[j] = L1'[f1 j] ∈ T)
9. f : ℕ||L2|| ⟶ ℕ||L2'||
10. increasing(f;||L2||)
11. ∀j:ℕ||L2||. (L2[j] = L2'[f j] ∈ T)
12. ∀i:ℕ(||L1|| + ||L2||) - 1
      if i <z ||L1|| then f1 i else (f (i - ||L1||)) + ||L1'|| fi  < if i + 1 <z ||L1||
      then f1 (i + 1)
      else (f ((i + 1) - ||L1||)) + ||L1'||
      fi 
13. j : ℕ||L1|| + ||L2||
14. ¬j < ||L1||
⊢ L1 @ L2[j] = L1' @ L2'[(f (j - ||L1||)) + ||L1'||] ∈ T

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L1  :  T  List
3.  L2  :  T  List
4.  L1'  :  T  List
5.  L2'  :  T  List
6.  f1  :  \mBbbN{}||L1||  {}\mrightarrow{}  \mBbbN{}||L1'||
7.  increasing(f1;||L1||)
8.  \mforall{}j:\mBbbN{}||L1||.  (L1[j]  =  L1'[f1  j])
9.  f  :  \mBbbN{}||L2||  {}\mrightarrow{}  \mBbbN{}||L2'||
10.  increasing(f;||L2||)
11.  \mforall{}j:\mBbbN{}||L2||.  (L2[j]  =  L2'[f  j])
\mvdash{}  increasing(\mlambda{}i.if  i  <z  ||L1||  then  f1  i  else  (f  (i  -  ||L1||))  +  ||L1'||  fi  ;||L1  @  L2||)
\mwedge{}  (\mforall{}j:\mBbbN{}||L1  @  L2||
          (L1  @  L2[j]  =  L1'  @  L2'[(\mlambda{}i.if  i  <z  ||L1||  then  f1  i  else  (f  (i  -  ||L1||))  +  ||L1'||  fi  )  j]))


By

---

Latex:
(TACTIC:RepUR  ``increasing``  0
  THEN  RWO  "length-append"  0
  THEN  Auto'
  THEN  Repeat  (AutoSplit)
  THEN  Auto')

---

Home Index