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: last > init > 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 (Star) 
  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 (Star) 
  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 definition 
  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 definition 
  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 (Star) 
  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:

  tl cons(X, Y) => Y 
  last => compose(hd, 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) 
  reverse X >? reverse2(X, nil) 
  reverse2(nil, X) >? X 
  reverse2(cons(X, Y), Z) >? reverse2(Y, cons(X, Z)) 
  hd(cons(X, Y)) >? X 
  init >? compose(reverse, compose(tl, reverse)) 

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

Argument functions:

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

We choose Lex = {reverse2} and Mul = {@_{o -> o}, compose, cons, hd, init}, and the following precedence: init > compose > hd > @_{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)) 
  hd(cons(X, Y)) >= X 
  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 (Star) 
  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] hd(cons(X, Y)) >= X  because [36], by (Star) 
  36] hd*(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] init > compose(_|_, compose(_|_, _|_))  because [41], by definition 
  41] init* >= compose(_|_, compose(_|_, _|_))  because init > compose, [42] and [43], by (Copy) 
  42] init* >= _|_  by (Bot) 
  43] init* >= compose(_|_, _|_)  because init > compose, [44] and [42], by (Copy) 
  44] init* >= _|_  by (Bot) 

We can thus remove the following rules:

  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) 
  reverse(X) >? reverse2(X, nil) 
  reverse2(cons(X, Y), Z) >? reverse2(Y, cons(X, Z)) 
  hd(cons(X, Y)) >? X 

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

Argument functions:

  [[nil]] = _|_ 

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

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

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

With these choices, we have:

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

  10] reverse(X) > reverse2(X, _|_)  because [11], by definition 
  11] reverse*(X) >= reverse2(X, _|_)  because reverse > reverse2, [12] and [14], by (Copy) 
  12] reverse*(X) >= X  because [13], by (Select) 
  13] X >= X  by (Meta) 
  14] reverse*(X) >= _|_  by (Bot) 

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

  29] hd(cons(X, Y)) >= X  because [30], by (Star) 
  30] hd*(cons(X, Y)) >= X  because [31], by (Select) 
  31] cons(X, Y) >= X  because [32], by (Star) 
  32] cons*(X, Y) >= X  because [33], by (Select) 
  33] X >= X  by (Meta) 

We can thus remove the following rules:

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

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

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

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

With these choices, we have:

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

  10] hd(cons(X, Y)) >= X  because [11], by (Star) 
  11] hd*(cons(X, Y)) >= X  because [12], by (Select) 
  12] cons(X, Y) >= X  because [13], by (Star) 
  13] cons*(X, Y) >= X  because [14], by (Select) 
  14] X >= X  by (Meta) 

We can thus remove the following rules:

  compose(F, G, X) => G (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]):

  hd(cons(X, Y)) >? X 

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

We choose Lex = {} and Mul = {cons, hd}, and the following precedence: cons > hd

With these choices, we have:

  1] hd(cons(X, Y)) > X  because [2], by definition 
  2] hd*(cons(X, Y)) >= X  because [3], by (Select) 
  3] cons(X, Y) >= X  because [4], by (Star) 
  4] cons*(X, Y) >= X  because [5], by (Select) 
  5] X >= X  by (Meta) 

We can thus remove the following rules:

  hd(cons(X, Y)) => 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.