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

At: append upto 2
1. 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)))
By:
UnivCD
THEN
InstHyp [j-i] 1
THEN
EasyHyp
Generated subgoals:

None

About:
intsubtractequalsqequalimpliesall

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