Decidability of the universal theory of natural numbers with addition and divisibility

The class of all quantifier-free formulas constructed from atomic formulas of the form $(x+y=z)$, $(x=1)$, and $(x/y)$ is considered, where the predicate symbol “|” is interpreted as the divisibility relation on nonnegative integers. The decidability isproved of the set of all formulas of this form which are true for at least one choice of values for the variables. This result is equivalent to the decidability of the universal theory of natural numbers with addition and divisibility.