Nuprl - Proof: array shift wf 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. 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,m1,a2>.l+m),(<n,m1,a2>.u+m),(

j.<n,m1,a2>[(j-m)])>

n:

m:{n...}

{n..m

}

T

By:	Unfolds [`array_el`;`array_lb`;`array_ub`] 0 THEN Rewrite (DepthC (pi1_evalC ORELSEC pi2_evalC)) 0 THEN Reduce 0

Generated subgoal:

1 <(n+m),(m1+m),(j.a2(j-m))> n:m:{n...}{n..m}T
4 steps

About:

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

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