For Simplify, I expect its a black, or at least gray box to Mathematica maintainers, too.

It will have simple rules such as constant folding, “replace x - x by zero”, “replace zero times something with the conditions under which ‘something’ has a value”, etc, lots of more complex but still easy to understand rules with conditionals such as “√x² = |x| if x is real”, and some weird logic that decides the order in which to try simplification rules.

There’s an analogy with compilers. In LLVM, most optimization passes are easy to understand, but if you look at the set of default optimization passes, there’s no clear reason for why it looks like it looks, other than “in our tests, that’s what performed best in a reasonable time frame”.

A lot of problems look like this. A while ago I was working on a calendar event optimization (think optimizing “every Monday from Jan 1, 2026 to March 10, 2026” + “every Monday from March 15, 2026 to March 31, 2026” to simply “every Monday from Jan 1, 2026 to March 31, 2026”). I wrote a number of intuitive and simple optimization passes as well as some unit tests. To my horror, some passes need to be repeated twice in different parts of the pipeline to get the tests to pass.

As a term-rewriting system the rule x-x=0 presumably won’t be in Simplify, it’ll be inside - (or Plus, actually). Instead I’d expect there to be strategies. Pick a strategy using a heuristic, push evaluation as far as it’ll go, pick a strategy, etc. But a lot of the work will be normal evaluation, not Simplify-specific.