And when does the rewriting process stop? Well, the process stops just when there are no longer redexes in a term. So, we keep rewriting redexes as far as redexes are present in a term. When we find a term that has no redexes, then we stop and we call that term a normal form. Many kinds of computations are possible in this apparently so simple a system. There are finite computations, for instance in this first example. There are two redexes here, the inner and the outer one. And we may reduce them, for instance in this order, getting the string zz, which is a normal form because there is no more lx. applied to something. But there are also infinite reductions. For instance, in this case, the term lx.x.x applied to itself keeps reducing to itself. And so this is an infinite reduction sequence. And there are even more complicated reduction sequences like this second example shows.

---