Total Correctness by Local Improvement in Program Transformation