We consider the system AotoYamada_05__013.

  Alphabet:

    append : [c * c] --> c 
    cons : [b * c] --> c 
    flatwith : [a -> b * b] --> c 
    flatwithsub : [a -> b * c] --> c 
    leaf : [a] --> b 
    nil : [] --> c 
    node : [c] --> b 

  Rules:

    append(nil, x) => x 
    append(cons(x, y), z) => cons(x, append(y, z)) 
    flatwith(f, leaf(x)) => cons(f x, nil) 
    flatwith(f, node(x)) => flatwithsub(f, x) 
    flatwithsub(f, nil) => nil 
    flatwithsub(f, cons(x, y)) => append(flatwith(f, x), flatwithsub(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]):

  append(nil, X) >? X 
  append(cons(X, Y), Z) >? cons(X, append(Y, Z)) 
  flatwith(F, leaf(X)) >? cons(F X, nil) 
  flatwith(F, node(X)) >? flatwithsub(F, X) 
  flatwithsub(F, nil) >? nil 
  flatwithsub(F, cons(X, Y)) >? append(flatwith(F, X), flatwithsub(F, Y)) 

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

Argument functions:

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

We choose Lex = {} and Mul = {@_{o -> o}, append, cons, flatwith, flatwithsub}, and the following precedence: flatwith = flatwithsub > @_{o -> o} > append > cons

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

  append(_|_, X) >= X 
  append(cons(X, Y), Z) >= cons(X, append(Y, Z)) 
  flatwith(F, X) >= cons(@_{o -> o}(F, X), _|_) 
  flatwith(F, X) >= flatwithsub(F, X) 
  flatwithsub(F, _|_) >= _|_ 
  flatwithsub(F, cons(X, Y)) > append(flatwith(F, X), flatwithsub(F, Y)) 

With these choices, we have:

  1] append(_|_, X) >= X  because [2], by (Star) 
  2] append*(_|_, X) >= X  because [3], by (Select) 
  3] X >= X  by (Meta) 

  4] append(cons(X, Y), Z) >= cons(X, append(Y, Z))  because [5], by (Star) 
  5] append*(cons(X, Y), Z) >= cons(X, append(Y, Z))  because append > cons, [6] and [10], by (Copy) 
  6] append*(cons(X, Y), Z) >= X  because [7], by (Select) 
  7] cons(X, Y) >= X  because [8], by (Star) 
  8] cons*(X, Y) >= X  because [9], by (Select) 
  9] X >= X  by (Meta) 
  10] append*(cons(X, Y), Z) >= append(Y, Z)  because append in Mul, [11] and [14], by (Stat) 
  11] cons(X, Y) > Y  because [12], by definition 
  12] cons*(X, Y) >= Y  because [13], by (Select) 
  13] Y >= Y  by (Meta) 
  14] Z >= Z  by (Meta) 

  15] flatwith(F, X) >= cons(@_{o -> o}(F, X), _|_)  because [16], by (Star) 
  16] flatwith*(F, X) >= cons(@_{o -> o}(F, X), _|_)  because flatwith > cons, [17] and [22], by (Copy) 
  17] flatwith*(F, X) >= @_{o -> o}(F, X)  because flatwith > @_{o -> o}, [18] and [20], by (Copy) 
  18] flatwith*(F, X) >= F  because [19], by (Select) 
  19] F >= F  by (Meta) 
  20] flatwith*(F, X) >= X  because [21], by (Select) 
  21] X >= X  by (Meta) 
  22] flatwith*(F, X) >= _|_  by (Bot) 

  23] flatwith(F, X) >= flatwithsub(F, X)  because flatwith = flatwithsub, flatwith in Mul, [24] and [25], by (Fun) 
  24] F >= F  by (Meta) 
  25] X >= X  by (Meta) 

  26] flatwithsub(F, _|_) >= _|_  by (Bot) 

  27] flatwithsub(F, cons(X, Y)) > append(flatwith(F, X), flatwithsub(F, Y))  because [28], by definition 
  28] flatwithsub*(F, cons(X, Y)) >= append(flatwith(F, X), flatwithsub(F, Y))  because flatwithsub > append, [29] and [34], by (Copy) 
  29] flatwithsub*(F, cons(X, Y)) >= flatwith(F, X)  because flatwithsub = flatwith, flatwithsub in Mul, [30] and [31], by (Stat) 
  30] F >= F  by (Meta) 
  31] cons(X, Y) > X  because [32], by definition 
  32] cons*(X, Y) >= X  because [33], by (Select) 
  33] X >= X  by (Meta) 
  34] flatwithsub*(F, cons(X, Y)) >= flatwithsub(F, Y)  because flatwithsub in Mul, [30] and [35], by (Stat) 
  35] cons(X, Y) > Y  because [36], by definition 
  36] cons*(X, Y) >= Y  because [37], by (Select) 
  37] Y >= Y  by (Meta) 

