a,a',b,b',y,y':.
  (a ~ a')  (b ~ b')  (y ~ y')  (GCD(a;b;y)  GCD(a';b';y'))

1

1. a :  2. a' :  3. b :  4. b' :  5. y :  6. y' :  7. a ~ a' 8. b ~ b' 9. y ~ y'   y | a & y | b & (z:. z | a & z | b  z | y)      y' | a' & y' | b' & (z:. z | a' & z | b'  z | y')

1 step

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