a:, n:. an  (a  n) = ((a-n)  n)+1

1

1. a :  2. n :  3. an 4. a = (a  n)n+(a rem n) 5. a-n = ((a-n)  n)n+((a-n) rem n) 6. (a rem n)  n 7. ((a-n) rem n)  n   (a  n) = ((a-n)  n)+1

2 steps

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