We investigate three proof rules for proving termination of while programs and show their proof-theoretic equivalence. This involves a proof-theoretic analysis of various auxiliary proof rules in Hoare's logic. By discussing representations of proofs in the form of proof outlines, we reveal differences between these equivalent proof rules when used in practice. We also address applications in the context of the paradigm of design by contract.