You can't encode the Collatz Conjecture (in that way) in Morte. It would require an infinite amount of computation and infinite loops have been disallowed. You would have to get a little bit more creative with the dependently typed parts of CIC and then finding a program which matches the needed type is as of today an unsolved task.