We consider the system reverse.

  Alphabet:

    app : [list * list] --> list 
    cons : [nat * list] --> list 
    foldl : [list -> nat -> list * list * list] --> list 
    iconsc : [] --> list -> nat -> list 
    nil : [] --> list 
    reverse : [list] --> list 
    reverse1 : [list] --> list 

  Rules:

    app(nil, x) => x 
    app(cons(x, y), z) => cons(x, app(y, z)) 
    foldl(f, x, nil) => x 
    foldl(f, x, cons(y, z)) => foldl(f, f x y, z) 
    iconsc => /\x./\y.cons(y, x) 
    reverse(x) => foldl(iconsc, nil, x) 
    reverse1(x) => foldl(/\y./\z.app(cons(z, nil), y), nil, x) 

This AFS is converted to an AFSM simply by replacing all free variables by meta-variables (with arity 0).

We use the dependency pair framework as described in [Kop12, Ch. 6/7], with dynamic dependency pairs.

To start, the system is beta-saturated by adding the following rules:

  iconsc X => /\x.cons(x, X) 
  iconsc X Y => cons(Y, X) 

After applying [Kop12, Thm. 7.22] to denote collapsing dependency pairs in an extended form, we thus obtain the following dependency pair problem (P_0, R_0, minimal, formative):

  Dependency Pairs P_0:

    0] app#(cons(X, Y), Z) =#> app#(Y, Z)   
    1] foldl#(F, X, cons(Y, Z)) =#> foldl#(F, F X Y, Z)   
    2] foldl#(F, X, cons(Y, Z)) =#> F(X, Y)   
    3] reverse#(X) =#> foldl#(iconsc, nil, X)   
    4] reverse#(X) =#> iconsc#   
    5] reverse1#(X) =#> foldl#(/\x./\y.app(cons(y, nil), x), nil, X)   
    6] reverse1#(X) =#> app#(cons(x, nil), y)   

  Rules R_0:

    app(nil, X) => X 
    app(cons(X, Y), Z) => cons(X, app(Y, Z)) 
    foldl(F, X, nil) => X 
    foldl(F, X, cons(Y, Z)) => foldl(F, F X Y, Z) 
    iconsc => /\x./\y.cons(y, x) 
    reverse(X) => foldl(iconsc, nil, X) 
    reverse1(X) => foldl(/\x./\y.app(cons(y, nil), x), nil, X) 
    iconsc X => /\x.cons(x, X) 
    iconsc X Y => cons(Y, X) 

Thus, the original system is terminating if (P_0, R_0, minimal, formative) is finite.

We consider the dependency pair problem (P_0, R_0, minimal, formative).

