Esse laço sempre termina?

Escolha um inteiro positivo n e execute:

• Se n for par, divida-o por 2.
• Se n for ímpar, substitua-o por 3*n + 1.
• Repita até chegar a 1.

Para n = 6:

6 → 3 → 10 → 5 → 16 → 8 → 4 → 2 → 1

Uma implementação em Python:

def transformar(n):
    while n != 1:
        n = n // 2 if n % 2 == 0 else 3 * n + 1
    return n

Desafio: prove que essa função termina para todo inteiro positivo ou encontre um valor para o qual ela nunca termine. Testar muitos valores não demonstra a conjectura. E uma execução demorada, por si só, não constitui um contraexemplo.