Solving inequations in terms algebras

Let T be the theory of term algebra over the relational symbols = or ⩾, where ⩾ is interpreted as a lexicographic path ordering. The decidability of the purely existential fragment of T is shown. The proof is carried out in three steps. The first step consists of the transformation of any quantifier-free formula φ (i.e. all variables are free) into a solved form that has the same set of solutions as φ. Then the author shows how to decide the satisfiability of some particular problems called simple systems. A simple system is a formula which defines a total ordering on the terms occurring in it and which is closed under deduction. This last property means that if ψ is a solved form of a simple system φ then ψ must be a subformula of φ. The proof is completed by showing how to reduce the satisfiability of an arbitrary solved form to the satisfiability of finitely many simple systems