Nuprl - Proof: member upto 2 2

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

At: member upto 2 2

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

(k upto(i;j)) ik & k < j

By: RecUnfold `upto` 0 THEN SplitOnConclITE

Generated subgoals:

1 6. i < j
(k [i / upto(i+1;j)]) ik & k < j 1 step

2 6. ji
(k nil) ik & k < j 1 step

About:

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