1. r : 
2. s : 
3. CoPrime(r,s)
4. a : 
5. b : 
6. x:. ((x = 1 mod r) & (x = 0 mod s))
7. x:. ((x = 1 mod s) & (x = 0 mod r))
  x:. ((x = a mod r) & (x = b mod s))

1

6. p :  7. (p = 1 mod r) & (p = 0 mod s)  [not for witness] 8. q :  9. (q = 1 mod s) & (q = 0 mod r)  [not for witness]   x:. ((x = a mod r) & (x = b mod s))

5 steps

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