---

Step * 2 1 2 1 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. ∀i:ℕ||L2|| - 1. f i < f (i + 1)
11. ∀j:ℕ||L2||. (L2[j] = L2'[f j] ∈ T)
12. i : ℕ(||L1|| + ||L2||) - 1
13. ¬i < ||L1||
14. f (i - ||L1||) < f ((i - ||L1||) + 1)
⊢ (f (i - ||L1||)) + ||L1'|| < (f ((i - ||L1||) + 1)) + ||L1'||
BY
{ (MoveToConcl (-1) THEN GenConclTerms Auto [⌜f (i - ||L1||)⌝;⌜f ((i - ||L1||) + 1)⌝]⋅) }

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. ∀i:ℕ||L2|| - 1. f i < f (i + 1)
11. ∀j:ℕ||L2||. (L2[j] = L2'[f j] ∈ T)
12. i : ℕ(||L1|| + ||L2||) - 1
13. ¬i < ||L1||
14. v : ℕ||L2'||
15. (f (i - ||L1||)) = v ∈ ℕ||L2'||
16. v1 : ℕ||L2'||
17. (f ((i - ||L1||) + 1)) = v1 ∈ ℕ||L2'||
⊢ v < v1 ⇒ v + ||L1'|| < v1 + ||L1'||

---

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.  \mforall{}i:\mBbbN{}||L2||  -  1.  f  i  <  f  (i  +  1)
11.  \mforall{}j:\mBbbN{}||L2||.  (L2[j]  =  L2'[f  j])
12.  i  :  \mBbbN{}(||L1||  +  ||L2||)  -  1
13.  \mneg{}i  <  ||L1||
14.  f  (i  -  ||L1||)  <  f  ((i  -  ||L1||)  +  1)
\mvdash{}  (f  (i  -  ||L1||))  +  ||L1'||  <  (f  ((i  -  ||L1||)  +  1))  +  ||L1'||


By

---

Latex:
(MoveToConcl  (-1)  THEN  GenConclTerms  Auto  [\mkleeneopen{}f  (i  -  ||L1||)\mkleeneclose{};\mkleeneopen{}f  ((i  -  ||L1||)  +  1)\mkleeneclose{}]\mcdot{})

---

Home Index