We place the elements of P in a dependency graph approximation G (see e.g. [Kop12, Thm. 7.27, 7.29], as follows:

    * 0 : 0 
    * 1 : 1, 2 
    * 2 : 0, 1, 2, 3, 4, 5, 6 
    * 3 : 1, 2 
    * 4 :  
    * 5 : 1, 2 
    * 6 :  

This graph has the following strongly connected components:

  P_1:

    app#(cons(X, Y), Z) =#> app#(Y, Z)   

  P_2:

    foldl#(F, X, cons(Y, Z)) =#> foldl#(F, F X Y, Z)   
    foldl#(F, X, cons(Y, Z)) =#> F(X, Y)   
    reverse#(X) =#> foldl#(iconsc, nil, X)   
    reverse1#(X) =#> foldl#(/\x./\y.app(cons(y, nil), x), nil, X)   

By [Kop12, Thm. 7.31], we may replace any dependency pair problem (P_0, R_0, m, f) by (P_1, R_0, m, f) and (P_2, R_0, m, f).

Thus, the original system is terminating if each of (P_1, R_0, minimal, formative) and (P_2, R_0, minimal, formative) is finite.

We consider the dependency pair problem (P_2, R_0, minimal, formative).

The formative rules of (P_2, R_0) are R_1 ::=

  app(nil, X) => X 
  app(cons(X, Y), Z) => cons(X, app(Y, Z)) 
  foldl(F, X, nil) => X 
  foldl(F, X, cons(Y, Z)) => foldl(F, F X Y, Z) 
  reverse(X) => foldl(iconsc, nil, X) 
  reverse1(X) => foldl(/\x./\y.app(cons(y, nil), x), nil, X) 
  iconsc X Y => cons(Y, X) 

By [Kop12, Thm. 7.17], we may replace the dependency pair problem (P_2, R_0, minimal, formative) by (P_2, R_1, minimal, formative).

Thus, the original system is terminating if each of (P_1, R_0, minimal, formative) and (P_2, R_1, minimal, formative) is finite.

We consider the dependency pair problem (P_2, R_1, minimal, formative).

We will use the reduction pair processor [Kop12, Thm. 7.16].  As the system is abstraction-simple and the formative flag is set, it suffices to find a tagged reduction pair [Kop12, Def. 6.70].  Thus, we must orient:

  foldl#(F, X, cons(Y, Z)) >? foldl#(F, F X Y, Z) 
  foldl#(F, X, cons(Y, Z)) >? F(X, Y) 
  reverse#(X) >? foldl#(iconsc, nil, X) 
  reverse1#(X) >? foldl#(/\x./\y.app-(cons-(y, nil), x), nil, X) 
  app(nil, X) >= X 
  app(cons(X, Y), Z) >= cons(X, app(Y, Z)) 
  foldl(F, X, nil) >= X 
  foldl(F, X, cons(Y, Z)) >= foldl(F, F X Y, Z) 
  reverse(X) >= foldl(iconsc, nil, X) 
  reverse1(X) >= foldl(/\x./\y.app-(cons-(y, nil), x), nil, X) 
  iconsc X Y >= cons(Y, X) 
  app-(X, Y) >= app(X, Y) 
  cons-(X, Y) >= cons(X, Y) 

We apply [Kop12, Thm. 6.75] and use the following argument functions:

  pi( iconsc ) = #argfun-iconsc#(/\x./\y.cons(y, x)) 
  pi( reverse(X) ) = #argfun-reverse#(foldl(#argfun-iconsc#(/\x./\y.cons(y, x)), nil, X)) 
  pi( reverse1(X) ) = #argfun-reverse1#(foldl(/\x./\y.app-(cons-(y, nil), x), nil, X)) 
  pi( reverse1#(X) ) = #argfun-reverse1##(foldl#(/\x./\y.app-(cons-(y, nil), x), nil, X)) 
  pi( reverse#(X) ) = #argfun-reverse##(foldl#(#argfun-iconsc#(/\x./\y.cons(y, x)), nil, X)) 

Since this representation is not advantageous for the higher-order recursive path ordering, we present the strict requirements in their unextended form, which is not problematic since for any F, s and substituion gamma: (F s)gamma beta-reduces to F(s)gamma.)

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

Argument functions:

  [[#argfun-iconsc#(x_1)]] = #argfun-iconsc# 
  [[#argfun-reverse#(x_1)]] = x_1 
  [[#argfun-reverse1##(x_1)]] = x_1 
  [[#argfun-reverse##(x_1)]] = x_1 
  [[foldl(x_1, x_2, x_3)]] = foldl(x_1, x_3, x_2) 
  [[foldl#(x_1, x_2, x_3)]] = foldl#(x_3, x_1, x_2) 
  [[reverse(x_1)]] = x_1 
  [[reverse1#(x_1)]] = x_1 
  [[reverse#(x_1)]] = x_1 

We choose Lex = {foldl, foldl#} and Mul = {#argfun-iconsc#, #argfun-reverse1#, @_{o -> o -> o}, @_{o -> o}, app, app-, cons, cons-, iconsc, nil, reverse1}, and the following precedence: app- > nil > app > foldl# > foldl > iconsc > #argfun-iconsc# > cons- > @_{o -> o -> o} > @_{o -> o} > reverse1 > cons > #argfun-reverse1#

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

  foldl#(F, X, cons(Y, Z)) > foldl#(F, @_{o -> o}(@_{o -> o -> o}(F, X), Y), Z) 
  foldl#(F, X, cons(Y, Z)) >= @_{o -> o}(@_{o -> o -> o}(F, X), Y) 
  foldl#(#argfun-iconsc#, nil, X) >= foldl#(#argfun-iconsc#, nil, X) 
  foldl#(/\x./\y.app-(cons-(y, nil), x), nil, X) >= foldl#(/\x./\y.app-(cons-(y, nil), x), nil, X) 
  app(nil, X) >= X 
  app(cons(X, Y), Z) >= cons(X, app(Y, Z)) 
  foldl(F, X, nil) >= X 
  foldl(F, X, cons(Y, Z)) >= foldl(F, @_{o -> o}(@_{o -> o -> o}(F, X), Y), Z) 
  foldl(#argfun-iconsc#, nil, X) >= foldl(#argfun-iconsc#, nil, X) 
  #argfun-reverse1#(foldl(/\x./\y.app-(cons-(y, nil), x), nil, X)) >= foldl(/\x./\y.app-(cons-(y, nil), x), nil, X) 
  @_{o -> o}(@_{o -> o -> o}(#argfun-iconsc#, X), Y) >= cons(Y, X) 
  app-(X, Y) >= app(X, Y) 
  cons-(X, Y) >= cons(X, Y) 

With these choices, we have:

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

  18] foldl#(F, X, cons(Y, Z)) >= @_{o -> o}(@_{o -> o -> o}(F, X), Y)  because [8], by (Star) 

  19] foldl#(#argfun-iconsc#, nil, X) >= foldl#(#argfun-iconsc#, nil, X)  because [20], [21] and [22], by (Fun) 
  20] #argfun-iconsc# >= #argfun-iconsc#  because #argfun-iconsc# in Mul, by (Fun) 
  21] nil >= nil  by (Fun) 
  22] X >= X  by (Meta) 

  23] foldl#(/\x./\y.app-(cons-(y, nil), x), nil, X) >= foldl#(/\x./\y.app-(cons-(y, nil), x), nil, X)  because [24], [21] and [30], by (Fun) 
  24] /\x./\z.app-(cons-(z, nil), x) >= /\x./\z.app-(cons-(z, nil), x)  because [25], by (Abs) 
  25] /\z.app-(cons-(z, nil), y) >= /\z.app-(cons-(z, nil), y)  because [26], by (Abs) 
  26] app-(cons-(x, nil), y) >= app-(cons-(x, nil), y)  because app- in Mul, [27] and [29], by (Fun) 
  27] cons-(x, nil) >= cons-(x, nil)  because cons- in Mul, [28] and [21], by (Fun) 
  28] x >= x  by (Var) 
  29] y >= y  by (Var) 
  30] X >= X  by (Meta) 

  31] app(nil, X) >= X  because [32], by (Star) 
  32] app*(nil, X) >= X  because [33], by (Select) 
  33] X >= X  by (Meta) 

  34] app(cons(X, Y), Z) >= cons(X, app(Y, Z))  because [35], by (Star) 
  35] app*(cons(X, Y), Z) >= cons(X, app(Y, Z))  because app > cons, [36] and [40], by (Copy) 
  36] app*(cons(X, Y), Z) >= 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] app*(cons(X, Y), Z) >= app(Y, Z)  because app in Mul, [41] and [44], by (Stat) 
  41] cons(X, Y) > Y  because [42], by definition 
  42] cons*(X, Y) >= Y  because [43], by (Select) 
  43] Y >= Y  by (Meta) 
  44] Z >= Z  by (Meta) 

  45] foldl(F, X, nil) >= X  because [46], by (Star) 
  46] foldl*(F, X, nil) >= X  because [47], by (Select) 
  47] X >= X  by (Meta) 

  48] foldl(F, X, cons(Y, Z)) >= foldl(F, @_{o -> o}(@_{o -> o -> o}(F, X), Y), Z)  because [49], by (Star) 
  49] foldl*(F, X, cons(Y, Z)) >= foldl(F, @_{o -> o}(@_{o -> o -> o}(F, X), Y), Z)  because [50], [3], [51], [52] and [56], by (Stat) 
  50] F >= F  by (Meta) 
  51] foldl*(F, X, cons(Y, Z)) >= F  because [50], by (Select) 
  52] foldl*(F, X, cons(Y, Z)) >= @_{o -> o}(@_{o -> o -> o}(F, X), Y)  because foldl > @_{o -> o}, [53] and [55], by (Copy) 
  53] foldl*(F, X, cons(Y, Z)) >= @_{o -> o -> o}(F, X)  because foldl > @_{o -> o -> o}, [51] and [54], by (Copy) 
  54] foldl*(F, X, cons(Y, Z)) >= X  because [11], by (Select) 
  55] foldl*(F, X, cons(Y, Z)) >= Y  because [13], by (Select) 
  56] foldl*(F, X, cons(Y, Z)) >= Z  because [17], by (Select) 

  57] foldl(#argfun-iconsc#, nil, X) >= foldl(#argfun-iconsc#, nil, X)  because [20], [21] and [22], by (Fun) 

  58] #argfun-reverse1#(foldl(/\x./\y.app-(cons-(y, nil), x), nil, X)) >= foldl(/\x./\y.app-(cons-(y, nil), x), nil, X)  because [59], by (Star) 
  59] #argfun-reverse1#*(foldl(/\x./\y.app-(cons-(y, nil), x), nil, X)) >= foldl(/\x./\y.app-(cons-(y, nil), x), nil, X)  because [60], by (Select) 
  60] foldl(/\x./\y.app-(cons-(y, nil), x), nil, X) >= foldl(/\x./\y.app-(cons-(y, nil), x), nil, X)  because [24], [21] and [30], by (Fun) 

  61] @_{o -> o}(@_{o -> o -> o}(#argfun-iconsc#, X), Y) >= cons(Y, X)  because [62], by (Star) 
  62] @_{o -> o}*(@_{o -> o -> o}(#argfun-iconsc#, X), Y) >= cons(Y, X)  because @_{o -> o} > cons, [63] and [65], by (Copy) 
  63] @_{o -> o}*(@_{o -> o -> o}(#argfun-iconsc#, X), Y) >= Y  because [64], by (Select) 
  64] Y >= Y  by (Meta) 
  65] @_{o -> o}*(@_{o -> o -> o}(#argfun-iconsc#, X), Y) >= X  because [66], by (Select) 
  66] @_{o -> o -> o}(#argfun-iconsc#, X) @_{o -> o}*(@_{o -> o -> o}(#argfun-iconsc#, X), Y) >= X  because [67] 
  67] @_{o -> o -> o}*(#argfun-iconsc#, X, @_{o -> o}*(@_{o -> o -> o}(#argfun-iconsc#, X), Y)) >= X  because [68], by (Select) 
  68] X >= X  by (Meta) 

  69] app-(X, Y) >= app(X, Y)  because [70], by (Star) 
  70] app-*(X, Y) >= app(X, Y)  because app- > app, [71] and [73], by (Copy) 
  71] app-*(X, Y) >= X  because [72], by (Select) 
  72] X >= X  by (Meta) 
  73] app-*(X, Y) >= Y  because [74], by (Select) 
  74] Y >= Y  by (Meta) 

  75] cons-(X, Y) >= cons(X, Y)  because [76], by (Star) 
  76] cons-*(X, Y) >= cons(X, Y)  because cons- > cons, [77] and [79], by (Copy) 
  77] cons-*(X, Y) >= X  because [78], by (Select) 
  78] X >= X  by (Meta) 
  79] cons-*(X, Y) >= Y  because [80], by (Select) 
  80] Y >= Y  by (Meta) 

