1. r : 
2. s : {s':| CoPrime(r,s') }
3. a : 
4. b : 
  x:. ((x = a mod r) & (x = b mod s))

1

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

9 steps

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