Nuprl - Proof: array shift wf 1 2

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

1. T : Type
2. i :

3. j : {i...}
4. a : [T]Array
5. a.l = i & a.u = j
6. m :

a[++m].l = i+m & a[++m].u = j+m

By:	Analyze 4 THEN Analyze 5 THEN Repeat (Unfolds [`array_shift`;`array_lb`;`array_ub`] 0) THEN Rewrite (DepthC (pi1_evalC ORELSEC pi2_evalC)) 0

Generated subgoal:

1 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 = i+m & m1+m = j+m
1 step

About:

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