Due to fundamental theoretical limitations, Tamarin cannot handle arbitrary equational theories. In this chapter, we explain the conditions that must be met by equational theories such that Tamarin can reason with them. The conditions go beyond mere syntactic ones and are nontrivial to check. But for simplicity, we start with a syntactically defined class of equational theories that tamarin can handle. We first define the notion of subterm-convergence: An equation is subterm-convergent when its right-hand side is either a strict subterm of its left-hand side or alternatively a constant. We call an equational theory subterm-convergent when all of its individual equations have this property, and the theory itself is convergent. To ensure convergence (meaning confluence and termination), first confluence must be checked.