---

Step * 2 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||
⊢ nth_tl(n - 1;tl(as)) = (Π n ≤ i < ||as||. [as[i]]) ∈ (T List)
BY
{ ((Assert ||as|| ≥ 1  BY Auto) THEN (RWO "4" 0 THENA Auto)) }

1
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 < ||tl(as)||. [tl(as)[i]]) = (Π n ≤ i < ||as||. [as[i]]) ∈ (T List)

---

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||
\mvdash{}  nth\_tl(n  -  1;tl(as))  =  (\mPi{}  n  \mleq{}  i  <  ||as||.  [as[i]])


By

---

Latex:
((Assert  ||as||  \mgeq{}  1    BY  Auto)  THEN  (RWO  "4"  0  THENA  Auto))

---

Home Index