Nuprl - Proof: array shift wf 1 1 1 1 3

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

1. T : Type
2. i :

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

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

}

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

10. j1 : {(n+m)..(m1+m)

}

j1-m<m1

By:

SupInf

Generated subgoals:

None

About:

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