---

Step * 2 1 1 of Lemma nth_tl_factor


1. T : Type
2. n : ℤ
3. 0 < n
4. ∀as:T List. (((n - 1) ≤ ||as||) ⇒ (nth_tl(n - 1;as) = (Π n - 1 ≤ i < ||as||. [as[i]]) ∈ (T List)))
5. 0 < n
6. as : T List
7. n ≤ ||as||
8. ||as|| ≥ 1 
⊢ (Π n - 1 ≤ i < ||as|| - 1. [as[i + 1]]) = (Π n ≤ i < ||as||. [as[i]]) ∈ (T List)
BY
{ ((RWN 1 (LemmaWithC [`k',1] `mon_itop_shift`) 0 THENM RW IntNormC 0) THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  \mforall{}as:T  List.  (((n  -  1)  \mleq{}  ||as||)  {}\mRightarrow{}  (nth\_tl(n  -  1;as)  =  (\mPi{}  n  -  1  \mleq{}  i  <  ||as||.  [as[i]])))
5.  0  <  n
6.  as  :  T  List
7.  n  \mleq{}  ||as||
8.  ||as||  \mgeq{}  1 
\mvdash{}  (\mPi{}  n  -  1  \mleq{}  i  <  ||as||  -  1.  [as[i  +  1]])  =  (\mPi{}  n  \mleq{}  i  <  ||as||.  [as[i]])


By

---

Latex:
((RWN  1  (LemmaWithC  [`k',1]  `mon\_itop\_shift`)  0  THENM  RW  IntNormC  0)  THEN  Auto)

---

Home Index