1. a : 
2. b : 
3. f : {a..b}
4. j : {a..b}
5. 0<f(j)
  j | {a..b}(f)

By:	Rewrite by Thm*  a,b:, f:({a..b}), z:{a..b}. Thm*  0<f(z)  {a..b}(f) = z{a..b}(reduce_factorization(f; z)) Using:[z:= j]

1

j | j{a..b}(reduce_factorization(f; j))

1 step

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