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

At: member upto 2 2 1
1. d,i,j:. j-i = d (k:. (k upto(i;j)) ik & k < j)
2. i:
3. j:
4. k:
5. ij
6. i < j
(k [i / upto(i+1;j)]) ik & k < j
By: Obvious
Generated subgoals:

None

About:
consintnatural_numberaddsubtractless_thanequalimpliesandall

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