By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_2, R_1, minimal, formative) by (P_3, R_1, minimal, formative), where P_3 consists of:

  foldl#(F, X, cons(Y, Z)) =#> F(X, Y)   
  reverse#(X) =#> foldl#(iconsc, nil, X)   
  reverse1#(X) =#> foldl#(/\x./\y.app(cons(y, nil), x), nil, X)   

Thus, the original system is terminating if each of (P_1, R_0, minimal, formative) and (P_3, R_1, minimal, formative) is finite.

We consider the dependency pair problem (P_3, R_1, minimal, formative).

We will use the reduction pair processor [Kop12, Thm. 7.16].  As the system is abstraction-simple and the formative flag is set, it suffices to find a tagged reduction pair [Kop12, Def. 6.70].  Thus, we must orient:

  foldl#(F, X, cons(Y, Z)) >? F(X, Y) 
  reverse#(X) >? foldl#(iconsc, nil, X) 
  reverse1#(X) >? foldl#(/\x./\y.app-(cons-(y, nil), x), nil, X) 
  app(nil, X) >= X 
  app(cons(X, Y), Z) >= cons(X, app(Y, Z)) 
  foldl(F, X, nil) >= X 
  foldl(F, X, cons(Y, Z)) >= foldl(F, F X Y, Z) 
  reverse(X) >= foldl(iconsc, nil, X) 
  reverse1(X) >= foldl(/\x./\y.app-(cons-(y, nil), x), nil, X) 
  iconsc X Y >= cons(Y, X) 
  app-(X, Y) >= app(X, Y) 
  cons-(X, Y) >= cons(X, Y) 

