Def  prime(a) == a = 0 & (a ~ 1) & (b,c:. a | bc  a | b  a | c)

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*  !{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]
Def  Prime == {x:| prime(x) }	[prime_nats]

In prior sections: num thy 1

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