We can thus remove the following rules:

  flatwithsub(F, cons(X, Y)) => append(flatwith(F, X), flatwithsub(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]):

  append(nil, X) >? X 
  append(cons(X, Y), Z) >? cons(X, append(Y, Z)) 
  flatwith(F, leaf(X)) >? cons(F X, nil) 
  flatwith(F, node(X)) >? flatwithsub(F, X) 
  flatwithsub(F, nil) >? nil 

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

Argument functions:

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

We choose Lex = {} and Mul = {@_{o -> o}, append, cons, flatwith, flatwithsub, leaf}, and the following precedence: flatwith = flatwithsub > leaf > append > @_{o -> o} > cons

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

  append(_|_, X) > X 
  append(cons(X, Y), Z) >= cons(X, append(Y, Z)) 
  flatwith(F, leaf(X)) > cons(@_{o -> o}(F, X), _|_) 
  flatwith(F, X) >= flatwithsub(F, X) 
  flatwithsub(F, _|_) >= _|_ 

With these choices, we have:

  1] append(_|_, X) > X  because [2], by definition 
  2] append*(_|_, X) >= X  because [3], by (Select) 
  3] X >= X  by (Meta) 

  4] append(cons(X, Y), Z) >= cons(X, append(Y, Z))  because [5], by (Star) 
  5] append*(cons(X, Y), Z) >= cons(X, append(Y, Z))  because append > cons, [6] and [10], by (Copy) 
  6] append*(cons(X, Y), Z) >= X  because [7], by (Select) 
  7] cons(X, Y) >= X  because [8], by (Star) 
  8] cons*(X, Y) >= X  because [9], by (Select) 
  9] X >= X  by (Meta) 
  10] append*(cons(X, Y), Z) >= append(Y, Z)  because append in Mul, [11] and [14], by (Stat) 
  11] cons(X, Y) > Y  because [12], by definition 
  12] cons*(X, Y) >= Y  because [13], by (Select) 
  13] Y >= Y  by (Meta) 
  14] Z >= Z  by (Meta) 

  15] flatwith(F, leaf(X)) > cons(@_{o -> o}(F, X), _|_)  because [16], by definition 
  16] flatwith*(F, leaf(X)) >= cons(@_{o -> o}(F, X), _|_)  because flatwith > cons, [17] and [24], by (Copy) 
  17] flatwith*(F, leaf(X)) >= @_{o -> o}(F, X)  because flatwith > @_{o -> o}, [18] and [20], by (Copy) 
  18] flatwith*(F, leaf(X)) >= F  because [19], by (Select) 
  19] F >= F  by (Meta) 
  20] flatwith*(F, leaf(X)) >= X  because [21], by (Select) 
  21] leaf(X) >= X  because [22], by (Star) 
  22] leaf*(X) >= X  because [23], by (Select) 
  23] X >= X  by (Meta) 
  24] flatwith*(F, leaf(X)) >= _|_  by (Bot) 

  25] flatwith(F, X) >= flatwithsub(F, X)  because flatwith = flatwithsub, flatwith in Mul, [26] and [27], by (Fun) 
  26] F >= F  by (Meta) 
  27] X >= X  by (Meta) 

  28] flatwithsub(F, _|_) >= _|_  by (Bot) 

