Termination checks of mutually recursive functions

[fpoli]

@vakaras pointed out that the current encoding of mutually recursive functions might be unsound when the (optional) termination checks are enabled. Until that's fixes, it's up to the users to ensure that all pure function definitions always terminate.