Step * 1 1 2 1 of Lemma cons_sublist_cons


1. Type
2. x1 T
3. x2 T
4. L1 List
5. L2 List
6. : ℕ||L1|| 1 ⟶ ℕ||L2|| 1
7. increasing(f;||L1|| 1)
8. ∀j:ℕ||L1|| 1. ([x1 L1][j] [x2 L2][f j] ∈ T)
9. [x1 L1][0] [x2 L2][f 0] ∈ T
10. 0 ≠ 0
11. : ℕ||L1|| 1
⊢ (f j) 1 ∈ ℕ||L2||
BY
(InstLemma `increasing_lower_bound` [||L1|| 1;f;j] THEN Auto) }


Latex:


Latex:

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


By


Latex:
(InstLemma  `increasing\_lower\_bound`  [||L1||  +  1;f;j]  THEN  Auto)




Home Index