We consider the system AotoYamada_05__006.

  Alphabet:

    branch : [a * b * b] --> b 
    leaf : [a] --> b 
    mapbt : [a -> a * b] --> b 

  Rules:

    mapbt(f, leaf(x)) => leaf(f x) 
    mapbt(f, branch(x, y, z)) => branch(f x, mapbt(f, y), mapbt(f, z)) 

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

  mapbt(F, leaf(X)) >? leaf(F X) 
  mapbt(F, branch(X, Y, Z)) >? branch(F X, mapbt(F, Y), mapbt(F, Z)) 

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

We choose Lex = {} and Mul = {@_{o -> o}, branch, leaf, mapbt}, and the following precedence: mapbt > @_{o -> o} > branch > leaf

With these choices, we have:

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

  10] mapbt(F, branch(X, Y, Z)) >= branch(@_{o -> o}(F, X), mapbt(F, Y), mapbt(F, Z))  because [11], by (Star) 
  11] mapbt*(F, branch(X, Y, Z)) >= branch(@_{o -> o}(F, X), mapbt(F, Y), mapbt(F, Z))  because mapbt > branch, [12], [19] and [24], by (Copy) 
  12] mapbt*(F, branch(X, Y, Z)) >= @_{o -> o}(F, X)  because mapbt > @_{o -> o}, [13] and [15], by (Copy) 
  13] mapbt*(F, branch(X, Y, Z)) >= F  because [14], by (Select) 
  14] F >= F  by (Meta) 
  15] mapbt*(F, branch(X, Y, Z)) >= X  because [16], by (Select) 
  16] branch(X, Y, Z) >= X  because [17], by (Star) 
  17] branch*(X, Y, Z) >= X  because [18], by (Select) 
  18] X >= X  by (Meta) 
  19] mapbt*(F, branch(X, Y, Z)) >= mapbt(F, Y)  because mapbt in Mul, [20] and [21], by (Stat) 
  20] F >= F  by (Meta) 
  21] branch(X, Y, Z) > Y  because [22], by definition 
  22] branch*(X, Y, Z) >= Y  because [23], by (Select) 
  23] Y >= Y  by (Meta) 
  24] mapbt*(F, branch(X, Y, Z)) >= mapbt(F, Z)  because mapbt in Mul, [20] and [25], by (Stat) 
  25] branch(X, Y, Z) > Z  because [26], by definition 
  26] branch*(X, Y, Z) >= Z  because [27], by (Select) 
  27] Z >= Z  by (Meta) 

We can thus remove the following rules:

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

  mapbt(F, branch(X, Y, Z)) >? branch(F X, mapbt(F, Y), mapbt(F, Z)) 

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

We choose Lex = {} and Mul = {@_{o -> o}, branch, mapbt}, and the following precedence: mapbt > @_{o -> o} > branch

With these choices, we have:

  1] mapbt(F, branch(X, Y, Z)) > branch(@_{o -> o}(F, X), mapbt(F, Y), mapbt(F, Z))  because [2], by definition 
  2] mapbt*(F, branch(X, Y, Z)) >= branch(@_{o -> o}(F, X), mapbt(F, Y), mapbt(F, Z))  because mapbt > branch, [3], [10] and [15], by (Copy) 
  3] mapbt*(F, branch(X, Y, Z)) >= @_{o -> o}(F, X)  because mapbt > @_{o -> o}, [4] and [6], by (Copy) 
  4] mapbt*(F, branch(X, Y, Z)) >= F  because [5], by (Select) 
  5] F >= F  by (Meta) 
  6] mapbt*(F, branch(X, Y, Z)) >= X  because [7], by (Select) 
  7] branch(X, Y, Z) >= X  because [8], by (Star) 
  8] branch*(X, Y, Z) >= X  because [9], by (Select) 
  9] X >= X  by (Meta) 
  10] mapbt*(F, branch(X, Y, Z)) >= mapbt(F, Y)  because mapbt in Mul, [11] and [12], by (Stat) 
  11] F >= F  by (Meta) 
  12] branch(X, Y, Z) > Y  because [13], by definition 
  13] branch*(X, Y, Z) >= Y  because [14], by (Select) 
  14] Y >= Y  by (Meta) 
  15] mapbt*(F, branch(X, Y, Z)) >= mapbt(F, Z)  because mapbt in Mul, [11] and [16], by (Stat) 
  16] branch(X, Y, Z) > Z  because [17], by definition 
  17] branch*(X, Y, Z) >= Z  because [18], by (Select) 
  18] Z >= Z  by (Meta) 

We can thus remove the following rules:

  mapbt(F, branch(X, Y, Z)) => branch(F X, mapbt(F, Y), mapbt(F, Z)) 

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.