Nuprl - Proof: append upto 1

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

d:, i,j,k:. j-i = d jk (upto(i;k) ~ (upto(i;j) @ upto(j;k)))

By: InductionOnNat THEN UnivCD THEN RW (AddrC [1] (RecUnfoldC `upto`) THENC AddrC [2;1] (RecUnfoldC `upto`)) 0 THEN SplitOnConclITE THEN SplitOnConclITE THEN Reduce 0 THEN Try (Complete Auto)

Generated subgoals:

1 1. i:
2. j:
3. k:
4. j-i = 0
5. jk
6. i < k
7. ji
[i / upto(i+1;k)] ~ upto(j;k) 1 step

2 1. i:
2. j:
3. k:
4. j-i = 0
5. jk
6. ki
7. ji
nil ~ upto(j;k) 1 step

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

About:

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

1	1. `i:` 2. `j:` 3. `k:` 4. `j-i = 0` 5. `jk` 6. `i < k` 7. `ji` `[i / upto(i+1;k)] ~ upto(j;k)`	1 step

2	1. `i:` 2. `j:` 3. `k:` 4. `j-i = 0` 5. `jk` 6. `ki` 7. `ji` `nil ~ upto(j;k)`	1 step

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