Nuprl - Proof: array shift wf 1 1 1 1

(10steps total) PrintForm Definitions array 1 Sections StandardLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: array shift wf 1 1 1 1

1. T : Type
2. i :

3. j : {i...}
4. n :

5. m1 : {n...}
6. a2 : {n..m1

}

T
7. <n,m1,a2>.l = i & <n,m1,a2>.u = j
8. m :

<(n+m),(m1+m),(

j.a2(j-m))>

n:

m:{n...}

{n..m

}

T

By:

Auto

Generated subgoals:

1 7. <n,m1,a2>.l = i
8. <n,m1,a2>.u = j
9. m :
  n+mm1+m
1 step

2 7. <n,m1,a2>.l = i
8. <n,m1,a2>.u = j
9. m :
10. j1 : {(n+m)..(m1+m)}
  nj1-m
1 step

3 7. <n,m1,a2>.l = i
8. <n,m1,a2>.u = j
9. m :
10. j1 : {(n+m)..(m1+m)}
  j1-m<m1
1 step

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(10steps total) PrintForm Definitions array 1 Sections StandardLIB Doc