(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:

11. 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:
listconsintnatural_numberaddsubtractequalmemberimpliesall

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