# Provably correct algorithm/CAS for checking term equalities

Within my research of term rewriting systems (TRS) I stumbled upon a paper (Siekmann, J., and P. Szabó. “The Undecidability of the DA-Unification Problem.” The Journal of Symbolic Logic, vol. 54, no. 2, 1989, pp. 402–414. JSTOR, JSTOR, www.jstor.org/stable/2274856.) that stated the following:

We show that the DA-unification problem is undecidable. That is, given two binary function symbols $+$ and $*$, variables and constants, it is undecidable if two terms built from these symbols can be unified provided the following DA-axioms hold: $(x + y) * z = (x * z) + (y * z),\\ x * (y + z) = (x * y) + (x * z),\\ x + (y + z) = (x + y) + z \\$
Two terms are DA-unifiable (i.e. an equation is solvable in DA) if there exist terms to be substituted for their variables such that the resulting terms are equal in the equational theory DA.
This is the smallest currently known axiomatic subset of Hilbert's tenth problem for which an undecidability result has been obtained.
[...] Hilbert's tenth problem presented to the International Congress of Mathematicians in his 1900 speech in Paris poses the question, if it is decidable whether a given polynomial equation is solvable in positive integers; a problem that was finally shown to be undecidable.

My resulting question is: Does this prove that there cannot be an algorithm / computer algebra system that, even for very restricted sets like $\mathbb{Q}$ with operators $+, -, *, /$, is provably correct when it comes to checking term equalities (for example), when distributivity and associativity hold?

The Wolfram documentation states that

[t]here is a basic result in the mathematical theory of computation which shows that this [ reduce all expressions to some standard form] is, in fact, not always possible.

which would be needed for such a system.

I found the Richardson theorem which basically states that there may not exist an algorithm that decides if two expressions representing numbers are semantically equal, if exponentials and logarithms are allowed in the expressions.

This still does not answer my question for a set without such expressions, although it hints that this should be possible.