  We introduce the $k$-variable-occurrence fragment, which is the set of terms
having at most $k$ occurrences of variables. We give a sufficient condition for
the decidability of the equational theory of the $k$-variable-occurrence
fragment using the finiteness of a monoid. As a case study, we prove that for
Tarski's calculus of relations with bounded dot-dagger alternation (an analogy
of quantifier alternation in first-order logic), the equational theory of the
$k$-variable-occurrence fragment is decidable for each $k$.
