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

At: append upto 1 3
1. d:
2. 0 < d
3. i,j,k:. j-i = d-1 jk (upto(i;k) ~ (upto(i;j) @ upto(j;k)))
4. i:
5. j:
6. k:
7. j-i = d
8. jk
9. i < k
10. i < j
[i / upto(i+1;k)] ~ [i / (upto(i+1;j) @ upto(j;k))]
By:
Analyze
THEN
EasyHyp
Generated subgoals:

None

About:
consintnatural_numberaddsubtractless_thanequalsqequalimpliesall

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