- predefined variables:
- expression to be evaluated:

- expression rewritten replacing , a fixed point of , by
:

- expression rewritten using rule 12:

- expression rewritten substituting the 1st occurrence of ::

- performing -reduction by substituting variable in the
body of the lambda abstraction by the
argument
:

- performing -reduction by substituting variable in the
body of the lambda abstraction by the
argument
:

- evaluating the `IF'-expression by selecting the `no'-branch
and evaluating the subtraction:

- expression rewritten substituting by
using rule 12:

- expression rewritten substituting the first occurrence of
the variable by its value:

- performing -reduction substituting `fac' in the body
of the lambda abstraction by the argument :

- performing -reduction substituting in the body
of the lambda abstraction by the argument
:

- evaluating `IF'-expression returning the `yes'-branch:

- evaluating the multiplication: