l:T List, i:
||l||, j:(i+1), x:(i-j). l_interval(l;j;i)[x] = l[(j+x)]n:, f:(n
T), i:n. mklist(n;f)[i] = f(i)| Rank | Theorem | Name |
| 3 | l:T List, i:||l||, j:(i+1), x:(i-j). l_interval(l;j;i)[x] = l[(j+x)] | [select_l_interval] |
| cites the following: | ||
| 2 | n:, f:(nT), i:n. mklist(n;f)[i] = f(i) | [mklist_select] |