(18steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

At: member upto 1 2

1. d:
2. 0 < d
3. i,j:. j-i = d-1 (k:. (k upto(i;j)) ik & k < j)
i,j:. j-i = d (k:. (k upto(i;j)) ik & k < j)

By:
UnivCD
THEN
RecUnfold `upto` 0
THEN
SplitOnConclITE


Generated subgoals:

14. i:
5. j:
6. j-i = d
7. k:
8. i < j
(k [i / upto(i+1;j)]) ik & k < j
7 steps
 
24. i:
5. j:
6. j-i = d
7. k:
8. ji
(k nil) ik & k < j
1 step

About:
consnilintnatural_numberaddsubtractless_thanequalimpliesandall

(18steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc