Def  reduce_factorization(f; j)(i) == if i=j f(i)-1 else f(i) fi

is mentioned by

Thm*  a:, b:, f:({a..b}), p:. Thm*  is_prime_factorization(a; b; f) Thm*   Thm*  prime(p) Thm*   Thm*  p | {a..b}(f)  {a..b}(f) = p{a..b}(reduce_factorization(f; p))	[remove_prime_factor]
Thm*  a,b:, f:({a..b}), j:{a..b}. Thm*  0<f(j) Thm*   Thm*  is_prime_factorization(a; b; f) Thm*   Thm*  is_prime_factorization(a; b; reduce_factorization(f; j))	[reduce_fac_pres_isprimefac]
Thm*  a:, b:, f:({a..b}), j:{a..b}. Thm*  2j  0<f(j)  {a..b}(reduce_factorization(f; j))<{a..b}(f)	[eval_reduce_factorization_less]
Thm*  a,b:, f:({a..b}), z:{a..b}. Thm*  0<f(z)  {a..b}(f) = z{a..b}(reduce_factorization(f; z))	[eval_factorization_pluck]
Thm*  a,b:, f:({a..b}), j:{a..b}. Thm*  0<f(j)  (i:{a..b}. reduce_factorization(f; j)(i)f(i))	[reduce_factorization_bound]
Thm*  a,b:, f,g:({a..b}), j:{a..b}. Thm*  0<f(j) Thm*   Thm*  0<g(j)  reduce_factorization(f; j) = reduce_factorization(g; j)  f = g	[reduce_factorization_cancel]

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html