1. i : 
2. j : 
3. n : 
4. (i rem n)+(j rem n)
4. =
4. (((i rem n)+(j rem n))  n)n+(((i rem n)+(j rem n)) rem n)
5. i = (i  n)n+(i rem n)
6. j = (j  n)n+(j rem n)
7. i+j = ((i+j)  n)n+((i+j) rem n)
8. (i rem n)  n
9. (j rem n)  n
10. (((i rem n)+(j rem n)) rem n)  n
11. ((i+j) rem n)  n
  ((i  n)+(j  n)+(((i rem n)+(j rem n))  n))n+(((i rem n)+(j rem n)) rem n)
  =
  ((i+j)  n)n+((i+j) rem n)

By:	i+j = ((i  n)+(j  n))n+(i rem n)+(j rem n)  Asserted  {Hyp:5 Hyp:6 then rearrange } THEN ((i  n)+(j  n))n+(i rem n)+(j rem n) = ((i  n)+(j  n)+(((i rem n)+(j rem n))  n))n+(((i rem n)+(j rem n)) rem n) Asserted {Hyp:4 then rearrange }

None

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