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

At: append upto
i,j,k:. ij jk (upto(i;k) ~ (upto(i;j) @ upto(j;k)))
By: Assert (d:, i,j,k:. j-i = d jk (upto(i;k) ~ (upto(i;j) @ upto(j;k))))
Generated subgoals:

1 d:, i,j,k:. j-i = d jk (upto(i;k) ~ (upto(i;j) @ upto(j;k)))4 steps
 
21. d:, i,j,k:. j-i = d jk (upto(i;k) ~ (upto(i;j) @ upto(j;k)))
i,j,k:. ij jk (upto(i;k) ~ (upto(i;j) @ upto(j;k)))		1 step

About:
intsubtractequalsqequalimpliesall

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