The total correctness of programs with mutually recursive procedures is significantly more complex than their partial correctness. Past methods of proving termination have suffered from being rigid, not general, non-intuitive, and ad hoc in structure, not suitable for mechanization. We have devised a new method for proving termination and mechanized it within an automatic tool called a Verification Condition Generator. This tool analyzes not only the program's syntax but also, uniquely, its procedure call graph, to produce verification conditions sufficient to ensure the program's total correctness. Diversion verification conditions reduce the labor involved in proving termination from infinite to finite. The VCG tool has itself been deeply embedded and proven sound within the HOL theorem prover with respect to the underlying structural operational semantics. Now proofs of total correctness of individual programs may be significantly automated with complete security.