We consider the system 723.

  Alphabet:

    a : [] --> o 
    f : [o * o] --> o 
    mu : [o -> o] --> o 
    s : [o] --> o 

  Rules:

    f(X, X) => a 
    s(X) => f(X, s(X)) 
    mu(/\x.X(x)) => X(mu(/\y.X(y))) 

It is easy to see that this system is non-terminating:

  s(x) 
    => f(x, s(x)) 
    |> s(x) 

That is, a term s reduces to a term t which has a subterm that is an instance of the original term.