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 use a recursive path ordering as defined in [Kop12, Chapter 5].

Argument functions:

  [[leaf(x_1)]] = x_1 
  [[nil]] = _|_ 

We choose Lex = {} and Mul = {@_{o -> o}, cons, mapt, maptlist, node}, and the following precedence: mapt = maptlist > cons > @_{o -> o} > node

Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows:

  mapt(F, X) >= @_{o -> o}(F, X) 
  mapt(F, node(X)) >= node(maptlist(F, X)) 
  maptlist(F, _|_) >= _|_ 
  maptlist(F, cons(X, Y)) > cons(mapt(F, X), maptlist(F, Y)) 

With these choices, we have:

  1] mapt(F, X) >= @_{o -> o}(F, X)  because [2], by (Star) 
  2] mapt*(F, X) >= @_{o -> o}(F, X)  because mapt > @_{o -> o}, [3] and [5], by (Copy) 
  3] mapt*(F, X) >= F  because [4], by (Select) 
  4] F >= F  by (Meta) 
  5] mapt*(F, X) >= X  because [6], by (Select) 
  6] X >= X  by (Meta) 

  7] mapt(F, node(X)) >= node(maptlist(F, X))  because [8], by (Star) 
  8] mapt*(F, node(X)) >= node(maptlist(F, X))  because mapt > node and [9], by (Copy) 
  9] mapt*(F, node(X)) >= maptlist(F, X)  because mapt = maptlist, mapt in Mul, [10] and [11], by (Stat) 
  10] F >= F  by (Meta) 
  11] node(X) > X  because [12], by definition 
  12] node*(X) >= X  because [13], by (Select) 
  13] X >= X  by (Meta) 

  14] maptlist(F, _|_) >= _|_  by (Bot) 

  15] maptlist(F, cons(X, Y)) > cons(mapt(F, X), maptlist(F, Y))  because [16], by definition 
  16] maptlist*(F, cons(X, Y)) >= cons(mapt(F, X), maptlist(F, Y))  because maptlist > cons, [17] and [22], by (Copy) 
  17] maptlist*(F, cons(X, Y)) >= mapt(F, X)  because maptlist = mapt, maptlist in Mul, [18] and [19], by (Stat) 
  18] F >= F  by (Meta) 
  19] cons(X, Y) > X  because [20], by definition 
  20] cons*(X, Y) >= X  because [21], by (Select) 
  21] X >= X  by (Meta) 
  22] maptlist*(F, cons(X, Y)) >= maptlist(F, Y)  because maptlist in Mul, [18] and [23], by (Stat) 
  23] cons(X, Y) > Y  because [24], by definition 
  24] cons*(X, Y) >= Y  because [25], by (Select) 
  25] Y >= Y  by (Meta) 

We can thus remove the following rules:

  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]):

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

We use a recursive path ordering as defined in [Kop12, Chapter 5].

We choose Lex = {} and Mul = {@_{o -> o}, leaf, mapt, maptlist, nil, node}, and the following precedence: @_{o -> o} = mapt > leaf > node > maptlist > nil

With these choices, we have:

  1] mapt(F, leaf(X)) > leaf(@_{o -> o}(F, X))  because [2], by definition 
  2] mapt*(F, leaf(X)) >= leaf(@_{o -> o}(F, X))  because mapt > leaf and [3], by (Copy) 
  3] mapt*(F, leaf(X)) >= @_{o -> o}(F, X)  because mapt = @_{o -> o}, mapt in Mul, [4] and [5], by (Stat) 
  4] F >= F  by (Meta) 
  5] leaf(X) > X  because [6], by definition 
  6] leaf*(X) >= X  because [7], by (Select) 
  7] X >= X  by (Meta) 

  8] mapt(F, node(X)) >= node(maptlist(F, X))  because [9], by (Star) 
  9] mapt*(F, node(X)) >= node(maptlist(F, X))  because mapt > node and [10], by (Copy) 
  10] mapt*(F, node(X)) >= maptlist(F, X)  because mapt > maptlist, [11] and [13], by (Copy) 
  11] mapt*(F, node(X)) >= F  because [12], by (Select) 
  12] F >= F  by (Meta) 
  13] mapt*(F, node(X)) >= X  because [14], by (Select) 
  14] node(X) >= X  because [15], by (Star) 
  15] node*(X) >= X  because [16], by (Select) 
  16] X >= X  by (Meta) 

  17] maptlist(F, nil) >= nil  because [18], by (Star) 
  18] maptlist*(F, nil) >= nil  because maptlist > nil, by (Copy) 

We can thus remove the following rules:

  mapt(F, leaf(X)) => leaf(F X) 

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, node(X)) >? node(maptlist(F, X)) 
  maptlist(F, nil) >? nil 

We use a recursive path ordering as defined in [Kop12, Chapter 5].

We choose Lex = {} and Mul = {mapt, maptlist, nil, node}, and the following precedence: mapt > maptlist > nil > node

With these choices, we have:

  1] mapt(F, node(X)) > node(maptlist(F, X))  because [2], by definition 
  2] mapt*(F, node(X)) >= node(maptlist(F, X))  because mapt > node and [3], by (Copy) 
  3] mapt*(F, node(X)) >= maptlist(F, X)  because mapt > maptlist, [4] and [6], by (Copy) 
  4] mapt*(F, node(X)) >= F  because [5], by (Select) 
  5] F >= F  by (Meta) 
  6] mapt*(F, node(X)) >= X  because [7], by (Select) 
  7] node(X) >= X  because [8], by (Star) 
  8] node*(X) >= X  because [9], by (Select) 
  9] X >= X  by (Meta) 

  10] maptlist(F, nil) > nil  because [11], by definition 
  11] maptlist*(F, nil) >= nil  because maptlist > nil, by (Copy) 

We can thus remove the following rules:

  mapt(F, node(X)) => node(maptlist(F, X)) 
  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.