1. a : 
2. (a ~ 1)
3. b:. b | a  (b ~ 1)  (b ~ a)
4. b : 
5. c : 
6. a | bc
7. gcd(a;b) ~ 1
8. gcd(a;c) ~ 1
9. CoPrime(a,b)
10. CoPrime(a,c)
11. CoPrime(a,bc)
  a | b  a | c

1

11. 1 | a 12. 1 | bc 13. z:. z | a & z | bc  z | 1   a | b  a | c

3 steps

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