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

At: upto wf 1 1
1. d:
2. 0 < d
3. i,j:. j-i = d-1 upto(i;j) {i..j} List
4. i:
5. j:
6. j-i = d
7. i < j
upto(i+1;j) {i..j} List
By: GenConcl (upto(i+1;j) = l)
Generated subgoal:

1 upto(i+1;j) {(i+1)..j} List1 step

About:
listintnatural_numberaddsubtractless_thanequalmemberimpliesall

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