---

Step * 1 1 of Lemma segment_factor


1. T : Type
2. as : T List
3. i : {0...||as||}
4. j : {i...||as||}
⊢ (Π 0 ≤ i1 < j - i. [nth_tl(i;as)[i1]]) = (Π i ≤ k < j. [as[k]]) ∈ (T List)
BY
{ (RWO "select_nth_tl" 0 THENA Auto') }

1
1. T : Type
2. as : T List
3. i : {0...||as||}
4. j : {i...||as||}
⊢ (Π 0 ≤ i1 < j - i. [as[i1 + i]]) = (Π i ≤ k < j. [as[k]]) ∈ (T List)

---

Latex:

---

Latex:

1.  T  :  Type
2.  as  :  T  List
3.  i  :  \{0...||as||\}
4.  j  :  \{i...||as||\}
\mvdash{}  (\mPi{}  0  \mleq{}  i1  <  j  -  i.  [nth\_tl(i;as)[i1]])  =  (\mPi{}  i  \mleq{}  k  <  j.  [as[k]])


By

---

Latex:
(RWO  "select\_nth\_tl"  0  THENA  Auto')

---

Home Index