Our results: Firstly, in Section , we compare the relative expressive power of the different theories. On the one hand, we manage to group certain families together, where they express the same class of languages. In the technical Lemma , we show that adding linear arithmetic over string-lengths to a theory allowing only language membership predicates for a class of languages with good language theoretic properties does not alter its expressive power. Thus, the theories in which only regular language (or visibly pushdown language) membership predicates are allowed and the theories in which length comparison is added to those membership predicates are equivalent. While in the case of theories based on regular language membership predicates we can also add concatenation without changing the expressive power, we show in Theorem  that adding this operation to theories based on visibly pushdown language membership predicates strictly increases their expressive power, as they can express all recursively enumerable languages. Moreover, we also provide several separation results between the classes of language expressed by various theories. One of the ways we achieve this is by non-trivially extending pumping-lemma style tools for word equations from [1]} to our more general settings. The overall hierarchy of classes of languages expressible in our theories is depicted in Figure REF .
