We consider the system h21.

  Alphabet:

    0 : [] --> A 
    01 : [] --> A 
    activate : [] --> A -> A 
    app : [] --> (A -> A) -> A -> A 
    cons : [] --> A -> A -> A 
    cons1 : [] --> A -> A -> A 
    fcons : [] --> A -> A -> A 
    first : [] --> A -> A -> A 
    first1 : [] --> A -> A -> A 
    from : [] --> A -> A 
    map : [] --> (A -> A) -> A -> A 
    nil : [] --> A 
    nil1 : [] --> A 
    nxx0 : [] --> A 
    nxxcons : [] --> A -> A -> A 
    nxxfirst : [] --> A -> A -> A 
    nxxfrom : [] --> A -> A 
    nxxnil : [] --> A 
    nxxs : [] --> A -> A 
    nxxsel : [] --> A -> A -> A 
    quote : [] --> A -> A 
    quote1 : [] --> A -> A 
    s : [] --> A -> A 
    s1 : [] --> A -> A 
    sel : [] --> A -> A -> A 
    sel1 : [] --> A -> A -> A 
    unquote : [] --> A -> A 
    unquote1 : [] --> A -> A 

  Rules:

    sel (s x) (cons y z) => sel x (activate z) 
    sel 0 (cons x y) => x 
    first 0 x => nil 
    first (s x) (cons y z) => cons y (nxxfirst x (activate z)) 
    from x => cons x (nxxfrom (nxxs x)) 
    sel1 (s x) (cons y z) => sel1 x (activate z) 
    sel1 0 (cons x y) => quote x 
    first1 0 x => nil1 
    first1 (s x) (cons y z) => cons1 (quote y) (first1 x (activate z)) 
    quote nxx0 => 01 
    quote1 (nxxcons x y) => cons1 (quote (activate x)) (quote1 (activate y)) 
    quote1 nxxnil => nil1 
    quote (nxxs x) => s1 (quote (activate x)) 
    quote (nxxsel x y) => sel1 (activate x) (activate y) 
    quote1 (nxxfirst x y) => first1 (activate x) (activate y) 
    unquote 01 => 0 
    unquote (s1 x) => s (unquote x) 
    unquote1 nil1 => nil 
    unquote1 (cons1 x y) => fcons (unquote x) (unquote1 y) 
    fcons x y => cons x y 
    first x y => nxxfirst x y 
    from x => nxxfrom x 
    s x => nxxs x 
    0 => nxx0 
    cons x y => nxxcons x y 
    nil => nxxnil 
    sel x y => nxxsel x y 
    activate (nxxfirst x y) => first (activate x) (activate y) 
    activate (nxxfrom x) => from (activate x) 
    activate (nxxs x) => s (activate x) 
    activate nxx0 => 0 
    activate (nxxcons x y) => cons (activate x) y 
    activate nxxnil => nil 
    activate (nxxsel x y) => sel (activate x) (activate y) 
    activate x => x 
    map (/\x.f x) nil => nil 
    app (/\x.f x) y => f y 

Using the transformations described in [Kop11], this system can be brought in a form without leading free variables in the left-hand side, and where the left-hand side of a variable is always a functional term or application headed by a functional term.