We apply [Kop12, Thm. 6.75] and use the following argument functions:

  pi( iconsc ) = #argfun-iconsc#(/\x./\y.cons(y, x)) 
  pi( reverse(X) ) = #argfun-reverse#(foldl(#argfun-iconsc#(/\x./\y.cons(y, x)), nil, X)) 
  pi( reverse1(X) ) = #argfun-reverse1#(foldl(/\x./\y.app-(cons-(y, nil), x), nil, X)) 
  pi( reverse1#(X) ) = #argfun-reverse1##(foldl#(/\x./\y.app-(cons-(y, nil), x), nil, X)) 
  pi( reverse#(X) ) = #argfun-reverse##(foldl#(#argfun-iconsc#(/\x./\y.cons(y, x)), nil, X)) 

Since this representation is not advantageous for the higher-order recursive path ordering, we present the strict requirements in their unextended form, which is not problematic since for any F, s and substituion gamma: (F s)gamma beta-reduces to F(s)gamma.)

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

Argument functions:

  [[#argfun-reverse#(x_1)]] = x_1 
  [[#argfun-reverse##(x_1)]] = x_1 
  [[foldl(x_1, x_2, x_3)]] = foldl(x_1, x_3, x_2) 
  [[reverse(x_1)]] = x_1 
  [[reverse1(x_1)]] = x_1 
  [[reverse1#(x_1)]] = x_1 
  [[reverse#(x_1)]] = x_1 

We choose Lex = {foldl} and Mul = {#argfun-iconsc#, #argfun-reverse1#, #argfun-reverse1##, @_{o -> o -> o}, @_{o -> o}, app, app-, cons, cons-, foldl#, iconsc, nil}, and the following precedence: #argfun-reverse1# > #argfun-reverse1## > iconsc > app- > app > foldl# > cons- > #argfun-iconsc# > foldl > @_{o -> o -> o} > @_{o -> o} > cons > nil

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

  foldl#(F, X, cons(Y, Z)) > @_{o -> o}(@_{o -> o -> o}(F, X), Y) 
  foldl#(#argfun-iconsc#(/\x./\y.cons(y, x)), nil, X) >= foldl#(#argfun-iconsc#(/\x./\y.cons(y, x)), nil, X) 
  #argfun-reverse1##(foldl#(/\x./\y.app-(cons-(y, nil), x), nil, X)) >= foldl#(/\x./\y.app-(cons-(y, nil), x), nil, X) 
  app(nil, X) >= X 
  app(cons(X, Y), Z) >= cons(X, app(Y, Z)) 
  foldl(F, X, nil) >= X 
  foldl(F, X, cons(Y, Z)) >= foldl(F, @_{o -> o}(@_{o -> o -> o}(F, X), Y), Z) 
  foldl(#argfun-iconsc#(/\x./\y.cons(y, x)), nil, X) >= foldl(#argfun-iconsc#(/\x./\y.cons(y, x)), nil, X) 
  #argfun-reverse1#(foldl(/\x./\y.app-(cons-(y, nil), x), nil, X)) >= foldl(/\x./\y.app-(cons-(y, nil), x), nil, X) 
  @_{o -> o}(@_{o -> o -> o}(#argfun-iconsc#(/\x./\y.cons(y, x)), X), Y) >= cons(Y, X) 
  app-(X, Y) >= app(X, Y) 
  cons-(X, Y) >= cons(X, Y) 

With these choices, we have:

  1] foldl#(F, X, cons(Y, Z)) > @_{o -> o}(@_{o -> o -> o}(F, X), Y)  because [2], by definition 
  2] foldl#*(F, X, cons(Y, Z)) >= @_{o -> o}(@_{o -> o -> o}(F, X), Y)  because foldl# > @_{o -> o}, [3] and [8], by (Copy) 
  3] foldl#*(F, X, cons(Y, Z)) >= @_{o -> o -> o}(F, X)  because foldl# > @_{o -> o -> o}, [4] and [6], by (Copy) 
  4] foldl#*(F, X, cons(Y, Z)) >= F  because [5], by (Select) 
  5] F >= F  by (Meta) 
  6] foldl#*(F, X, cons(Y, Z)) >= X  because [7], by (Select) 
  7] X >= X  by (Meta) 
  8] foldl#*(F, X, cons(Y, Z)) >= Y  because [9], by (Select) 
  9] cons(Y, Z) >= Y  because [10], by (Star) 
  10] cons*(Y, Z) >= Y  because [11], by (Select) 
  11] Y >= Y  by (Meta) 

  12] foldl#(#argfun-iconsc#(/\x./\y.cons(y, x)), nil, X) >= foldl#(#argfun-iconsc#(/\x./\y.cons(y, x)), nil, X)  because foldl# in Mul, [13], [19] and [20], by (Fun) 
  13] #argfun-iconsc#(/\x./\y.cons(y, x)) >= #argfun-iconsc#(/\x./\y.cons(y, x))  because #argfun-iconsc# in Mul and [14], by (Fun) 
  14] /\x./\z.cons(z, x) >= /\x./\z.cons(z, x)  because [15], by (Abs) 
  15] /\z.cons(z, y) >= /\z.cons(z, y)  because [16], by (Abs) 
  16] cons(x, y) >= cons(x, y)  because cons in Mul, [17] and [18], by (Fun) 
  17] x >= x  by (Var) 
  18] y >= y  by (Var) 
  19] nil >= nil  by (Fun) 
  20] X >= X  by (Meta) 

  21] #argfun-reverse1##(foldl#(/\x./\y.app-(cons-(y, nil), x), nil, X)) >= foldl#(/\x./\y.app-(cons-(y, nil), x), nil, X)  because [22], by (Star) 
  22] #argfun-reverse1##*(foldl#(/\x./\y.app-(cons-(y, nil), x), nil, X)) >= foldl#(/\x./\y.app-(cons-(y, nil), x), nil, X)  because #argfun-reverse1## > foldl#, [23], [32] and [33], by (Copy) 
  23] #argfun-reverse1##*(foldl#(/\x./\y.app-(cons-(y, nil), x), nil, X)) >= /\x./\y.app-(cons-(y, nil), x)  because [24], by (F-Abs) 
  24] #argfun-reverse1##*(foldl#(/\x./\y.app-(cons-(y, nil), x), nil, X), z) >= /\x.app-(cons-(x, nil), z)  because [25], by (F-Abs) 
  25] #argfun-reverse1##*(foldl#(/\x./\y.app-(cons-(y, nil), x), nil, X), z, u) >= app-(cons-(u, nil), z)  because #argfun-reverse1## > app-, [26] and [30], by (Copy) 
  26] #argfun-reverse1##*(foldl#(/\x./\y.app-(cons-(y, nil), x), nil, X), z, u) >= cons-(u, nil)  because #argfun-reverse1## > cons-, [27] and [29], by (Copy) 
  27] #argfun-reverse1##*(foldl#(/\x./\y.app-(cons-(y, nil), x), nil, X), z, u) >= u  because [28], by (Select) 
  28] u >= u  by (Var) 
  29] #argfun-reverse1##*(foldl#(/\x./\y.app-(cons-(y, nil), x), nil, X), z, u) >= nil  because #argfun-reverse1## > nil, by (Copy) 
  30] #argfun-reverse1##*(foldl#(/\x./\y.app-(cons-(y, nil), x), nil, X), z, u) >= z  because [31], by (Select) 
  31] z >= z  by (Var) 
  32] #argfun-reverse1##*(foldl#(/\x./\y.app-(cons-(y, nil), x), nil, X)) >= nil  because #argfun-reverse1## > nil, by (Copy) 
  33] #argfun-reverse1##*(foldl#(/\x./\y.app-(cons-(y, nil), x), nil, X)) >= X  because [34], by (Select) 
  34] foldl#(/\x./\y.app-(cons-(y, nil), x), nil, X) >= X  because [35], by (Star) 
  35] foldl#*(/\x./\y.app-(cons-(y, nil), x), nil, X) >= X  because [36], by (Select) 
  36] X >= X  by (Meta) 

  37] app(nil, X) >= X  because [38], by (Star) 
  38] app*(nil, X) >= X  because [39], by (Select) 
  39] X >= X  by (Meta) 

  40] app(cons(X, Y), Z) >= cons(X, app(Y, Z))  because [41], by (Star) 
  41] app*(cons(X, Y), Z) >= cons(X, app(Y, Z))  because app > cons, [42] and [46], by (Copy) 
  42] app*(cons(X, Y), Z) >= X  because [43], by (Select) 
  43] cons(X, Y) >= X  because [44], by (Star) 
  44] cons*(X, Y) >= X  because [45], by (Select) 
  45] X >= X  by (Meta) 
  46] app*(cons(X, Y), Z) >= app(Y, Z)  because app in Mul, [47] and [50], by (Stat) 
  47] cons(X, Y) > Y  because [48], by definition 
  48] cons*(X, Y) >= Y  because [49], by (Select) 
  49] Y >= Y  by (Meta) 
  50] Z >= Z  by (Meta) 

  51] foldl(F, X, nil) >= X  because [52], by (Star) 
  52] foldl*(F, X, nil) >= X  because [53], by (Select) 
  53] X >= X  by (Meta) 

  54] foldl(F, X, cons(Y, Z)) >= foldl(F, @_{o -> o}(@_{o -> o -> o}(F, X), Y), Z)  because [55], by (Star) 
  55] foldl*(F, X, cons(Y, Z)) >= foldl(F, @_{o -> o}(@_{o -> o -> o}(F, X), Y), Z)  because [56], [57], [60], [61] and [65], by (Stat) 
  56] F >= F  by (Meta) 
  57] cons(Y, Z) > Z  because [58], by definition 
  58] cons*(Y, Z) >= Z  because [59], by (Select) 
  59] Z >= Z  by (Meta) 
  60] foldl*(F, X, cons(Y, Z)) >= F  because [56], by (Select) 
  61] foldl*(F, X, cons(Y, Z)) >= @_{o -> o}(@_{o -> o -> o}(F, X), Y)  because foldl > @_{o -> o}, [62] and [64], by (Copy) 
  62] foldl*(F, X, cons(Y, Z)) >= @_{o -> o -> o}(F, X)  because foldl > @_{o -> o -> o}, [60] and [63], by (Copy) 
  63] foldl*(F, X, cons(Y, Z)) >= X  because [7], by (Select) 
  64] foldl*(F, X, cons(Y, Z)) >= Y  because [9], by (Select) 
  65] foldl*(F, X, cons(Y, Z)) >= Z  because [66], by (Select) 
  66] cons(Y, Z) >= Z  because [58], by (Star) 

  67] foldl(#argfun-iconsc#(/\x./\y.cons(y, x)), nil, X) >= foldl(#argfun-iconsc#(/\x./\y.cons(y, x)), nil, X)  because [13], [19] and [20], by (Fun) 

  68] #argfun-reverse1#(foldl(/\x./\y.app-(cons-(y, nil), x), nil, X)) >= foldl(/\x./\y.app-(cons-(y, nil), x), nil, X)  because [69], by (Star) 
  69] #argfun-reverse1#*(foldl(/\x./\y.app-(cons-(y, nil), x), nil, X)) >= foldl(/\x./\y.app-(cons-(y, nil), x), nil, X)  because #argfun-reverse1# > foldl, [70], [79] and [80], by (Copy) 
  70] #argfun-reverse1#*(foldl(/\x./\y.app-(cons-(y, nil), x), nil, X)) >= /\x./\y.app-(cons-(y, nil), x)  because [71], by (F-Abs) 
  71] #argfun-reverse1#*(foldl(/\x./\y.app-(cons-(y, nil), x), nil, X), z) >= /\x.app-(cons-(x, nil), z)  because [72], by (F-Abs) 
  72] #argfun-reverse1#*(foldl(/\x./\y.app-(cons-(y, nil), x), nil, X), z, u) >= app-(cons-(u, nil), z)  because #argfun-reverse1# > app-, [73] and [77], by (Copy) 
  73] #argfun-reverse1#*(foldl(/\x./\y.app-(cons-(y, nil), x), nil, X), z, u) >= cons-(u, nil)  because #argfun-reverse1# > cons-, [74] and [76], by (Copy) 
  74] #argfun-reverse1#*(foldl(/\x./\y.app-(cons-(y, nil), x), nil, X), z, u) >= u  because [75], by (Select) 
  75] u >= u  by (Var) 
  76] #argfun-reverse1#*(foldl(/\x./\y.app-(cons-(y, nil), x), nil, X), z, u) >= nil  because #argfun-reverse1# > nil, by (Copy) 
  77] #argfun-reverse1#*(foldl(/\x./\y.app-(cons-(y, nil), x), nil, X), z, u) >= z  because [78], by (Select) 
  78] z >= z  by (Var) 
  79] #argfun-reverse1#*(foldl(/\x./\y.app-(cons-(y, nil), x), nil, X)) >= nil  because #argfun-reverse1# > nil, by (Copy) 
  80] #argfun-reverse1#*(foldl(/\x./\y.app-(cons-(y, nil), x), nil, X)) >= X  because [81], by (Select) 
  81] foldl(/\x./\y.app-(cons-(y, nil), x), nil, X) >= X  because [82], by (Star) 
  82] foldl*(/\x./\y.app-(cons-(y, nil), x), nil, X) >= X  because [36], by (Select) 

  83] @_{o -> o}(@_{o -> o -> o}(#argfun-iconsc#(/\x./\y.cons(y, x)), X), Y) >= cons(Y, X)  because [84], by (Star) 
  84] @_{o -> o}*(@_{o -> o -> o}(#argfun-iconsc#(/\x./\y.cons(y, x)), X), Y) >= cons(Y, X)  because @_{o -> o} > cons, [85] and [87], by (Copy) 
  85] @_{o -> o}*(@_{o -> o -> o}(#argfun-iconsc#(/\x./\y.cons(y, x)), X), Y) >= Y  because [86], by (Select) 
  86] Y >= Y  by (Meta) 
  87] @_{o -> o}*(@_{o -> o -> o}(#argfun-iconsc#(/\x./\y.cons(y, x)), X), Y) >= X  because [88], by (Select) 
  88] @_{o -> o -> o}(#argfun-iconsc#(/\x./\y.cons(y, x)), X) @_{o -> o}*(@_{o -> o -> o}(#argfun-iconsc#(/\z./\u.cons(u, z)), X), Y) >= X  because [89] 
  89] @_{o -> o -> o}*(#argfun-iconsc#(/\x./\y.cons(y, x)), X, @_{o -> o}*(@_{o -> o -> o}(#argfun-iconsc#(/\z./\u.cons(u, z)), X), Y)) >= X  because [90], by (Select) 
  90] X >= X  by (Meta) 

  91] app-(X, Y) >= app(X, Y)  because [92], by (Star) 
  92] app-*(X, Y) >= app(X, Y)  because app- > app, [93] and [95], by (Copy) 
  93] app-*(X, Y) >= X  because [94], by (Select) 
  94] X >= X  by (Meta) 
  95] app-*(X, Y) >= Y  because [96], by (Select) 
  96] Y >= Y  by (Meta) 

  97] cons-(X, Y) >= cons(X, Y)  because [98], by (Star) 
  98] cons-*(X, Y) >= cons(X, Y)  because cons- > cons, [99] and [101], by (Copy) 
  99] cons-*(X, Y) >= X  because [100], by (Select) 
  100] X >= X  by (Meta) 
  101] cons-*(X, Y) >= Y  because [102], by (Select) 
  102] Y >= Y  by (Meta) 

