Def  {a..b}(f) ==  i:{a..b}. if(i)

is mentioned by

Thm*  n:{1...}.  Thm*  h:({2..(n+1)}).  Thm*  n = {2..n+1}(h) & is_prime_factorization(2; (n+1); h)	[prime_factorization_exists]
Thm*  k:{2...}, n:, g:({2..k}). Thm*  2  n < k+1 Thm*   Thm*  (i:{2..k}. ni  0<g(i)  prime(i)) Thm*   Thm*  (h:({2..k}).  Thm*  ({2..k}(g) = {2..k}(h) & is_prime_factorization(2; k; h))	[prime_factorization_existsLEMMA]
Thm*  k:{2...}, g:({2..k}), z:{2..k}. Thm*  prime(z) Thm*   Thm*  (g':({2..k}).  Thm*  ({2..k}(g) = {2..k}(g') Thm*  (& g'(z) = 0 Thm*  (& (u:{2..k}. z<u  g'(u) = g(u)))	[can_reduce_composite_factor2]
Thm*  k:{2...}, g:({2..k}), x,y:{2..k}. Thm*  xy<k Thm*   Thm*  (h:({2..k}).  Thm*  ({2..k}(g) = {2..k}(h) Thm*  (& h(xy) = 0 Thm*  (& (u:{2..k}. xy<u  h(u) = g(u)))	[can_reduce_composite_factor]
Thm*  k:{2...}, g:({2..k}), x:{2..k}. Thm*  xx<k Thm*   Thm*  {2..k}(g) = {2..k}(split_factor1(g; x)) Thm*  & split_factor1(g; x)(xx) = 0 Thm*  & (u:{2..k}. xx<u  split_factor1(g; x)(u) = g(u))	[split_factor1_char]
Thm*  k:{2...}, g:({2..k}), x,y:{2..k}. Thm*  xy<k Thm*   Thm*  x<y Thm*   Thm*  {2..k}(g) = {2..k}(split_factor2(g; x; y)) Thm*  & split_factor2(g; x; y)(xy) = 0 Thm*  & (u:{2..k}. xy<u  split_factor2(g; x; y)(u) = g(u))	[split_factor2_char]
Thm*  a:{2...}, b:, g,h:({a..b}). Thm*  is_prime_factorization(a; b; g) Thm*   Thm*  is_prime_factorization(a; b; h)  {a..b}(g) = {a..b}(h)  g = h	[prime_factorization_unique]
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}), p:. Thm*  is_prime_factorization(a; b; f) Thm*   Thm*  prime(p)  p | {a..b}(f)  p  {a..b} & 0<f(p)	[prime_factorization_includes_prime_divisors]
Thm*  a,b:, f:({a..b}), j:{a..b}. 0<f(j)  j | {a..b}(f)	[factor_divides_evalfactorization]
Thm*  a,b:, f:({a..b}). ba  {a..b}(f) = {a..a}(f)	[eval_factorization_nullnorm]
Thm*  a,b:, f:({a..b}). ba  {a..b}(f) = 1	[eval_factorization_intseg_null]
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,g:({a..b}). Thm*  {a..b}(f){a..b}(g) = {a..b}(i.f(i)+g(i))	[eval_factorization_prod]
Thm*  a:{2...}, b:, f:({a..b}). Thm*  {a..b}(f) = 1  (i:{a..b}. f(i) = 0)	[eval_factorization_not_one]
Thm*  a:{2...}, b:, f:({a..b}). {a..b}(f) = 1  f = (x.0)	[eval_factorization_one_c]
Thm*  a:{2...}, b:, f:({a..b}). {a..b}(f) = 1  (i:{a..b}. 0<f(i))	[eval_factorization_one_b]
Thm*  a:{2...}, b:, f:({a..b}). {a..b}(f) = 1  (i:{a..b}. f(i) = 0)	[eval_factorization_one]
Thm*  a:, b:, f:({a..b}). {a..b}(f)	[eval_factorization_nat_plus]
Thm*  a,b:, j:{a..b}. {a..b}(trivial_factorization(j)) = j	[eval_trivial_factorization]
Thm*  a,c,b:, f:({a..b}). Thm*  ac  c<b  {a..b}(f) = {a..c}(f)cf(c){c+1..b}(f)	[eval_factorization_split_pluck]
Thm*  a,c,b:, f:({a..b}). Thm*  ac  cb  {a..b}(f) = {a..c}(f){c..b}(f)	[eval_factorization_split_mid]
Def  f is a factorization of k Def  == (x:Prime. k<x  f(x) = 0) & k = {2..k+1}(prime_mset_complete(f))	[prime_factorization_of]

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