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

is mentioned by

Thm*  a,b:. prime(ab)  ab = a  ab = b	[prime_among_factors]
Thm*  x:{2...}, y:. prime(y)  x | y  x = y	[prime_nat_divby_self_only]
Thm*  b:. prime(b)  b | 1	[no_prime_divs_one_b]
Thm*  b:. b | 1  prime(b)	[no_prime_divs_one]
Thm*  b:. b | 1  prime(b)	[no_nat_prime_divs_one]
Thm*  x:. is_prime(x)	[prime_decider_wf]
Thm*  !{p:()| x:. p(x)  prime(x) }	[prime_decider_exists]
Thm*  x:. Dec(prime(x))	[decidable__prime]
Thm*  y:. prime(-y)  prime(y)	[prime_neg]
Thm*  x:{2...}. p:{2...}. px & prime(p) & p | x	[prime_or_smaller_prime_factor]
Thm*  x:{2...}. p:{2...}, c:{1...}. px & prime(p) & x = pc	[prime_or_smaller_prime_factor2]
Thm*  x:{2...}. prime(x)  (i,j:{2..x}. x = ij & prime(i))	[composite_with_prime_factor]
Thm*  x:. prime(x)  x<2  (i,j:{2..x}. x = ij)	[nonprime_nat]
Thm*  x:. prime(x)  (i:{2..x}. i | x)	[natprime_nondivs]
Thm*  x:. prime(x)  2x	[natprimes_lb]
Thm*  x:. prime(x)  2x & (i:{2..x}. i | x)	[prime_nat]
Thm*  x:, y,z:. x = yz  (x  z) = y	[div_inverts_nat_mul2]
Thm*  x,y:, z:. x = yz  (x  z) = y	[div_inverts_nat_mul]
Thm*  b:. b | 1  b = 1	[only_one_nat_divs_one]
Thm*  a,b:. a | b  (c:. b = ac)	[divides_def_on_nat]
Thm*  x,y:. xy	[mul_nat_plus]
Thm*  k:, i:{2..k}, j:. ij = k  2  j < k & i<k	[factors_smaller2]
Thm*  i,j:{2...}. i<ij & j<ij	[factors_smaller]
Thm*  i:{2...}, j:. j<ij	[factor_smaller2]
Thm*  i:{2...}, j:{1...}. j<ij	[factor_smaller]
Thm*  i,j:. 0<ij  iij & jij	[pos_mul_arg_boundsNat2]
Thm*  a,b:. 0<ab  0<a & 0<b	[pos_mul_arg_boundsNat]
Thm*  i,j:. iij & jij	[factors_bound]
Thm*  x,y:, z:. x<y  x<yz	[lt_mul_rt_by_pos]
Thm*  k:, n:, x,y:. kx+n = ky  xy	[factor_bound]
Thm*  x,y:, z:. xy  xyz	[le_mul_rt_by_pos]
Thm*  a,b:, m,n:. m = n  (ma = nb  a = b)	[mul_cancel_in_eq2]
Thm*  a,b:, n:. na = nb  a = b	[mul_cancel_in_eq1]
Thm*  a,b:, n:. nanb  ab	[nat_factor_cancel_rw]
Thm*  a,b,c,d:. a = b  c = d  ac = db	[mul_nat_com]
Thm*  a,b:. ab = 0  a = 0  b = 0	[prod_zero_iff_factor_zero]
Thm*  x,y:. xy = 1  x = 1 & y = 1	[nat_prod_one_iff_factors_one]

In prior sections: core well fnd int 1 bool 1 rel 1 quot 1 LogicSupplement int 2 union num thy 1

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