Upper bounds on the height of terms in the solution of the semiunification problem

In this paper we investigate on one decidable case of term semiunification problem, namely when all the functional symbols in the given terms have arity one, except, possibly, for outer symbols of terms, which have no restrictions. We propose an algorithm that builds a most general solution of the semiunification problem, and prove an upper bound on the height of this solution; the upper bound is linear by the height of terms in the given problem. Our method is to reduce the problem for terms to a special system of equations in free semigroups, and then to solve this system.