p:. prime(p)  p = 0 & (p ~ 1) & (a:. a | p  (a ~ 1)  (a ~ p))

By:	RepD THEN (FwdThru Thm* a:. prime(a)  atomic(a) [-1]) THEN (Unfold `atomic` -1) THEN GenRepD THEN (Try Trivial)

1

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

11 steps

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