By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_3, R_1, minimal, formative) by (P_4, R_1, minimal, formative), where P_4 consists of:

  reverse#(X) =#> foldl#(iconsc, nil, X)   
  reverse1#(X) =#> foldl#(/\x./\y.app(cons(y, nil), x), nil, X)   

Thus, the original system is terminating if each of (P_1, R_0, minimal, formative) and (P_4, R_1, minimal, formative) is finite.

We consider the dependency pair problem (P_4, R_1, minimal, formative).

We place the elements of P in a dependency graph approximation G (see e.g. [Kop12, Thm. 7.27, 7.29], as follows:

    * 0 :  
    * 1 :  

This graph has no strongly connected components.  By [Kop12, Thm. 7.31], this implies finiteness of the dependency pair problem.

Thus, the original system is terminating if (P_1, R_0, minimal, formative) is finite.

We consider the dependency pair problem (P_1, R_0, minimal, formative).

We apply the subterm criterion with the following projection function:

  nu(app#) = 1 

Thus, we can orient the dependency pairs as follows:

  nu(app#(cons(X, Y), Z)) = cons(X, Y) |> Y = nu(app#(Y, Z)) 

By [Kop12, Thm. 7.35], we may replace a dependency pair problem (P_1, R_0, minimal, f) by ({}, R_0, minimal, f).  By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed.

As all dependency pair problems were succesfully simplified with sound (and complete) processors until nothing remained, we conclude termination.


+++ Citations +++

[Kop12]  C. Kop.  Higher Order Termination.  PhD Thesis, 2012.