Selected Objects

Introduction		Introductory Remarks
THM	prime_divides_square	A number and its square have the same prime divisors. a:. prime(a)  (x:. a | xx  a | x)
THM	nat_descent	There is no inhabited class of natural numbers in which one can always find a smaller member. P:(Prop). (x:. P(x)  (x':. x'<x & P(x')))  (x:. P(x))
THM	two_sqr_roots_LEMMA1 (Proof Gloss)	Lemma for Thm: two sqr roots, rewriting (pp = 2qq) to (qq = 2p'p') p:, q:. pp = 2qq  (p':. p'<p & qq = 2p'p')
THM	two_sqr_roots (Proof Gloss)	2 has no rational square root. (p:, q:. pp = 2qq)
COM	two_sqr_roots_example1	An example of the two step rewrite ...
THM	primes_sqr_roots_LEMMA1 (Proof Gloss)	Lemma for Thm: primes sqr roots, rewriting (pp = aqq) to (qq = ap'p') a:. prime(a)  (p:, q:. pp = aqq  (p':. p'<p & qq = ap'p'))
THM	primes_sqr_roots (Proof Gloss)	Primes have no rational square roots. a:. prime(a)  (p:, q:. pp = aqq)
COM	primes_sqr_roots_example1	An example of the two step rewrite ...

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html