Preserving termination when rewriting recursive programs
The standard presentation of program transformation ideas is unsound, quite unfortunately.  They usually think of program transformation as forward deduction.  Using equational reasoning, you can deduce new facts from the old program, and lo and behold, it gives a better program!  While the new facts are quite clearly facts, nothing guarantees that they constitute a program.  The problem you have spotted is this naive presentation of the program transformation ideas.

However, it is possible to think of very much the same process as a backward deduction.  We think of the old program as a specification, and derive a new program that satisfies the specification.  Since equational reasoning is often bidirectional, you would see very similar steps in deriving the new program.  However, the meaning of these steps is opposite to what the naive methods imply.  When you use this "correct" method, you reason about termination while introducing recursion, and always derive a correct program.

For a paper describing the technique, see Deductive and inductive synthesis of equational programs (PDF).  This was done for first-order "equational" programs, but very similar ideas should be applicable to terminating functional programs.  If you are interested in non-terminating programs, I think you could use coinduction techniques (an off-the-cuff intuition).  However, my efforts to apply domain theory techniques to do these kinds of transformations did not bear fruit.  It might still be possible, but I haven't seen anything written on it.