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

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

None

About:
intnatural_numberaddsubtractequalimpliesall

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