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

At: member upto 1 2 2
1. d:
2. 0 < d
3. i,j:. j-i = d-1 (k:. (k upto(i;j)) ik & k < j)
4. i:
5. j:
6. j-i = d
7. k:
8. ji
(k nil) ik & k < j
By: Obvious
Generated subgoals:

None

About:
nilintnatural_numbersubtractless_thanequalimpliesandall

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