Nuprl - Proof: select upto 1

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

d,i,j:, k:d. j-i = d upto(i;j)[k] = i+k

By: InductionOnNat THEN RecUnfold `upto` 0 THEN SplitOnConclITE THEN CaseNat 0 `k' THEN Reduce 0

Generated subgoal:

1 1. d:
2. 0 < d
3. i,j:, k:(d-1). j-i = d-1 upto(i;j)[k] = i+k
4. i:
5. j:
6. k: d
7. j-i = d
8. i < j
9. k = 0
[i / upto(i+1;j)][k] = i+k 3 steps

About:

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