(4steps total)
PrintForm
Definitions
graph
1
1
Sections
Graphs
Doc
At:
length
upto
j:
, i:
j. ||upto(i;j)|| = j-i
By:
Assert (
d,j,i:
. j-i = d
||upto(i;j)|| = d)
Generated subgoals:
1
d,j,i:
. j-i = d
||upto(i;j)|| = d
2
steps
 
2
1.
d,j,i:
. j-i = d
||upto(i;j)|| = d
j:
, i:
j. ||upto(i;j)|| = j-i
1
step
About:
(4steps total)
PrintForm
Definitions
graph
1
1
Sections
Graphs
Doc