In this example

Neg(x) -> <: Minus(Zero(), x) >;

In general both sides are terms with variables, where all variables of the
right-hand side also appear on the left-hand side.
Actually, the left-hand side can be the same kind of pattern that is allowed in
function definitions.
To allow `greater control' (a euphemism for hacking...) we allow
arbitrary C functions and string- and int-denotations in the right-hand side (see below).
For the collection of rewrite rules, the system generates a function
*rewrite_**phylum*
for each phylum, which has the normalised form as its result.
This function can be called in the same way as any other function.

The rewrite functions have an additional argument of type *rview*.
Rewrite views can be used to group rewrite rules in separate rewrite systems.
Rewrite rules can be made specific for a set of rewrite
*views*
(or, added to one or more rewrite systems) by naming
these views between the angle open bracket and the colon of a rewrite rule.
For example:

An omitted view list defaults to all rewrite views. If no views are specified, the angle brackets and colon may be omitted (as we usually do), as we show below for the rewrite rule for

Neg(x) -> < view1 view2: Minus(Zero(), x) >;

This is equivalent to a view list that only contains the view name

Neg(x) -> Minus(Zero(), x);

Rewrite views can be declared as in the following example:

Rewrite views should be declared. If the termprocessor input contains one or more rewrite view declarations it will report errors for all rewrite views that are used and not declared. The use of view declarations may help to find typing errors in view names - in term processor input that does not contain view declarations, the misspelling of a view name may just introduce a new view (with the misspelled name).

%rview view1 view2;/* the `%' is part of the keyword */

If several rewrite rules share the same left-hand side, they may be combined by grouping the right-hand sides (with seperating commas), provided that all the angle brackets haven't been omitted from the right-hand sides. If several rewrite rules share the same right-hand side, they may be combined by grouping the left-hand sides (with seperating commas). The general form of a rewrite rule is shown below:

pattern1, pattern2, ... -> < v1 v2 ... : ... >, ..., < vn ... : ... > ;

How we can prove that a rewrite system always yields a normal form
is beyond the scope of this
manual, but informally stated, each rule should bring the term `closer' to
its normal form, and the order in which the rules are
applied (the *rewrite strategy*) should not matter.
Two simple warnings: never ever use a rule in which the right-hand side
is equal to the left-hand side, or a rule that directly expresses a
commutative property.

The default rewrite strategy is leftmost innermost.
In the case of overlapping patterns , where more than one left-hand side matches,
the *most* specific match is taken.

Rewrite rules with functional right-hand sides are a bit harder to prove correct.
The first requirement of course is that the arguments and the results
of those functions should have the correct types,
which *lint* can check.
The second requirement is that the rule is meaningful,
but that is hard to check automatically.
The writer of such rules should convince herself of the correctness
of the rewrite rules.
Here we give some considerations that can be used in doing so.
The `purpose' of a rewrite system is to convert a term to its
*normal form*.
Now let us look closer at a rule with a function in it:

The rewrite system uses this rule when it has a subterm that matches the left-hand side, and `assumes' that substituting it by the right-hand side brings it closer to the normal form. It then continues applying rules on the new term. The function

Operator(x) -> Function(x);