Def  x:A. B(x) == x:AB(x)

is mentioned by

Thm*  n:{1...}. f:(Prime). f is a factorization of n	[prime_factorization_exists2]
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*  p:.  Thm*  prime(p) Thm*   Thm*  (a,b:, e:({a..b}). Thm*  (a<b  p | ( i:{a..b}. e(i))  (i:{a..b}. p | e(i)))	[prime_divs_mul_via_intseg]
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  (i:{a..b}. 0<f(i))	[eval_factorization_one_b]

In prior sections: core quot 1 LogicSupplement int 2 num thy 1 SimpleMulFacts IteratedBinops

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