  TopKAT is the algebraic theory of Kleene algebra with tests (KAT) extended
with a top element. Compared to KAT, one pleasant feature of TopKAT is that, in
relational models, the top element allows us to express the domain and codomain
of a relation. This enables several applications in program logics, such as
proving under-approximate specifications or reachability properties of
imperative programs. However, while TopKAT inherits many pleasant features of
KATs, such as having a decidable equational theory, it is incomplete with
respect to relational models. In other words, there are properties that hold
true of all relational TopKATs but cannot be proved with the axioms of TopKAT.
This issue is potentially worrisome for program-logic applications, in which
relational models play a key role.
  In this paper, we further investigate the completeness properties of TopKAT
with respect to relational models. We show that TopKAT is complete with respect
to (co)domain comparison of KAT terms, but incomplete when comparing the
(co)domain of arbitrary TopKAT terms. Since the encoding of under-approximate
specifications in TopKAT hinges on this type of formula, the aforementioned
incompleteness results have a limited impact when using TopKAT to reason about
such specifications.
