From: wyniijj5@gmail.com   
      
   The proof is revised (bug fixed), even shorter (109 lines)!   
      
   ----------   
   This file is intended a proof of Collatz Conjecture. The contents may be   
   updated anytime.   
   https://sourceforge.net/projects/cscall/files/MisFiles/Coll-proo   
   -en.txt/download   
      
   The text is converted by google translate with modest modification from   
   https://sourceforge.net/projects/cscall/files/MisFiles/Coll-proo   
   -zh.txt/download   
   Reader might want to try different translator or different settings.   
      
   +---------+   
   | Preface |   
   +---------+   
      3x+1 problem: For any integer n greater than or equal to 1, if n is odd,   
      multiply by 3 and add 1. If n is even, divide by 2.   
      The question is, will all numbers be calculated to 1 using this method? The   
      following proof states that the answer is yes, they will always be   
   calculated   
      to 1. Proving this problem using Peano's axioms like axiomatic system is   
      difficult (or would be very lengthy), so an algorithm (Turing machine model)   
      is used for proof.   
      
   -----------------------------------------------------------------------------   
   Collatz function ::=   
      
         int cop(int n) {   
           if(n<=1) {   
             if(n<1) {   
               throw Error;   
             }   
             return 1;     // 1 is the iteration endpoint   
           }   
           if(n%2) {   
             return 3*n+1; // Odd number rule   
           } else {   
             return n/2;   // Even number rule    
           }   
         }   
      
   Collatz number: If an integer n, n∈N<1,+1>, after the cop iteration will   
       eventually calculate to 1 (i.e., cop(...cop(n))=1), then n is a Collatz   
       number. Otherwise n is not a Collatz number.   
      
   Collatz Problem: For each integer n, n∈N<1,+1>, is n a Collatz number? IOW,   
       the question is equivalent to asking whether the following procedure rcop   
       terminates or not.   
      
         void rcop(int n) {   
           for(;n!=1;) {   
             n=cop(n);   
           }   
         }   
      
   Prop: For any n∈N<1,+1>, the cop iteration operation terminates.   
     Proof: Let procedure rcop2 decomposes the n in rcop into n= a+b form.   
      
           void rcop2(int n) {   
             int a=n, b=0;   
             for(;a+b!=1;) { // a+b measure point A (a+b is equivalent to n in the   
                             // cop iteration process)   
               if((a%2) != 0) {   
                 --a; ++b; // a,b are adjusted so that a remains even, so that the   
                           // following algorithm can be performed and remains   
                           // equivalent to the cop(n) iteration.   
               }   
               // a/b measures point B   
               if((b%2)!=0) { // Equivalent to (a+b)%2 (because a is even)   
                 a= 3*a;   
                 b= 3*b+1; // 3*(a+b)+1 =(3*a) +(3*b+1)   
               }   
               a= a/2; // (a+b)/2 will be executed in each iteration   
               b= b/2;   
             }   
           }   
      
         Let n be odd and there be no --a, ++b process. Assume that each odd   
         operation is paired with an even operation. Then, at measurement point B,   
         we have:   
      
         a₁= n-1   
         aₓ= (3*aₓ₋₁)/2 =... = (n-1)*(3/2)ˣ⁻¹   
         b₁= 1   
         bₓ= (3*bₓ₋₁+1)/2=... = 2*(3/2)ˣ⁻¹ -1   
      
         aₓ/bₓ= (aₓ₋₁)/(bₓ₋₁) = ((n-1)*(3/2)ˣ⁻¹   
   /(2*(3/2)ˣ⁻¹ -1)   
                              =... = (n-1)/(2- 1/(3/2)ˣ⁻¹)   
      
         Interim summary: aₓ/bₓ < aₓ₋₁/bₓ₋₁, and lim{x->∞}   
   aₓ/bₓ = (n-1)/2.   
           Because "approximately half the limit value (n-1)/2" (not including the   
           actual iterations which involve --a and ++b operations making aₓ   
   smaller   
           and bₓ larger) is recursively true, we can deduce that:   
           (1) The actual value of aₓ/bₓ will decrease to the final value 0,   
   and   
               a=0, eventually.   
           (2) The number of times bₓ is odd is less than the number of times   
   bₓ is   
               even (there are two, or more, consecutive even operations).   
      
         Let r= a/b, aₓ=0. The value aₓ₋₁, before iterating to 0, is 1   
   (measurement   
         point A). At this point, rₓ₋₁ is a small value, relative to the   
   initial   
         value r₁ (the value of aₓ/bₓ can be considered as decreasing   
   continuously   
         by (n-1)/2). When n>=5, bₓ₋₁ (=aₓ₋₁*rₓ₋₁ =rₓ₋₁)   
   is guaranteed to be less   
         than n-1. Therefore, nₓ₋₁= aₓ₋₁+bₓ₋₁ < 1+(n-1) <=>   
   nₓ₋₁