  A proof tableau of Hoare logic is an annotated program with pre- and
post-conditions, which corresponds to an inference tree of Hoare logic. In this
paper, we show that a proof tableau for partial correctness can be transformed
into an inference sequence of rewriting induction for constrained rewriting. We
also show that the resulting sequence is a valid proof for an inductive theorem
corresponding to the Hoare triple if the constrained rewriting system obtained
from the program is terminating. Such a valid proof with termination of the
constrained rewriting system implies total correctness of the program w.r.t.
the Hoare triple. The transformation enables us to apply techniques for proving
termination of constrained rewriting to proving total correctness of programs
together with proof tableaux for partial correctness.
