Math 405   Constructive Proof of FTA (Fundamental Theorem of Arithmetic)
									4 Feb.

	Construct the prime factors of a positive integer n.
	Use brute force.  Store the factors in factorVec.
    
	Initialize.  Set divisor to 2.  Set currentN to n.

/*	Loop Invariant:

	a. Each element in factorVec is a prime number and a divisor of n.
	b. If g is an integer with 1 < g < divisor, then g does not divide 
	   currentN.
	c. currentN is a factor of n.
	d. The product of the elements in factorVec and currentN equals n.

	Finiteness of loop:
	Each trip through the loop either decreases currentN or 
	increases divisor.
 */
	while ( ( divisor * divisor ) <= currentN )
	    if divisor is a factor of currentN then
		Assert1: divisor is prime.
		Append divisor to factorVec.
		Reduce currentN by divisor.    currentN = currentN / divisor.
	    else
		if ( divisor is 2 ) Set divisor to 3.
		else Increase divisor by 2.

	By Loop Invariant, the product of elements in factorVec and currentN 
	is n and each element in factorVec is prime. 

	Assert2: currentN is prime.
	Append currentN to factorVec.

	Thus the product of the elements in factorVec equals n and
	each element in factorVec is prime and a divisor of n.

	Prove that the Loop invariant is true on each trip through the loop.
	Use math induction.
	Base case.  factorVec is empty.  So the first two lines are true
	by default.  Since currentN is n, currentN is a factor of n.
	The product of no primes is 1 (by default). (Recall 0! = 1.)
	So product of elements of factorVec and currentN is n.

	Show Loop invariant remains true on trip k.
	Assume Loop invariant is true at top of trip k.(IA induction assumption)
	Prove Loop invariant is true at top of next trip k + 1.

	Either divisor is a factor of currentN or not.

	Case divisor is a factor of currentN.
	Append divisor to factorVec.
	a. By IA each element but last of factorVec is prime and a divisor of n.
	   By assert1, last element of factorVec or divisor is prime.
	   So each element of factorVec is prime.
	   divisor is a factor of currentN. By IA currentN is a factor of n.
	   So divisor is a factor of n by transitivity of factor.
	   So each element of factorVec is a divisor of n.

	Assert1. divisor is prime.
	Proof.  Suppose not.  Suppose divisor = a * b for 1 < a <= b < divisor.
	So a is a factor of divisor and divisor is a factor of currentN.
	So a is a factor of currentN.
	By IA, each g with 1 < g < divisor does not divide currentN.
	When g = a, this is a contradiction.  So the assumption that divisor
	is not prime is false.  divisor is prime.

	b. Since divisor does not change during this trip and the second line 
	   of the Loop invariant is true at top, the second line is true at
	   bottom.

	c. At top of loop currentN is a factor of n.
	   currentN / divisor is an integer factor of currentN since
	   divisor is a factor of currentN.
	   By transitivity of factor, currentN / divisor, the new currentN
	   is a factor of n.

	d. At top of loop, product of elements of factorVec and currentN = n.
	   So product of elements of factorVec and divisor and 
		currentN / divisor = n.
	   After the append and the reduce n steps,
	    	the product of elements of factorVec and currentN = n.

	Case divisor is not a factor of currentN.
	factorVec and currentN do not change. So a, c and d are true at
	top of loop by IA at step k and so true at top of loop at step k + 1.
	Only b requires proof.
	Either divisor moves from 2 to 3 or increases by 2.
	Subcase divisor moves from 2 to 3.
	The only g with 1 < g < divisor = 3 is g = 2.  The current case is 
	divisor = 2 is not a factor of n.  So statement b is true.

	Subcase divisor increases by 2.
	Consider g = divisor and g = divisor + 1.
	If g = divisor, divisor is not a factor of n because of the current
	case.
	If g = divisor + 1, then g is even and so g = 2 * g' for 
	g' < old divisor.  By IA each of 2 and g' does not divide currentN.
	So g = 2 * g' does not divide currentN.

	So loop invariant is true for each trip through the loop by
	math induction.


	Loop is finite.
	Proof. Each trip through the loop either reduces n by divisor or 
	increases divisor by 1 (once) or 2.  The loop continues as long as
	divisor * divisor <= currentN.  So each trip through the loop either
	increases the left side or decreases the right side.  So the
	difference left side - right side decreases by at least one for
	each trip.  So the difference which starts at n - 4 and which
	decreases by at least 1 on each trip must be negative within n - 3
	trips through the loop.

	Assert2. currentN is prime.
	Proof.  Suppose not.  Suppose currentN is not prime.  
	So currentN = a * b where 1 < a <= b < currentN.
	Claim. a < divisor.  If not, a >= divisor. Since b >= a, b > divisor,
	So a * b >= divisor^2.  But a * b = currentN.
	Since assert2 is outside the while loop, divisor^2 > currentN.
	So currentN = a * b >= divisor^2 > currentN, which is not true.
	The contradiction means that the claim is true.
	Since a < divisor, part b of the loop invariant is true
	and so a does not divide currentN.  But a is a factor of currentN.
	This contradiction means that currentN is prime.