That's not enough. You also have to constrain what the mapped function is doing. For example, it could create one or more brand new arrays or for that matter pe

That's not enough. You also have to constrain what the mapped function is doing. For example, it could create one or more brand new arrays or for that matter perform any infinite computation without mutating the original array. Proving that the mapped function does not do any of that requires that it not be Turing Complete.