A general translation rule from recursive procedures to iterative ones is augmented by also translating the correctness proof.The augmented translation rule is defined within the framework of Pascal programs, with the correctness proof expressed in the Hoare style.The translation is consistent with the stepwise development of Pascal programs.Moreover the translation can be done automatically provided that the assertions are expressed in a formal specification language.Given are a few simplification rules, whose applicability, after the translation, is easily detectable and strongly suggested by the translated assertions.It is shown that the particular cases of linear, tail, and simple recursion (which are known to be easily handled and simplified when expressed in a schematic functional notation) can be simplified automatically after the translation step without leaving the Pascal language.Two examples are provided to show that the given simplification rules can also effectively apply to more general recursive procedures.