At:
select upto
1
1
1.
d:
2.
0 < d
3.
i,j:
, k:
(d-1). j-i = d-1 
upto(i;j)[k] = i+k
4.
i:
5.
j:
6.
k:
d
7.
j-i = d
8.
i < j
9.
k = 0
[i / upto(i+1;j)][k] = i+k
By:
RWO
Thm*
a:T, as:T List, i:
. 0 < i 
i
||as|| 
[a / as][i] = as[(i-1)]
0
Generated subgoals:
1 | k ||upto(i+1;j)|| | 1 step |
  |
2 | upto(i+1;j)[(k-1)] = i+k | 1 step |
About: