  We prove two completeness results for Kleene algebra with tests and a top
element, with respect to guarded string languages and binary relations. While
the equational theories of those two classes of models coincide over the
signature of Kleene algebra, this is no longer the case when we consider an
additional constant ``top'' for the full element. Indeed, the full relation
satisfies more laws than the full language, and we show that those additional
laws can all be derived from a single additional axiom. We recover that the two
equational theories coincide if we slightly generalise the notion of relational
model, allowing sub-algebras of relations where top is a greatest element but
not necessarily the full relation. We use models of closed languages and
reductions in order to prove our completeness results, which are relative to
any axiomatisation of the algebra of regular events. For one of our
constructions, we extend the concept of finite monoid recognisability to
guarded-string languages; this device makes it possible to obtain a PSpace
algorithm for the equational theory of binary relations.
