---

Step * 2 1 1 2 of Lemma sublist_append_front


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||
BY
{ (ExtWith [`z'] [ℕ||L|| ⟶ ℕ||L1 @ L2||; ℕ||L|| ⟶ ℕ||L1 @ L2||] THEN Auto) }

1
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||
11. z : ℕ||L||
⊢ f z ∈ ℕ||L1||

---

Latex:

---

Latex:

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)
10.  f  (||L||  -  1)  <  ||L1||
\mvdash{}  f  \mmember{}  \mBbbN{}||L||  {}\mrightarrow{}  \mBbbN{}||L1||


By

---

Latex:
(ExtWith  [`z']  [\mBbbN{}||L||  {}\mrightarrow{}  \mBbbN{}||L1  @  L2||;  \mBbbN{}||L||  {}\mrightarrow{}  \mBbbN{}||L1  @  L2||]  THEN  Auto)

---

Home Index