We consider the system lambda2.

  Alphabet:

    fapp : [o * o] --> o 
    lam : [o] --> o 
    subst : [o * o] --> o 
    v : [] --> o 

  Rules:

    fapp(lam(x), y) => subst(x, y) 
    subst(v, x) => x 
    subst(lam(x), y) => lam(x) 
    subst(fapp(x, y), z) => fapp(subst(x, z), subst(y, z)) 

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 our external first-order non-termination checker: