1. a : 
2. a = 0
3. (a ~ 1)
4. b,c:. a | bc  a | b  a | c
  reducible(a)

1

5. b :  6. c :  7. (b ~ 1) 8. (c ~ 1) 9. a = bc   False

4 steps

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html