We now transform the resulting AFS into an AFSM by replacing all free variables by meta-variables (with arity 0).  This leads to the following AFSM:

  Alphabet:

    0 : [] --> A 
    01 : [] --> A 
    activate : [A] --> A 
    app : [A -> A * A] --> A 
    cons : [A * A] --> A 
    cons1 : [A * A] --> A 
    fcons : [A * A] --> A 
    first : [A * A] --> A 
    first1 : [A * A] --> A 
    from : [A] --> A 
    map : [A -> A * A] --> A 
    nil : [] --> A 
    nil1 : [] --> A 
    nxx0 : [] --> A 
    nxxcons : [A * A] --> A 
    nxxfirst : [A * A] --> A 
    nxxfrom : [A] --> A 
    nxxnil : [] --> A 
    nxxs : [A] --> A 
    nxxsel : [A * A] --> A 
    quote : [A] --> A 
    quote1 : [A] --> A 
    s : [A] --> A 
    s1 : [A] --> A 
    sel : [A * A] --> A 
    sel1 : [A * A] --> A 
    unquote : [A] --> A 
    unquote1 : [A] --> A 
    ~AP1 : [A -> A * A] --> A 

  Rules:

    sel(s(X), cons(Y, Z)) => sel(X, activate(Z)) 
    sel(0, cons(X, Y)) => X 
    first(0, X) => nil 
    first(s(X), cons(Y, Z)) => cons(Y, nxxfirst(X, activate(Z))) 
    from(X) => cons(X, nxxfrom(nxxs(X))) 
    sel1(s(X), cons(Y, Z)) => sel1(X, activate(Z)) 
    sel1(0, cons(X, Y)) => quote(X) 
    first1(0, X) => nil1 
    first1(s(X), cons(Y, Z)) => cons1(quote(Y), first1(X, activate(Z))) 
    quote(nxx0) => 01 
    quote1(nxxcons(X, Y)) => cons1(quote(activate(X)), quote1(activate(Y))) 
    quote1(nxxnil) => nil1 
    quote(nxxs(X)) => s1(quote(activate(X))) 
    quote(nxxsel(X, Y)) => sel1(activate(X), activate(Y)) 
    quote1(nxxfirst(X, Y)) => first1(activate(X), activate(Y)) 
    unquote(01) => 0 
    unquote(s1(X)) => s(unquote(X)) 
    unquote1(nil1) => nil 
    unquote1(cons1(X, Y)) => fcons(unquote(X), unquote1(Y)) 
    fcons(X, Y) => cons(X, Y) 
    first(X, Y) => nxxfirst(X, Y) 
    from(X) => nxxfrom(X) 
    s(X) => nxxs(X) 
    0 => nxx0 
    cons(X, Y) => nxxcons(X, Y) 
    nil => nxxnil 
    sel(X, Y) => nxxsel(X, Y) 
    activate(nxxfirst(X, Y)) => first(activate(X), activate(Y)) 
    activate(nxxfrom(X)) => from(activate(X)) 
    activate(nxxs(X)) => s(activate(X)) 
    activate(nxx0) => 0 
    activate(nxxcons(X, Y)) => cons(activate(X), Y) 
    activate(nxxnil) => nil 
    activate(nxxsel(X, Y)) => sel(activate(X), activate(Y)) 
    activate(X) => X 
    map(/\x.~AP1(F, x), nil) => nil 
    app(/\x.~AP1(F, x), X) => ~AP1(F, X) 
    map(/\x.activate(x), nil) => nil 
    map(/\x.app(F, x), nil) => nil 
    map(/\x.cons(X, x), nil) => nil 
    map(/\x.cons1(X, x), nil) => nil 
    map(/\x.fcons(X, x), nil) => nil 
    map(/\x.first(X, x), nil) => nil 
    map(/\x.first1(X, x), nil) => nil 
    map(/\x.from(x), nil) => nil 
    map(/\x.map(F, x), nil) => nil 
    map(/\x.nxxcons(X, x), nil) => nil 
    map(/\x.nxxfirst(X, x), nil) => nil 
    map(/\x.nxxfrom(x), nil) => nil 
    map(/\x.nxxs(x), nil) => nil 
    map(/\x.nxxsel(X, x), nil) => nil 
    map(/\x.quote(x), nil) => nil 
    map(/\x.quote1(x), nil) => nil 
    map(/\x.s(x), nil) => nil 
    map(/\x.s1(x), nil) => nil 
    map(/\x.sel(X, x), nil) => nil 
    map(/\x.sel1(X, x), nil) => nil 
    map(/\x.unquote(x), nil) => nil 
    map(/\x.unquote1(x), nil) => nil 
    app(/\x.activate(x), X) => activate(X) 
    app(/\x.app(F, x), X) => app(F, X) 
    app(/\x.cons(X, x), Y) => cons(X, Y) 
    app(/\x.cons1(X, x), Y) => cons1(X, Y) 
    app(/\x.fcons(X, x), Y) => fcons(X, Y) 
    app(/\x.first(X, x), Y) => first(X, Y) 
    app(/\x.first1(X, x), Y) => first1(X, Y) 
    app(/\x.from(x), X) => from(X) 
    app(/\x.map(F, x), X) => map(F, X) 
    app(/\x.nxxcons(X, x), Y) => nxxcons(X, Y) 
    app(/\x.nxxfirst(X, x), Y) => nxxfirst(X, Y) 
    app(/\x.nxxfrom(x), X) => nxxfrom(X) 
    app(/\x.nxxs(x), X) => nxxs(X) 
    app(/\x.nxxsel(X, x), Y) => nxxsel(X, Y) 
    app(/\x.quote(x), X) => quote(X) 
    app(/\x.quote1(x), X) => quote1(X) 
    app(/\x.s(x), X) => s(X) 
    app(/\x.s1(x), X) => s1(X) 
    app(/\x.sel(X, x), Y) => sel(X, Y) 
    app(/\x.sel1(X, x), Y) => sel1(X, Y) 
    app(/\x.unquote(x), X) => unquote(X) 
    app(/\x.unquote1(x), X) => unquote1(X) 
    ~AP1(F, X) => F X 

