I
am playing with Coq and Isabelle now :) Formalizing the following:

fun p(a) = if (p(a) % 2 = 0) then (p(a div 2)) else (a).
The greatest divisor of a, which is power of two = p(a).

I want to show that the number of multiplication-addition series always equals p(a+1) and gives odd result for odd, even result for even and follows the formula (((3/2)**(p(a+1)))*a+1)-1.
This should be trivial by binary analysis.

I want to show that because of this even-odd differentiation, 3n+1 series is never called more than twice in a row. This follows from upper.

I want to show that for any even number, all following even numbers will have p(n) >= a(n) and that when looked from the position of n/2, that will come back to even if n/2 it started with was odd and vice versa, because div2 can't possibly change oddity of any upper level.

Thus, starting from even it leads to odd (next number) and starting from odd it leads to even (smaller number). Modulus is built in such way that p(n) for each even number is p(n)+1 related to it's division by two and this p(n) is how many times it will be divided by two, thus p(n) for any following even is big enough to lead to smaller number (n/2+1 for next one, as numbers grow, also this p(n) grows and thus, even leads to following(n)=n+1).

I want, thus, to show that the sequence always eventually leads to smaller number than it started from or 1.

Python check for those claims for first 100000 numbers (or just make the constant larger) is available.