---

Step * 2 1 1 of Lemma sublist_append_front

.....assertion..... 
1. [T] : Type
2. L : T List
3. L1 : T List
4. L2 : T List
5. f : ℕ||L|| ⟶ ℕ||L1 @ L2||
6. increasing(f;||L||)
7. ∀j:ℕ||L||. (L[j] = L1 @ L2[f j] ∈ T)
8. ¬↑null(L)
9. ¬(last(L) ∈ L2)
⊢ f ∈ ℕ||L|| ⟶ ℕ||L1||
BY
{ Assert f (||L|| - 1) < ||L1|| }

1
.....assertion..... 
1. T : Type
2. L : T List
3. L1 : T List
4. L2 : T List
5. f : ℕ||L|| ⟶ ℕ||L1 @ L2||
6. increasing(f;||L||)
7. ∀j:ℕ||L||. (L[j] = L1 @ L2[f j] ∈ T)
8. ¬↑null(L)
9. ¬(last(L) ∈ L2)
⊢ f (||L|| - 1) < ||L1||

2
1. [T] : Type
2. L : T List
3. L1 : T List
4. L2 : T List
5. f : ℕ||L|| ⟶ ℕ||L1 @ L2||
6. increasing(f;||L||)
7. ∀j:ℕ||L||. (L[j] = L1 @ L2[f j] ∈ T)
8. ¬↑null(L)
9. ¬(last(L) ∈ L2)
10. f (||L|| - 1) < ||L1||
⊢ f ∈ ℕ||L|| ⟶ ℕ||L1||

---

Latex:

---

Latex:
.....assertion..... 
1.  [T]  :  Type
2.  L  :  T  List
3.  L1  :  T  List
4.  L2  :  T  List
5.  f  :  \mBbbN{}||L||  {}\mrightarrow{}  \mBbbN{}||L1  @  L2||
6.  increasing(f;||L||)
7.  \mforall{}j:\mBbbN{}||L||.  (L[j]  =  L1  @  L2[f  j])
8.  \mneg{}\muparrow{}null(L)
9.  \mneg{}(last(L)  \mmember{}  L2)
\mvdash{}  f  \mmember{}  \mBbbN{}||L||  {}\mrightarrow{}  \mBbbN{}||L1||


By

---

Latex:
Assert  f  (||L||  -  1)  <  ||L1||

---

Home Index