Step
*
1
of Lemma
segment_factor
1. T : Type
2. as : T List
3. i : {0...||as||}
4. j : {i...||as||}
⊢ firstn(j - i;nth_tl(i;as)) = (Π i ≤ k < j. [as[k]]) ∈ (T List)
BY
{ (RWO "firstn_factor" 0 THENA Auto') }
1
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)
Latex:
Latex:
1. T : Type
2. as : T List
3. i : \{0...||as||\}
4. j : \{i...||as||\}
\mvdash{} firstn(j - i;nth\_tl(i;as)) = (\mPi{} i \mleq{} k < j. [as[k]])
By
Latex:
(RWO "firstn\_factor" 0 THENA Auto')
Home
Index