  In relational verification, judicious alignment of computational steps
facilitates proof of relations between programs using simple relational
assertions. Relational Hoare logics (RHL) provide compositional rules that
embody various alignments of executions. Seemingly more flexible alignments can
be expressed in terms of product automata based on program transition
relations. A single degenerate alignment rule (self-composition), atop a
complete Hoare logic, comprises a RHL for $\forall\forall$ properties that is
complete in the ordinary logical sense (Cook'78). The notion of alignment
completeness was previously proposed as a more satisfactory measure, and some
rules were shown to be alignment complete with respect to a few ad hoc forms of
alignment automata. This paper proves alignment completeness with respect to a
general class of $\forall\forall$ alignment automata, for a RHL comprised of
standard rules together with a rule of semantics-preserving rewrites based on
Kleene algebra with tests. A new logic for $\forall\exists$ properties is
introduced and shown to be alignment complete. The $\forall\forall$ and
$\forall\exists$ automata are shown to be semantically complete. Thus the
logics are both complete in the ordinary sense. Recent work by D'Osualdo et al
highlights the importance of completeness relative to assumptions (which we
term entailment completeness), and presents $\forall\forall$ examples seemingly
beyond the scope of RHLs. Additional rules enable these examples to be proved
in our RHL, shedding light on the open problem of entailment completeness.