Symbol ~AP1 is an encoding for application that is only used in innocuous ways.  We can simplify the program (without losing non-termination) by removing it.  Additionally, we can remove some (now-)redundant rules.  This gives:

  Alphabet:

    0 : [] --> A 
    01 : [] --> A 
    activate : [A] --> A 
    app : [A -> A * A] --> A 
    cons : [A * A] --> A 
    cons1 : [A * A] --> A 
    fcons : [A * A] --> A 
    first : [A * A] --> A 
    first1 : [A * A] --> A 
    from : [A] --> A 
    map : [A -> A * A] --> A 
    nil : [] --> A 
    nil1 : [] --> A 
    nxx0 : [] --> A 
    nxxcons : [A * A] --> A 
    nxxfirst : [A * A] --> A 
    nxxfrom : [A] --> A 
    nxxnil : [] --> A 
    nxxs : [A] --> A 
    nxxsel : [A * A] --> A 
    quote : [A] --> A 
    quote1 : [A] --> A 
    s : [A] --> A 
    s1 : [A] --> A 
    sel : [A * A] --> A 
    sel1 : [A * A] --> A 
    unquote : [A] --> A 
    unquote1 : [A] --> A 

  Rules:

    sel(s(X), cons(Y, Z)) => sel(X, activate(Z)) 
    sel(0, cons(X, Y)) => X 
    first(0, X) => nil 
    first(s(X), cons(Y, Z)) => cons(Y, nxxfirst(X, activate(Z))) 
    from(X) => cons(X, nxxfrom(nxxs(X))) 
    sel1(s(X), cons(Y, Z)) => sel1(X, activate(Z)) 
    sel1(0, cons(X, Y)) => quote(X) 
    first1(0, X) => nil1 
    first1(s(X), cons(Y, Z)) => cons1(quote(Y), first1(X, activate(Z))) 
    quote(nxx0) => 01 
    quote1(nxxcons(X, Y)) => cons1(quote(activate(X)), quote1(activate(Y))) 
    quote1(nxxnil) => nil1 
    quote(nxxs(X)) => s1(quote(activate(X))) 
    quote(nxxsel(X, Y)) => sel1(activate(X), activate(Y)) 
    quote1(nxxfirst(X, Y)) => first1(activate(X), activate(Y)) 
    unquote(01) => 0 
    unquote(s1(X)) => s(unquote(X)) 
    unquote1(nil1) => nil 
    unquote1(cons1(X, Y)) => fcons(unquote(X), unquote1(Y)) 
    fcons(X, Y) => cons(X, Y) 
    first(X, Y) => nxxfirst(X, Y) 
    from(X) => nxxfrom(X) 
    s(X) => nxxs(X) 
    0 => nxx0 
    cons(X, Y) => nxxcons(X, Y) 
    nil => nxxnil 
    sel(X, Y) => nxxsel(X, Y) 
    activate(nxxfirst(X, Y)) => first(activate(X), activate(Y)) 
    activate(nxxfrom(X)) => from(activate(X)) 
    activate(nxxs(X)) => s(activate(X)) 
    activate(nxx0) => 0 
    activate(nxxcons(X, Y)) => cons(activate(X), Y) 
    activate(nxxnil) => nil 
    activate(nxxsel(X, Y)) => sel(activate(X), activate(Y)) 
    activate(X) => X 
    map(/\x.X(x), nil) => nil 
    app(/\x.X(x), Y) => X(Y) 

This system is non-terminating, as demonstrated by nattprover:


+++ Citations +++

[Kop11]  C. Kop.  Simplifying Algebraic Functional Systems.  In Proceedings of CAI 2011, volume 6742 of LNCS.  201--215, Springer, 2011.