We consider the system Applicative_05__ReverseLastInit.

  Alphabet:

    compose : [a -> a * a -> a] --> a -> a 
    cons : [a * a] --> a 
    hd : [] --> a -> a 
    init : [] --> a -> a 
    last : [] --> a -> a 
    nil : [] --> a 
    reverse : [] --> a -> a 
    reverse2 : [a * a] --> a 
    tl : [] --> a -> a 

  Rules:

    compose(f, g) x => g (f x) 
    reverse x => reverse2(x, nil) 
    reverse2(nil, x) => x 
    reverse2(cons(x, y), z) => reverse2(y, cons(x, z)) 
    hd cons(x, y) => x 
    tl cons(x, y) => y 
    last => compose(hd, reverse) 
    init => compose(reverse, compose(tl, reverse)) 

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

  compose(F, G) X >? G (F X) 
  reverse X >? reverse2(X, nil) 
  reverse2(nil, X) >? X 
  reverse2(cons(X, Y), Z) >? reverse2(Y, cons(X, Z)) 
  hd cons(X, Y) >? X 
  tl cons(X, Y) >? Y 
  last >? compose(hd, reverse) 
  init >? compose(reverse, compose(tl, reverse)) 

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

Argument functions:

  [[hd]] = _|_ 
  [[nil]] = _|_ 
  [[reverse]] = _|_ 
  [[tl]] = _|_ 

We choose Lex = {reverse2} and Mul = {@_{o -> o}, compose, cons, init, last}, and the following precedence: init > last > compose > @_{o -> o} > reverse2 > cons

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

  @_{o -> o}(compose(F, G), X) >= @_{o -> o}(G, @_{o -> o}(F, X)) 
  @_{o -> o}(_|_, X) > reverse2(X, _|_) 
  reverse2(_|_, X) > X 
  reverse2(cons(X, Y), Z) >= reverse2(Y, cons(X, Z)) 
  @_{o -> o}(_|_, cons(X, Y)) >= X 
  @_{o -> o}(_|_, cons(X, Y)) >= Y 
  last >= compose(_|_, _|_) 
  init > compose(_|_, compose(_|_, _|_)) 

With these choices, we have:

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

  13] @_{o -> o}(_|_, X) > reverse2(X, _|_)  because [14], by definition 
  14] @_{o -> o}*(_|_, X) >= reverse2(X, _|_)  because @_{o -> o} > reverse2, [15] and [17], by (Copy) 
  15] @_{o -> o}*(_|_, X) >= X  because [16], by (Select) 
  16] X >= X  by (Meta) 
  17] @_{o -> o}*(_|_, X) >= _|_  by (Bot) 

  18] reverse2(_|_, X) > X  because [19], by definition 
  19] reverse2*(_|_, X) >= X  because [20], by (Select) 
  20] X >= X  by (Meta) 

  21] reverse2(cons(X, Y), Z) >= reverse2(Y, cons(X, Z))  because [22], by (Star) 
  22] reverse2*(cons(X, Y), Z) >= reverse2(Y, cons(X, Z))  because [23], [26] and [28], 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) 
  26] reverse2*(cons(X, Y), Z) >= Y  because [27], by (Select) 
  27] cons(X, Y) >= Y  because [24], by (Star) 
  28] reverse2*(cons(X, Y), Z) >= cons(X, Z)  because reverse2 > cons, [29] and [33], by (Copy) 
  29] reverse2*(cons(X, Y), Z) >= X  because [30], by (Select) 
  30] cons(X, Y) >= X  because [31], by (Star) 
  31] cons*(X, Y) >= X  because [32], by (Select) 
  32] X >= X  by (Meta) 
  33] reverse2*(cons(X, Y), Z) >= Z  because [34], by (Select) 
  34] Z >= Z  by (Meta) 

  35] @_{o -> o}(_|_, cons(X, Y)) >= X  because [36], by (Star) 
  36] @_{o -> o}*(_|_, cons(X, Y)) >= X  because [37], by (Select) 
  37] cons(X, Y) >= X  because [38], by (Star) 
  38] cons*(X, Y) >= X  because [39], by (Select) 
  39] X >= X  by (Meta) 

  40] @_{o -> o}(_|_, cons(X, Y)) >= Y  because [41], by (Star) 
  41] @_{o -> o}*(_|_, cons(X, Y)) >= Y  because [42], by (Select) 
  42] cons(X, Y) >= Y  because [43], by (Star) 
  43] cons*(X, Y) >= Y  because [44], by (Select) 
  44] Y >= Y  by (Meta) 

  45] last >= compose(_|_, _|_)  because [46], by (Star) 
  46] last* >= compose(_|_, _|_)  because last > compose, [47] and [48], by (Copy) 
  47] last* >= _|_  by (Bot) 
  48] last* >= _|_  by (Bot) 

  49] init > compose(_|_, compose(_|_, _|_))  because [50], by definition 
  50] init* >= compose(_|_, compose(_|_, _|_))  because init > compose, [51] and [52], by (Copy) 
  51] init* >= _|_  by (Bot) 
  52] init* >= compose(_|_, _|_)  because init > compose, [53] and [51], by (Copy) 
  53] init* >= _|_  by (Bot) 

