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

At: member upto 1 1

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

By:
UnivCD
THEN
RecUnfold `upto` 0


Generated subgoal:

11. i:
2. j:
3. j-i = 0
4. k:
(k if i < j [i / upto(i+1;j)] else nil fi) ik & k < j
1 step

About:
consnilifthenelseintnatural_number
addsubtractless_thanequalimpliesandall

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