The “equal last letter” predicate for words on infinite alphabets and classes of multitape automata

We consider the first-order theory of the free infinitely generated monoid with the usual predicates “prefix” and “equal length” along with the predicate “equal last letter”. The associated definable relations are related to the algebras of relations recognized by different types of multitape automata which are natural extensions of the famous Rabin–Scott multitape automata and the synchronous automata. We investigate these classes of automata and solve decision issues concerning them.