The Coq mailing list

[Tambet <qtvali AT gmail.com>]

I also played with Isabelle and playing with both helped to formalize, what I want to prove. Anyway, I am unable to enter this proof to either of those ...at leas reading this would help you to help me ;) This needs creating some class, defining Collatz sequence next number, "follows" concept and "is followed by 1" concept; also it needs, possibly, a binary analysis of a number?

Thus, the following is what I want to formalize (and check):


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.

Tambet