L:
List, i,j:||L||. 0 < L[i] 
L[i--][j] = if j=
i
L[j]-1 else L[j] fin:, f:(n
T), i:n. mklist(n;f)[i] = f(i)| Rank | Theorem | Name |
| 3 | Thm* L: List, i,j:||L||. 0 < L[i] L[i--][j] = if j=i L[j]-1 else L[j] fi | [list-dec-select] |
| cites | ||
| 2 | Thm* n:, f:(nT), i:n. mklist(n;f)[i] = f(i) | [mklist_select] |