A term rewrite system is a collection of directed equations that change an equation into a standard form.

The TRS for a very simple algebraic structure, a monoid, might look like this:

```(x*y)*z -> x*(y*z)
1*x -> x
x*1 ->
```

Here * does not necessarily mean multiplication. It could mean addition or some other odd operator, just as long as the operator follows the rules set down by a monoid.

By applying these three rules on any equation defined over this monoid, an equation can be both simplified and changed into a form that allows its structure and order to be compared to another equation for use in a symbolic computation system.

Example: the equation `((x*1)*(1*y))*(z*1)` can be changed around like so:

```((x*1)*(1*y))*(z*1) -> (x*(1*y))*(z*1) -> (x*y*(z*1) -> (x*y)*z -> x*(y*z) ```

A set of term rewrite rules is said to be terminating if any sequence of term rewrites results in an equation that cannot be changed after a finite number of steps.

If the final equation produced is unique, then that equation is called the normal form of any equation in the term rewrite steps that precede it.

Some of this information comes from "Logic for Mathematics and Computer Science" by Stanley N. Burris.