---

Step * 2 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|| ⟶ ℕ||L1||
⊢ ∃f:ℕ||L|| ⟶ ℕ||L1||. (increasing(f;||L||) ∧ (∀j:ℕ||L||. (L[j] = L1[f j] ∈ T)))
BY
{ (InstConcl [f] THEN Auto) }

---

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  \mmember{}  \mBbbN{}||L||  {}\mrightarrow{}  \mBbbN{}||L1||
\mvdash{}  \mexists{}f:\mBbbN{}||L||  {}\mrightarrow{}  \mBbbN{}||L1||.  (increasing(f;||L||)  \mwedge{}  (\mforall{}j:\mBbbN{}||L||.  (L[j]  =  L1[f  j])))


By

---

Latex:
(InstConcl  [f]  THEN  Auto)

---

Home Index