Target Equation info Equation to evaluate.
Format: t1 = t2.

Set of Equations / Term Rewriting System info Introduce either a Set of Equations:
(VAR ...)(EQUATIONS l1 = r1 ...)
Or a Term Rewriting System:
(VAR ...)(RULES l1 -> r1 ...)

Go!

Salvador Lucas and Julia Pagan.
Proving Equations with Nonterminating Term Rewriting Systems using Context-Sensitive Rewriting.
In Silvio Ghilardi and Cleo Pau, editors, Proceedings of the 40th International Workshop on Unification, UNIF 2026, Lisbon, Portugal, July 24 2026, to appear 2026.