(6steps total)
PrintForm
Definitions
graph
1
1
Sections
Graphs
Doc
At:
upto
int
wf
1
d:
, i,j:
. j-i = d
upto(i;j)
List
By:
InductionOnNat
THEN
UnivCD
THEN
RecUnfold `upto` 0
THEN
SplitOnConclITE
THEN
Try (Complete Auto)
Generated subgoal:
1
1.
d:
2.
0 < d
3.
i,j:
. j-i = d-1
upto(i;j)
List
4.
i:
5.
j:
6.
j-i = d
7.
i < j
[i / upto(i+1;j)]
List
1
step
About:
(6steps total)
PrintForm
Definitions
graph
1
1
Sections
Graphs
Doc