We consider the system lambda5.

  Alphabet:

    f : [d -> d * b] --> c 
    g : [b * a] --> d -> d 
    h : [a -> b -> c] --> b 
    i : [c] --> c 

  Rules:

    f(g(h(j), x), y) => i(j x y) 

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

This system is non-terminating, as demonstrated by the following reduction:

  f(g(h(/\x./\y.f(g(y, x), y)), z), h(/\u./\v.f(g(v, u), v))) 
    => i((/\x./\y.f(g(y, x), y)) z h(/\u./\v.f(g(v, u), v))) 
    =>_beta i(f(g(h(/\x./\y.f(g(y, x), y)), z), h(/\u./\v.f(g(v, u), v)))) 

That is, a term s reduces to a term of the form C[s].