On computational complexity of successor theory with unary transitive closure

The present article concerns the theory of the successor function with the unary transitive closure (TC) operator. This theory is equivalent to the TC-theory of discrete linear order with respect to TC-definability. We prove that any decision algorithm for this theory has at least hyperexponential computational complexity. The latter is much higher than the complexity of the same theories without the TC-operator.