We consider the system counterex1.

  Alphabet:

    f : [nat * nat] --> nat 
    g : [nat -> nat] --> nat 

  Rules:

    f(g(/\x.f(x, x)), g(/\y.f(y, y))) => (/\z.f(z, z)) g(/\u.f(u, u)) 

This AFS is converted to an AFSM simply by replacing all free variables by meta-variables (with arity 0).

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

  f(g(/\x.f(x, x)), g(/\y.f(y, y))) 
    => (/\x.f(x, x)) g(/\y.f(y, y)) 
    => f(g(/\x.f(x, x)), g(/\y.f(y, y))) 

That is, a term s reduces to a term t which instantiates s.