We can thus remove the following rules:

  reverse X => reverse2(X, nil) 
  reverse2(nil, X) => X 
  init => compose(reverse, compose(tl, reverse)) 

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

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

  compose(F, G) X >? G (F X) 
  reverse2(cons(X, Y), Z) >? reverse2(Y, cons(X, Z)) 
  hd cons(X, Y) >? X 
  tl(cons(X, Y)) >? Y 
  last >? compose(hd, reverse) 

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

Argument functions:

  [[hd]] = _|_ 
  [[reverse]] = _|_ 
  [[tl(x_1)]] = x_1 

We choose Lex = {reverse2} and Mul = {@_{o -> o}, compose, cons, last}, and the following precedence: last > compose > @_{o -> o} > reverse2 > cons

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

  @_{o -> o}(compose(F, G), X) >= @_{o -> o}(G, @_{o -> o}(F, X)) 
  reverse2(cons(X, Y), Z) > reverse2(Y, cons(X, Z)) 
  @_{o -> o}(_|_, cons(X, Y)) >= X 
  cons(X, Y) > Y 
  last >= compose(_|_, _|_) 

With these choices, we have:

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

  13] reverse2(cons(X, Y), Z) > reverse2(Y, cons(X, Z))  because [14], by definition 
  14] reverse2*(cons(X, Y), Z) >= reverse2(Y, cons(X, Z))  because [15], [18] and [20], by (Stat) 
  15] cons(X, Y) > Y  because [16], by definition 
  16] cons*(X, Y) >= Y  because [17], by (Select) 
  17] Y >= Y  by (Meta) 
  18] reverse2*(cons(X, Y), Z) >= Y  because [19], by (Select) 
  19] cons(X, Y) >= Y  because [16], by (Star) 
  20] reverse2*(cons(X, Y), Z) >= cons(X, Z)  because reverse2 > cons, [21] and [25], by (Copy) 
  21] reverse2*(cons(X, Y), Z) >= X  because [22], by (Select) 
  22] cons(X, Y) >= X  because [23], by (Star) 
  23] cons*(X, Y) >= X  because [24], by (Select) 
  24] X >= X  by (Meta) 
  25] reverse2*(cons(X, Y), Z) >= Z  because [26], by (Select) 
  26] Z >= Z  by (Meta) 

  27] @_{o -> o}(_|_, cons(X, Y)) >= X  because [28], by (Star) 
  28] @_{o -> o}*(_|_, cons(X, Y)) >= X  because [29], by (Select) 
  29] cons(X, Y) >= X  because [30], by (Star) 
  30] cons*(X, Y) >= X  because [31], by (Select) 
  31] X >= X  by (Meta) 

  32] cons(X, Y) > Y  because [33], by definition 
  33] cons*(X, Y) >= Y  because [34], by (Select) 
  34] Y >= Y  by (Meta) 

  35] last >= compose(_|_, _|_)  because [36], by (Star) 
  36] last* >= compose(_|_, _|_)  because last > compose, [37] and [38], by (Copy) 
  37] last* >= _|_  by (Bot) 
  38] last* >= _|_  by (Bot) 

We can thus remove the following rules:

  reverse2(cons(X, Y), Z) => reverse2(Y, cons(X, Z)) 
  tl(cons(X, Y)) => 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]):

  compose(F, G) X >? G (F X) 
  hd cons(X, Y) >? X 
  last >? compose(hd, reverse) 

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

Argument functions:

  [[hd]] = _|_ 
  [[reverse]] = _|_ 

We choose Lex = {} and Mul = {@_{o -> o}, compose, cons, last}, and the following precedence: cons > last > compose > @_{o -> o}

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

  @_{o -> o}(compose(F, G), X) > @_{o -> o}(G, @_{o -> o}(F, X)) 
  @_{o -> o}(_|_, cons(X, Y)) > X 
  last > compose(_|_, _|_) 

With these choices, we have:

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

  13] @_{o -> o}(_|_, cons(X, Y)) > X  because [14], by definition 
  14] @_{o -> o}*(_|_, cons(X, Y)) >= X  because [15], by (Select) 
  15] cons(X, Y) >= X  because [16], by (Star) 
  16] cons*(X, Y) >= X  because [17], by (Select) 
  17] X >= X  by (Meta) 

  18] last > compose(_|_, _|_)  because [19], by definition 
  19] last* >= compose(_|_, _|_)  because last > compose, [20] and [21], by (Copy) 
  20] last* >= _|_  by (Bot) 
  21] last* >= _|_  by (Bot) 

We can thus remove the following rules:

  compose(F, G) X => G (F X) 
  hd cons(X, Y) => X 
  last => compose(hd, reverse) 

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.