We consider the system 462.

  Alphabet:

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

  Rules:

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

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

  mu(/\x.g x) 
    => g mu(/\x.g x) 
    |> mu(/\y.g y) 

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