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

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.