A complete, terminating set of rules for term rewriting on linear equations

Question

Recently I have done some research on term rewriting.
I feel not very experienced yet and hence there might be an easy answer to this questions, but I was curious if there is a ruleset for a term rewriting system for linear equations that provide commutativity, associativity and distributivity as well as completeness and termination.

I found some 'tricks' that use the system 'modulo' commutativity for example, but since 'linear equations' is such a specification, I find there has to be a finite ruleset to cover this.
On the other hand I found rulesets for Groups (hence with only one operator), but that is not sufficient in my case.
In the TeReSe paper I found that

A term can be represented as a finite labeled, non-commutative tree according to the following inductive definition:

1. A variable or a constant is represented by the tree consisting of one single node, labelled by the variable or constant itself.
2. The term $F(t_1,\dots,t_n)$ is represented by the tree of which the root node has as its label the symbol $F$, and which has as its immediate subtrees, in order from left to right, the trees representing $t_1,\dots,t_n$.'
   

So using this tree representation I came up with the idea of evaluating subtrees as sets. By that I mean rules like

1. If $symb(t) = A:$
   1.1 if $\exists x \in graph(t): symb(x)=A$ then $graph(t) \rightarrow graph(t) \backslash \{x \in graph(t)|symb(x)=A\} \cup \{y \in graph(x)| x \in graph(t) \wedge symb(x)=A\}$
   1.2 if $\forall x \in graph(t)~ \exists (-x) \in graph(t)$ then $ graph(t) \rightarrow 0$
   1.3 if $\exists x \in graph(t): \exists (-x) \in graph(t)$ then $graph(t) \rightarrow t\backslash \{x|(-x) \in graph(t)\}$
   1.4 if $\exists 0 \in graph(t)$ then $graph(t) \rightarrow graph(t) \backslash \{0\}$
2. If $symb(t) = M:$
   2.1 if $\exists x \in graph(t): symb(x)=M$ then $graph(t) \rightarrow graph(t) \backslash \{x \in graph(t)|symb(x)=M\} \cup \{y \in graph(x)| x \in graph(t) \wedge symb(x)=M\}$
   2.2 if $\forall x \in graph(t)~ \exists x^{-1} \in graph(t)$ then $graph(t) \rightarrow 1$
   2.3 if $\exists x \in graph(t): \exists x^{-1} \in graph(t)$ then $t \rightarrow graph(t)\backslash \{x|x^{-1} \in graph(t)\}$
   2.4 if $\exists 1 \in graph(t)$ then $graph(t) \rightarrow graph(t) \backslash \{1\}$
   2.5 if $\exists 0 \in graph(t)$ then $graph(t) \rightarrow 0$
   
3. if $\exists !x \in graph(t)$ then $t \rightarrow \{x | x \in graph(t) \}$
4. If $symb(t) = A $ then if $\exists x : symb(x) = M \wedge t \in graph(x) $ then $graph(t) \rightarrow \{y \rightarrow y~ \cup x\backslash t ~(symb(y) \rightarrow M)|y \in t \}; x \rightarrow t$

where $symb(t)$ is the symbol of $t$, $A$ is the addition, $M$ is multiplikation and with $\in$ meaning is subtree of .
Note that the rules need to be processed in order, since 1.3 and 2.3 need a check of the previous rule to not get completely removed.
Together with the distributive law, in my opinion, this should solve my problem. My ruleset is not yet complete, but I am working on it.
Actually, the distributive law seems to become my major problem here.
I tried an approach for a rule, but notation becomes very unclear here.

My resulting question is the following: Is there an existing ruleset for linear (or even more complex) equations that satisfy my requirements? If not, what else do I need to complete my provided ruleset? Since I am starting to get confused with my own notation I would also be glad for improvement advice on that matter.

Note 1: In the TeReSe paper I found

'[...] the specification $E$ consisting of a single binary commutative operator $+$ and a constant $0$, and a single equation $x + y = y + x$. [...] no complete TRS $R$ can be found for $E$.'

Does that mean that there can never be a complete TRS when commutativity holds?

Note 2: Theorem 10.5 in the not freely published paper (G.E. Peterson and M.E. Stickel, Complete sets of reductions for some equational theories, Journal of the ACM, 28, 2, p.233-264, 1981.) might have the answer for me, but I just don't understand it. For completeness I will cite it here, although it might be not very helpful for you due to various missing definitions:

Theorem 10.5. Let $T$ be an $A,C$ (meaning associative and commutative) theory and $R$ a set of reductions. Then $R^e_T$ is $T$-compatible.

If desired I can provide some of the previous definitions.

Answer 1

I think I can now provide an answer to the biggest part of my question: Is there a ruleset for a TRS with the specified requirements?

For this I will cite an again not openly published 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.):

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.

To my understanding this directly proves that there cannot be defined reductions that guarantee that arbirtarily represented, mathematically equal terms are reduced into the exact same term, hence not every ("logical") occurrence of $x + (-x)$ can be found and eliminated.

In the future I will likely work again on my ruleset mentioned above, since I realized that it doesn't fulfill the requirements of term rewriting rules anyway, but might be interesting to investigate nevertheless.