i,j:
, k:(j-i). upto(i;j)[k] = i+ka:T, as:T List, i:
. 0 < i 
i
||as|| [a / as][i] = as[(i-1)]j:, i:j. ||upto(i;j)|| = j-i 
| Theorem | Name |
| Thm* i,j:, k:(j-i). upto(i;j)[k] = i+k | [select_upto] |
| cites | |
| Thm* a:T, as:T List, i:. 0 < i i||as|| [a / as][i] = as[(i-1)] | [select_cons_tl] |
| Thm* j:, i:j. ||upto(i;j)|| = j-i | [length_upto] |