(4steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc

At: length upto

j:, i:j. ||upto(i;j)|| = j-i

By: Assert (d,j,i:. j-i = d ||upto(i;j)|| = d)

Generated subgoals:

1 d,j,i:. j-i = d ||upto(i;j)|| = d 2 steps
 
21. d,j,i:. j-i = d ||upto(i;j)|| = d
j:, i:j. ||upto(i;j)|| = j-i
1 step

About:
intnatural_numbersubtractequalimpliesall

(4steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc