---

Step * 2 1 of Lemma cons_sublist_cons


1. [T] : Type
2. x1 : T
3. x2 : T
4. L1 : T List
5. L2 : T List
6. x1 = x2 ∈ T
7. f : ℕ||L1|| ⟶ ℕ||L2||
8. increasing(f;||L1||)
9. ∀j:ℕ||L1||. (L1[j] = L2[f j] ∈ T)
⊢ ∃f:ℕ||L1|| + 1 ⟶ ℕ||L2|| + 1. (increasing(f;||L1|| + 1) ∧ (∀j:ℕ||L1|| + 1. ([x1 / L1][j] = [x2 / L2][f j] ∈ T)))
BY
{ ((Unfold `increasing` 0 THEN InstConcl [λi.if (i =z 0) then 0 else (f (i - 1)) + 1 fi ]) THEN Reduce 0) }

1
.....wf..... 
1. T : Type
2. x1 : T
3. x2 : T
4. L1 : T List
5. L2 : T List
6. x1 = x2 ∈ T
7. f : ℕ||L1|| ⟶ ℕ||L2||
8. increasing(f;||L1||)
9. ∀j:ℕ||L1||. (L1[j] = L2[f j] ∈ T)
⊢ λi.if (i =z 0) then 0 else (f (i - 1)) + 1 fi  ∈ ℕ||L1|| + 1 ⟶ ℕ||L2|| + 1

2
1. [T] : Type
2. x1 : T
3. x2 : T
4. L1 : T List
5. L2 : T List
6. x1 = x2 ∈ T
7. f : ℕ||L1|| ⟶ ℕ||L2||
8. increasing(f;||L1||)
9. ∀j:ℕ||L1||. (L1[j] = L2[f j] ∈ T)
⊢ (∀i:ℕ(||L1|| + 1) - 1
     if (i =z 0) then 0 else (f (i - 1)) + 1 fi  < if (i + 1 =z 0) then 0 else (f ((i + 1) - 1)) + 1 fi )
∧ (∀j:ℕ||L1|| + 1. ([x1 / L1][j] = [x2 / L2][if (j =z 0) then 0 else (f (j - 1)) + 1 fi ] ∈ T))

3
.....wf..... 
1. T : Type
2. x1 : T
3. x2 : T
4. L1 : T List
5. L2 : T List
6. x1 = x2 ∈ T
7. f : ℕ||L1|| ⟶ ℕ||L2||
8. increasing(f;||L1||)
9. ∀j:ℕ||L1||. (L1[j] = L2[f j] ∈ T)
10. f1 : ℕ||L1|| + 1 ⟶ ℕ||L2|| + 1
⊢ istype((∀i:ℕ(||L1|| + 1) - 1. f1 i < f1 (i + 1)) ∧ (∀j:ℕ||L1|| + 1. ([x1 / L1][j] = [x2 / L2][f1 j] ∈ T)))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  x1  :  T
3.  x2  :  T
4.  L1  :  T  List
5.  L2  :  T  List
6.  x1  =  x2
7.  f  :  \mBbbN{}||L1||  {}\mrightarrow{}  \mBbbN{}||L2||
8.  increasing(f;||L1||)
9.  \mforall{}j:\mBbbN{}||L1||.  (L1[j]  =  L2[f  j])
\mvdash{}  \mexists{}f:\mBbbN{}||L1||  +  1  {}\mrightarrow{}  \mBbbN{}||L2||  +  1
      (increasing(f;||L1||  +  1)  \mwedge{}  (\mforall{}j:\mBbbN{}||L1||  +  1.  ([x1  /  L1][j]  =  [x2  /  L2][f  j])))


By

---

Latex:
((Unfold  `increasing`  0  THEN  InstConcl  [\mlambda{}i.if  (i  =\msubz{}  0)  then  0  else  (f  (i  -  1))  +  1  fi  ])
  THEN  Reduce  0
  )

---

Home Index