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

At: length upto 2
1. d,j,i:. j-i = d ||upto(i;j)|| = d
j:, i:j. ||upto(i;j)|| = j-i
By:
Auto
THEN
InstHyp [j-i;j;i] 1
Generated subgoals:

None

About:
intnatural_numbersubtractequalimpliesall

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