# Reduce

CafeOBJ supports reduction of terms. An input term is reduced by applying equations where each equation is regarded as a left-to-right rewrite rule. A term which no equation can be applied to is called a normal form.

The `red` command reduces a term.

`red `<term>` .`

Example:

Let us reduce Term `s(s(0)) + s(s(s(0)))` in Module `NAT+`.

First, select Module `NAT+`.

```CafeOBJ> select NAT+
NAT+> ```

Then, reduce Term `s(s(0)) + s(s(s(0)))` by the `red` command:

```NAT+> red s(s(0)) + s(s(s(0))) .
-- reduce in NAT+ : s(s(0)) + s(s(s(0)))
s(s(s(s(s(0))))) : Nat
(0.000 sec for parse, 3 rewrites(0.010 sec), 5 matches)
NAT+> ```

In the above, the `red` command reduced Term `s(s(0)) + s(s(s(0)))` into its normal form `s(s(s(s(s(0)))))`. Reduction guarantees that the input term is equivalent with the output term in the specification. So, the above example is a proof of 2 + 3 = 5.

## Trace

To show a trace of reduction, set the `trace` switch on as follows.

```NAT+> set trace on
NAT+> red s(s(0)) + s(s(s(0))) .
-- reduce in NAT+ : s(s(0)) + s(s(s(0)))
1>[1] rule: eq s(N:Nat) + M:Nat = s(N + M)
{ N:Nat |-> s(0), M:Nat |-> s(s(s(0))) }
1<[1] s(s(0)) + s(s(s(0))) --> s(s(0) + s(s(s(0))))
1>[2] rule: eq s(N:Nat) + M:Nat = s(N + M)
{ N:Nat |-> 0, M:Nat |-> s(s(s(0))) }
1<[2] s(0) + s(s(s(0))) --> s(0 + s(s(s(0))))
1>[3] rule: eq 0 + M:Nat = M
{ M:Nat |-> s(s(s(0))) }
1<[3] 0 + s(s(s(0))) --> s(s(s(0)))
s(s(s(s(s(0))))) : Nat
(0.000 sec for parse, 3 rewrites(0.020 sec), 5 matches)
NAT+> ```

There is another trace mode: the `trace whole` switch:

```NAT+> set trace whole on
NAT+> red s(s(0)) + s(s(s(0))) .
-- reduce in NAT+ : s(s(0)) + s(s(s(0)))
[1]: s(s(0)) + s(s(s(0)))
---> s(s(0) + s(s(s(0))))
[2]: s(s(0) + s(s(s(0))))
---> s(s(0 + s(s(s(0)))))
[3]: s(s(0 + s(s(s(0)))))
---> s(s(s(s(s(0)))))
s(s(s(s(s(0))))) : Nat
(0.000 sec for parse, 3 rewrites(0.020 sec), 5 matches)
NAT+> ```

In this mode, only the whole terms in the trace are shown simply.