1. a : 
2. a = 0
3. (a ~ 1)
4. reducible(a)
5. b : 
6. b | a
  (b ~ 1)  (b ~ a)

By:	(NegateConcl2 THENA BackThru Thm* Dec(P)  Stable{P}) THEN (RWH (LemmaC Thm* (A  B)  A & B) -1) THEN (Analyze -1)

1

7. (b ~ 1) 8. (b ~ a)   False

6 steps

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