(6steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

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+k1 step

About:
listconsintnatural_numberaddsubtractless_thanuniverseequalimpliesall

(6steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc