---

Step * 3 of Lemma sublist_append

.....wf..... 
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. f2 : ℕ||L1 @ L2|| ⟶ ℕ||L1' @ L2'||
⊢ istype(increasing(f2;||L1 @ L2||) ∧ (∀j:ℕ||L1 @ L2||. (L1 @ L2[j] = L1' @ L2'[f2 j] ∈ T)))
BY
{ Auto }

---

Latex:

---

Latex:
.....wf..... 
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])
12.  f2  :  \mBbbN{}||L1  @  L2||  {}\mrightarrow{}  \mBbbN{}||L1'  @  L2'||
\mvdash{}  istype(increasing(f2;||L1  @  L2||)  \mwedge{}  (\mforall{}j:\mBbbN{}||L1  @  L2||.  (L1  @  L2[j]  =  L1'  @  L2'[f2  j])))


By

---

Latex:
Auto

---

Home Index