a:, b:, f:({a..b}), p:.
  is_prime_factorization(a; b; f)
  
  prime(p)  p | {a..b}(f)  p  {a..b} & 0<f(p)

By:	IntroduceGuardForms (<prop> & <prop>) 0 THEN Def of {<int>..<int>}(<exponents>) ...

1

1. a :  2. b :  3. f : {a..b} 4. p :  5. is_prime_factorization(a; b; f) 6. prime(p) 7. p | ( i:{a..b}. if(i))   p  {a..b} & 0<f(p)

11 steps

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