m:
, n:m. upto(m)[n] = nas,bs:T List, i:||as||. (as @ bs)[i] = as[i]n:. ||upto(n)|| ~ nas,bs:T List, i:{||as||..(||as||+||bs||)
}. (as @ bs)[i] = bs[(i-||as||)]| Rank | Theorem | Name |
| 2 | m:, n:m. upto(m)[n] = n | [select_upto] |
| cites the following: | ||
| 1 | as,bs:T List, i:||as||. (as @ bs)[i] = as[i] | [select_append_front] |
| 1 | n:. ||upto(n)|| ~ n | [length_upto] |
| 1 | as,bs:T List, i:{||as||..(||as||+||bs||)}. (as @ bs)[i] = bs[(i-||as||)] | [select_append_back] |