We can thus remove the following rules:

  append(nil, X) => X 
  flatwith(F, leaf(X)) => cons(F X, nil) 

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

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

  append(cons(X, Y), Z) >? cons(X, append(Y, Z)) 
  flatwith(F, node(X)) >? flatwithsub(F, X) 
  flatwithsub(F, nil) >? nil 

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

Argument functions:

  [[nil]] = _|_ 

We choose Lex = {} and Mul = {append, cons, flatwith, flatwithsub, node}, and the following precedence: append > flatwith > node > cons > flatwithsub

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

  append(cons(X, Y), Z) > cons(X, append(Y, Z)) 
  flatwith(F, node(X)) >= flatwithsub(F, X) 
  flatwithsub(F, _|_) >= _|_ 

With these choices, we have:

  1] append(cons(X, Y), Z) > cons(X, append(Y, Z))  because [2], by definition 
  2] append*(cons(X, Y), Z) >= cons(X, append(Y, Z))  because append > cons, [3] and [7], by (Copy) 
  3] append*(cons(X, Y), Z) >= X  because [4], by (Select) 
  4] cons(X, Y) >= X  because [5], by (Star) 
  5] cons*(X, Y) >= X  because [6], by (Select) 
  6] X >= X  by (Meta) 
  7] append*(cons(X, Y), Z) >= append(Y, Z)  because append in Mul, [8] and [11], by (Stat) 
  8] cons(X, Y) > Y  because [9], by definition 
  9] cons*(X, Y) >= Y  because [10], by (Select) 
  10] Y >= Y  by (Meta) 
  11] Z >= Z  by (Meta) 

  12] flatwith(F, node(X)) >= flatwithsub(F, X)  because [13], by (Star) 
  13] flatwith*(F, node(X)) >= flatwithsub(F, X)  because flatwith > flatwithsub, [14] and [16], by (Copy) 
  14] flatwith*(F, node(X)) >= F  because [15], by (Select) 
  15] F >= F  by (Meta) 
  16] flatwith*(F, node(X)) >= X  because [17], by (Select) 
  17] node(X) >= X  because [18], by (Star) 
  18] node*(X) >= X  because [19], by (Select) 
  19] X >= X  by (Meta) 

  20] flatwithsub(F, _|_) >= _|_  by (Bot) 

We can thus remove the following rules:

  append(cons(X, Y), Z) => cons(X, append(Y, Z)) 

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

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

  flatwith(F, node(X)) >? flatwithsub(F, X) 
  flatwithsub(F, nil) >? nil 

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

Argument functions:

  [[nil]] = _|_ 

We choose Lex = {} and Mul = {flatwith, flatwithsub, node}, and the following precedence: flatwith > flatwithsub > node

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

  flatwith(F, node(X)) >= flatwithsub(F, X) 
  flatwithsub(F, _|_) > _|_ 

With these choices, we have:

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

  9] flatwithsub(F, _|_) > _|_  because [10], by definition 
  10] flatwithsub*(F, _|_) >= _|_  by (Bot) 

We can thus remove the following rules:

  flatwithsub(F, nil) => nil 

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

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

  flatwith(F, node(X)) >? flatwithsub(F, X) 

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

We choose Lex = {} and Mul = {flatwith, flatwithsub, node}, and the following precedence: flatwith > node > flatwithsub

With these choices, we have:

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

We can thus remove the following rules:

  flatwith(F, node(X)) => flatwithsub(F, X) 

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.