We consider the system AotoYamada_05__022.

  Alphabet:

    cons : [b * c] --> c 
    leaf : [a] --> b 
    mapt : [a -> a * b] --> b 
    maptlist : [a -> a * c] --> c 
    nil : [] --> c 
    node : [c] --> b 

  Rules:

    mapt(f, leaf(x)) => leaf(f x) 
    mapt(f, node(x)) => node(maptlist(f, x)) 
    maptlist(f, nil) => nil 
    maptlist(f, cons(x, y)) => cons(mapt(f, x), maptlist(f, y)) 

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

We use rule removal, following [Kop12, Theorem 2.23].

This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]):

  mapt(F, leaf(X)) >? leaf(F X) 
  mapt(F, node(X)) >? node(maptlist(F, X)) 
  maptlist(F, nil) >? nil 
  maptlist(F, cons(X, Y)) >? cons(mapt(F, X), maptlist(F, Y)) 

We orient these requirements with a polynomial interpretation in the natural numbers.

The following interpretation satisfies the requirements:

  cons = Lam[y0;y1].3 + y1 + 2*y0 
  leaf = Lam[y0].y0 
  mapt = Lam[G0;y1].2 + 3*y1 + G0(0) + 3*y1*G0(y1) + 3*G0(y1) 
  maptlist = Lam[G0;y1].3*y1 + G0(0) + G0(y1) + 3*y1*G0(y1) 
  nil = 0 
  node = Lam[y0].3 + 2*y0 

Using this interpretation, the requirements translate to:

  [[mapt(_F0, leaf(_x1))]] = 2 + 3*x1 + F0(0) + 3*x1*F0(x1) + 3*F0(x1) > x1 + F0(x1) = [[leaf(_F0 _x1)]] 
  [[mapt(_F0, node(_x1))]] = 11 + 6*x1 + F0(0) + 6*x1*F0(3 + 2*x1) + 12*F0(3 + 2*x1) > 3 + 6*x1 + 2*F0(0) + 2*F0(x1) + 6*x1*F0(x1) = [[node(maptlist(_F0, _x1))]] 
  [[maptlist(_F0, nil)]] = 2*F0(0) >= 0 = [[nil]] 
  [[maptlist(_F0, cons(_x1, _x2))]] = 9 + 3*x2 + 6*x1 + F0(0) + 3*x2*F0(3 + x2 + 2*x1) + 6*x1*F0(3 + x2 + 2*x1) + 10*F0(3 + x2 + 2*x1) > 7 + 3*x2 + 6*x1 + F0(x2) + 3*x2*F0(x2) + 3*F0(0) + 6*x1*F0(x1) + 6*F0(x1) = [[cons(mapt(_F0, _x1), maptlist(_F0, _x2))]] 

We can thus remove the following rules:

  mapt(F, leaf(X)) => leaf(F X) 
  mapt(F, node(X)) => node(maptlist(F, X)) 
  maptlist(F, cons(X, Y)) => cons(mapt(F, X), maptlist(F, Y)) 

We use rule removal, following [Kop12, Theorem 2.23].

This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]):

  maptlist(F, nil) >? nil 

We orient these requirements with a polynomial interpretation in the natural numbers.

The following interpretation satisfies the requirements:

  maptlist = Lam[G0;y1].3 + 3*y1 + 2*G0(0) + 2*G0(y1) 
  nil = 2 

Using this interpretation, the requirements translate to:

  [[maptlist(_F0, nil)]] = 9 + 2*F0(0) + 2*F0(2) > 2 = [[nil]] 

We can thus remove the following rules:

  maptlist(F, nil) => nil 

All rules were succesfully removed.  Thus, termination of the original system has been reduced to termination of the beta-rule, which is well-known to hold.


+++ Citations +++

[Kop12]  C. Kop.  Higher Order Termination.  PhD Thesis, 2012.