We consider the system Applicative_05__Ex5Folding.

  Alphabet:

    0 : [] --> c 
    add : [] --> a -> c -> c 
    cons : [a * b] --> b 
    fold : [a -> c -> c * c] --> b -> c 
    mul : [] --> a -> c -> c 
    nil : [] --> b 
    plus : [c * c] --> c 
    prod : [] --> b -> c 
    s : [c] --> c 
    sum : [] --> b -> c 
    times : [c * c] --> c 

  Rules:

    fold(f, x) nil => x 
    fold(f, x) cons(y, z) => f y (fold(f, x) z) 
    plus(0, x) => x 
    plus(s(x), y) => s(plus(x, y)) 
    times(0, x) => 0 
    times(s(x), y) => plus(times(x, y), y) 
    sum => fold(add, 0) 
    prod => fold(mul, s(0)) 

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 static dependency pairs (see [KusIsoSakBla09] and the adaptation for AFSMs and accessible arguments in [Kop13]).

In order to do so, we start by eta-expanding the system, which gives:

  fold(F, X, nil) => X 
  fold(F, X, cons(Y, Z)) => F Y fold(F, X, Z) 
  plus(0, X) => X 
  plus(s(X), Y) => s(plus(X, Y)) 
  times(0, X) => 0 
  times(s(X), Y) => plus(times(X, Y), Y) 
  sum(X) => fold(/\x./\y.add(x, y), 0, X) 
  prod(X) => fold(/\x./\y.mul(x, y), s(0), X) 

We thus obtain the following dependency pair problem (P_0, R_0, static, formative):

  Dependency Pairs P_0:

    0] fold#(F, X, cons(Y, Z)) =#> fold#(F, X, Z)   
    1] plus#(s(X), Y) =#> plus#(X, Y)   
    2] times#(s(X), Y) =#> plus#(times(X, Y), Y)   
    3] times#(s(X), Y) =#> times#(X, Y)   
    4] sum#(X) =#> fold#(/\x./\y.add(x, y), 0, X)   
    5] prod#(X) =#> fold#(/\x./\y.mul(x, y), s(0), X)   

  Rules R_0:

    fold(F, X, nil) => X 
    fold(F, X, cons(Y, Z)) => F Y fold(F, X, Z) 
    plus(0, X) => X 
    plus(s(X), Y) => s(plus(X, Y)) 
    times(0, X) => 0 
    times(s(X), Y) => plus(times(X, Y), Y) 
    sum(X) => fold(/\x./\y.add(x, y), 0, X) 
    prod(X) => fold(/\x./\y.mul(x, y), s(0), X) 

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

We consider the dependency pair problem (P_0, R_0, static, 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 : 1 
    * 3 : 2, 3 
    * 4 : 0 
    * 5 : 0 

This graph has the following strongly connected components:

  P_1:

    fold#(F, X, cons(Y, Z)) =#> fold#(F, X, Z)   

  P_2:

    plus#(s(X), Y) =#> plus#(X, Y)   

  P_3:

    times#(s(X), Y) =#> times#(X, Y)   

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), (P_2, R_0, m, f) and (P_3, R_0, m, f).

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

We consider the dependency pair problem (P_3, R_0, static, formative).

We will use the reduction pair processor [Kop12, Thm. 7.16].  It suffices to find a standard reduction pair [Kop12, Def. 6.69].  Thus, we must orient:

  times#(s(X), Y) >? times#(X, Y) 
  fold(F, X, nil) >= X 
  fold(F, X, cons(Y, Z)) >= F Y fold(F, X, Z) 
  plus(0, X) >= X 
  plus(s(X), Y) >= s(plus(X, Y)) 
  times(0, X) >= 0 
  times(s(X), Y) >= plus(times(X, Y), Y) 
  sum(X) >= fold(/\x./\y.add(x, y), 0, X) 
  prod(X) >= fold(/\x./\y.mul(x, y), s(0), X) 

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

  pi( prod(X) ) = #argfun-prod#(fold(/\x./\y.mul(x, y), s(0), X)) 
  pi( sum(X) ) = #argfun-sum#(fold(/\x./\y.add(x, y), 0, 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-prod#(x_1)]] = x_1 
  [[prod(x_1)]] = x_1 

We choose Lex = {} and Mul = {#argfun-sum#, 0, @_{o -> o -> o}, @_{o -> o}, add, cons, fold, mul, nil, plus, s, sum, times, times#}, and the following precedence: #argfun-sum# > add > times > plus > fold > @_{o -> o -> o} > @_{o -> o} > cons > 0 > times# > s > sum > nil > mul

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

  times#(s(X), Y) > times#(X, Y) 
  fold(F, X, nil) >= X 
  fold(F, X, cons(Y, Z)) >= @_{o -> o}(@_{o -> o -> o}(F, Y), fold(F, X, Z)) 
  plus(0, X) >= X 
  plus(s(X), Y) >= s(plus(X, Y)) 
  times(0, X) >= 0 
  times(s(X), Y) >= plus(times(X, Y), Y) 
  #argfun-sum#(fold(/\x./\y.add(x, y), 0, X)) >= fold(/\x./\y.add(x, y), 0, X) 
  fold(/\x./\y.mul(x, y), s(0), X) >= fold(/\x./\y.mul(x, y), s(0), X) 

With these choices, we have:

  1] times#(s(X), Y) > times#(X, Y)  because [2], by definition 
  2] times#*(s(X), Y) >= times#(X, Y)  because times# in Mul, [3] and [6], by (Stat) 
  3] s(X) > X  because [4], by definition 
  4] s*(X) >= X  because [5], by (Select) 
  5] X >= X  by (Meta) 
  6] Y >= Y  by (Meta) 

  7] fold(F, X, nil) >= X  because [8], by (Star) 
  8] fold*(F, X, nil) >= X  because [9], by (Select) 
  9] X >= X  by (Meta) 

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

  25] plus(0, X) >= X  because [26], by (Star) 
  26] plus*(0, X) >= X  because [27], by (Select) 
  27] X >= X  by (Meta) 

  28] plus(s(X), Y) >= s(plus(X, Y))  because [29], by (Star) 
  29] plus*(s(X), Y) >= s(plus(X, Y))  because plus > s and [30], by (Copy) 
  30] plus*(s(X), Y) >= plus(X, Y)  because plus in Mul, [31] and [34], by (Stat) 
  31] s(X) > X  because [32], by definition 
  32] s*(X) >= X  because [33], by (Select) 
  33] X >= X  by (Meta) 
  34] Y >= Y  by (Meta) 

  35] times(0, X) >= 0  because [36], by (Star) 
  36] times*(0, X) >= 0  because times > 0, by (Copy) 

  37] times(s(X), Y) >= plus(times(X, Y), Y)  because [38], by (Star) 
  38] times*(s(X), Y) >= plus(times(X, Y), Y)  because times > plus, [39] and [40], by (Copy) 
  39] times*(s(X), Y) >= times(X, Y)  because times in Mul, [3] and [6], by (Stat) 
  40] times*(s(X), Y) >= Y  because [6], by (Select) 

  41] #argfun-sum#(fold(/\x./\y.add(x, y), 0, X)) >= fold(/\x./\y.add(x, y), 0, X)  because [42], by (Star) 
  42] #argfun-sum#*(fold(/\x./\y.add(x, y), 0, X)) >= fold(/\x./\y.add(x, y), 0, X)  because #argfun-sum# > fold, [43], [50] and [51], by (Copy) 
  43] #argfun-sum#*(fold(/\x./\y.add(x, y), 0, X)) >= /\x./\y.add(x, y)  because [44], by (F-Abs) 
  44] #argfun-sum#*(fold(/\x./\y.add(x, y), 0, X), z) >= /\x.add(z, x)  because [45], by (F-Abs) 
  45] #argfun-sum#*(fold(/\x./\y.add(x, y), 0, X), z, u) >= add(z, u)  because #argfun-sum# > add, [46] and [48], by (Copy) 
  46] #argfun-sum#*(fold(/\x./\y.add(x, y), 0, X), z, u) >= z  because [47], by (Select) 
  47] z >= z  by (Var) 
  48] #argfun-sum#*(fold(/\x./\y.add(x, y), 0, X), z, u) >= u  because [49], by (Select) 
  49] u >= u  by (Var) 
  50] #argfun-sum#*(fold(/\x./\y.add(x, y), 0, X)) >= 0  because #argfun-sum# > 0, by (Copy) 
  51] #argfun-sum#*(fold(/\x./\y.add(x, y), 0, X)) >= X  because [52], by (Select) 
  52] fold(/\x./\y.add(x, y), 0, X) >= X  because [53], by (Star) 
  53] fold*(/\x./\y.add(x, y), 0, X) >= X  because [54], by (Select) 
  54] X >= X  by (Meta) 

  55] fold(/\x./\y.mul(x, y), s(0), X) >= fold(/\x./\y.mul(x, y), s(0), X)  because fold in Mul, [56], [61] and [63], by (Fun) 
  56] /\x./\z.mul(x, z) >= /\x./\z.mul(x, z)  because [57], by (Abs) 
  57] /\z.mul(y, z) >= /\z.mul(y, z)  because [58], by (Abs) 
  58] mul(y, x) >= mul(y, x)  because mul in Mul, [59] and [60], by (Fun) 
  59] y >= y  by (Var) 
  60] x >= x  by (Var) 
  61] s(0) >= s(0)  because s in Mul and [62], by (Fun) 
  62] 0 >= 0  by (Fun) 
  63] X >= X  by (Meta) 

By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_3, R_0) by ({}, R_0).  By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed.

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

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

We will use the reduction pair processor [Kop12, Thm. 7.16].  It suffices to find a standard reduction pair [Kop12, Def. 6.69].  Thus, we must orient:

  plus#(s(X), Y) >? plus#(X, Y) 
  fold(F, X, nil) >= X 
  fold(F, X, cons(Y, Z)) >= F Y fold(F, X, Z) 
  plus(0, X) >= X 
  plus(s(X), Y) >= s(plus(X, Y)) 
  times(0, X) >= 0 
  times(s(X), Y) >= plus(times(X, Y), Y) 
  sum(X) >= fold(/\x./\y.add(x, y), 0, X) 
  prod(X) >= fold(/\x./\y.mul(x, y), s(0), X) 

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

  pi( prod(X) ) = #argfun-prod#(fold(/\x./\y.mul(x, y), s(0), X)) 
  pi( sum(X) ) = #argfun-sum#(fold(/\x./\y.add(x, y), 0, 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:

  [[prod(x_1)]] = x_1 
  [[sum(x_1)]] = x_1 

We choose Lex = {plus#} and Mul = {#argfun-prod#, #argfun-sum#, 0, @_{o -> o -> o}, @_{o -> o}, add, cons, fold, mul, nil, plus, s, times}, and the following precedence: #argfun-prod# > cons > mul > nil > plus# > #argfun-sum# > add > 0 = times > plus > s > @_{o -> o -> o} = fold > @_{o -> o}

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

  plus#(s(X), Y) > plus#(X, Y) 
  fold(F, X, nil) >= X 
  fold(F, X, cons(Y, Z)) >= @_{o -> o}(@_{o -> o -> o}(F, Y), fold(F, X, Z)) 
  plus(0, X) >= X 
  plus(s(X), Y) >= s(plus(X, Y)) 
  times(0, X) >= 0 
  times(s(X), Y) >= plus(times(X, Y), Y) 
  #argfun-sum#(fold(/\x./\y.add(x, y), 0, X)) >= fold(/\x./\y.add(x, y), 0, X) 
  #argfun-prod#(fold(/\x./\y.mul(x, y), s(0), X)) >= fold(/\x./\y.mul(x, y), s(0), X) 

With these choices, we have:

  1] plus#(s(X), Y) > plus#(X, Y)  because [2], by definition 
  2] plus#*(s(X), Y) >= plus#(X, Y)  because [3], [6] and [8], by (Stat) 
  3] s(X) > X  because [4], by definition 
  4] s*(X) >= X  because [5], by (Select) 
  5] X >= X  by (Meta) 
  6] plus#*(s(X), Y) >= X  because [7], by (Select) 
  7] s(X) >= X  because [4], by (Star) 
  8] plus#*(s(X), Y) >= Y  because [9], by (Select) 
  9] Y >= Y  by (Meta) 

  10] fold(F, X, nil) >= X  because [11], by (Star) 
  11] fold*(F, X, nil) >= X  because [12], by (Select) 
  12] X >= X  by (Meta) 

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

  25] plus(0, X) >= X  because [26], by (Star) 
  26] plus*(0, X) >= X  because [27], by (Select) 
  27] X >= X  by (Meta) 

  28] plus(s(X), Y) >= s(plus(X, Y))  because [29], by (Star) 
  29] plus*(s(X), Y) >= s(plus(X, Y))  because plus > s and [30], by (Copy) 
  30] plus*(s(X), Y) >= plus(X, Y)  because plus in Mul, [3] and [31], by (Stat) 
  31] Y >= Y  by (Meta) 

  32] times(0, X) >= 0  because [33], by (Star) 
  33] times*(0, X) >= 0  because times = 0 and times in Mul, by (Stat) 

  34] times(s(X), Y) >= plus(times(X, Y), Y)  because [35], by (Star) 
  35] times*(s(X), Y) >= plus(times(X, Y), Y)  because times > plus, [36] and [41], by (Copy) 
  36] times*(s(X), Y) >= times(X, Y)  because times in Mul, [37] and [40], by (Stat) 
  37] s(X) > X  because [38], by definition 
  38] s*(X) >= X  because [39], by (Select) 
  39] X >= X  by (Meta) 
  40] Y >= Y  by (Meta) 
  41] times*(s(X), Y) >= Y  because [40], by (Select) 

  42] #argfun-sum#(fold(/\x./\y.add(x, y), 0, X)) >= fold(/\x./\y.add(x, y), 0, X)  because [43], by (Star) 
  43] #argfun-sum#*(fold(/\x./\y.add(x, y), 0, X)) >= fold(/\x./\y.add(x, y), 0, X)  because #argfun-sum# > fold, [44], [51] and [52], by (Copy) 
  44] #argfun-sum#*(fold(/\x./\y.add(x, y), 0, X)) >= /\x./\y.add(x, y)  because [45], by (F-Abs) 
  45] #argfun-sum#*(fold(/\x./\y.add(x, y), 0, X), z) >= /\x.add(z, x)  because [46], by (F-Abs) 
  46] #argfun-sum#*(fold(/\x./\y.add(x, y), 0, X), z, u) >= add(z, u)  because #argfun-sum# > add, [47] and [49], by (Copy) 
  47] #argfun-sum#*(fold(/\x./\y.add(x, y), 0, X), z, u) >= z  because [48], by (Select) 
  48] z >= z  by (Var) 
  49] #argfun-sum#*(fold(/\x./\y.add(x, y), 0, X), z, u) >= u  because [50], by (Select) 
  50] u >= u  by (Var) 
  51] #argfun-sum#*(fold(/\x./\y.add(x, y), 0, X)) >= 0  because #argfun-sum# > 0, by (Copy) 
  52] #argfun-sum#*(fold(/\x./\y.add(x, y), 0, X)) >= X  because [53], by (Select) 
  53] fold(/\x./\y.add(x, y), 0, X) >= X  because [54], by (Star) 
  54] fold*(/\x./\y.add(x, y), 0, X) >= X  because [55], by (Select) 
  55] X >= X  by (Meta) 

  56] #argfun-prod#(fold(/\x./\y.mul(x, y), s(0), X)) >= fold(/\x./\y.mul(x, y), s(0), X)  because [57], by (Star) 
  57] #argfun-prod#*(fold(/\x./\y.mul(x, y), s(0), X)) >= fold(/\x./\y.mul(x, y), s(0), X)  because #argfun-prod# > fold, [58], [65] and [67], by (Copy) 
  58] #argfun-prod#*(fold(/\x./\y.mul(x, y), s(0), X)) >= /\x./\y.mul(x, y)  because [59], by (F-Abs) 
  59] #argfun-prod#*(fold(/\x./\y.mul(x, y), s(0), X), z) >= /\x.mul(z, x)  because [60], by (F-Abs) 
  60] #argfun-prod#*(fold(/\x./\y.mul(x, y), s(0), X), z, u) >= mul(z, u)  because #argfun-prod# > mul, [61] and [63], by (Copy) 
  61] #argfun-prod#*(fold(/\x./\y.mul(x, y), s(0), X), z, u) >= z  because [62], by (Select) 
  62] z >= z  by (Var) 
  63] #argfun-prod#*(fold(/\x./\y.mul(x, y), s(0), X), z, u) >= u  because [64], by (Select) 
  64] u >= u  by (Var) 
  65] #argfun-prod#*(fold(/\x./\y.mul(x, y), s(0), X)) >= s(0)  because #argfun-prod# > s and [66], by (Copy) 
  66] #argfun-prod#*(fold(/\x./\y.mul(x, y), s(0), X)) >= 0  because #argfun-prod# > 0, by (Copy) 
  67] #argfun-prod#*(fold(/\x./\y.mul(x, y), s(0), X)) >= X  because [68], by (Select) 
  68] fold(/\x./\y.mul(x, y), s(0), X) >= X  because [69], by (Star) 
  69] fold*(/\x./\y.mul(x, y), s(0), X) >= X  because [70], by (Select) 
  70] X >= X  by (Meta) 

By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_2, R_0) by ({}, R_0).  By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed.

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

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

We will use the reduction pair processor [Kop12, Thm. 7.16].  It suffices to find a standard reduction pair [Kop12, Def. 6.69].  Thus, we must orient:

  fold#(F, X, cons(Y, Z)) >? fold#(F, X, Z) 
  fold(F, X, nil) >= X 
  fold(F, X, cons(Y, Z)) >= F Y fold(F, X, Z) 
  plus(0, X) >= X 
  plus(s(X), Y) >= s(plus(X, Y)) 
  times(0, X) >= 0 
  times(s(X), Y) >= plus(times(X, Y), Y) 
  sum(X) >= fold(/\x./\y.add(x, y), 0, X) 
  prod(X) >= fold(/\x./\y.mul(x, y), s(0), X) 

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

  pi( prod(X) ) = #argfun-prod#(fold(/\x./\y.mul(x, y), s(0), X)) 
  pi( sum(X) ) = #argfun-sum#(fold(/\x./\y.add(x, y), 0, 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:

  [[0]] = _|_ 
  [[plus(x_1, x_2)]] = x_2 
  [[prod(x_1)]] = x_1 
  [[s(x_1)]] = x_1 
  [[sum(x_1)]] = x_1 

We choose Lex = {} and Mul = {#argfun-prod#, #argfun-sum#, @_{o -> o -> o}, @_{o -> o}, add, cons, fold, fold#, mul, nil, times}, and the following precedence: #argfun-prod# > #argfun-sum# > fold# > mul > fold > @_{o -> o -> o} > @_{o -> o} > nil > add > cons > times

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

  fold#(F, X, cons(Y, Z)) > fold#(F, X, Z) 
  fold(F, X, nil) >= X 
  fold(F, X, cons(Y, Z)) >= @_{o -> o}(@_{o -> o -> o}(F, Y), fold(F, X, Z)) 
  X >= X 
  X >= X 
  times(_|_, X) >= _|_ 
  times(X, Y) >= Y 
  #argfun-sum#(fold(/\x./\y.add(x, y), _|_, X)) >= fold(/\x./\y.add(x, y), _|_, X) 
  #argfun-prod#(fold(/\x./\y.mul(x, y), _|_, X)) >= fold(/\x./\y.mul(x, y), _|_, X) 

With these choices, we have:

  1] fold#(F, X, cons(Y, Z)) > fold#(F, X, Z)  because [2], by definition 
  2] fold#*(F, X, cons(Y, Z)) >= fold#(F, X, Z)  because fold# in Mul, [3], [4] and [5], by (Stat) 
  3] F >= F  by (Meta) 
  4] X >= X  by (Meta) 
  5] cons(Y, Z) > Z  because [6], by definition 
  6] cons*(Y, Z) >= Z  because [7], by (Select) 
  7] Z >= Z  by (Meta) 

  8] fold(F, X, nil) >= X  because [9], by (Star) 
  9] fold*(F, X, nil) >= X  because [10], by (Select) 
  10] X >= X  by (Meta) 

  11] fold(F, X, cons(Y, Z)) >= @_{o -> o}(@_{o -> o -> o}(F, Y), fold(F, X, Z))  because [12], by (Star) 
  12] fold*(F, X, cons(Y, Z)) >= @_{o -> o}(@_{o -> o -> o}(F, Y), fold(F, X, Z))  because fold > @_{o -> o}, [13] and [19], by (Copy) 
  13] fold*(F, X, cons(Y, Z)) >= @_{o -> o -> o}(F, Y)  because fold > @_{o -> o -> o}, [14] and [15], by (Copy) 
  14] fold*(F, X, cons(Y, Z)) >= F  because [3], by (Select) 
  15] fold*(F, X, cons(Y, Z)) >= Y  because [16], by (Select) 
  16] cons(Y, Z) >= Y  because [17], by (Star) 
  17] cons*(Y, Z) >= Y  because [18], by (Select) 
  18] Y >= Y  by (Meta) 
  19] fold*(F, X, cons(Y, Z)) >= fold(F, X, Z)  because fold in Mul, [3], [4] and [5], by (Stat) 

  20] X >= X  by (Meta) 

  21] X >= X  by (Meta) 

  22] times(_|_, X) >= _|_  by (Bot) 

  23] times(X, Y) >= Y  because [24], by (Star) 
  24] times*(X, Y) >= Y  because [25], by (Select) 
  25] Y >= Y  by (Meta) 

  26] #argfun-sum#(fold(/\x./\y.add(x, y), _|_, X)) >= fold(/\x./\y.add(x, y), _|_, X)  because [27], by (Star) 
  27] #argfun-sum#*(fold(/\x./\y.add(x, y), _|_, X)) >= fold(/\x./\y.add(x, y), _|_, X)  because #argfun-sum# > fold, [28], [35] and [36], by (Copy) 
  28] #argfun-sum#*(fold(/\x./\y.add(x, y), _|_, X)) >= /\x./\y.add(x, y)  because [29], by (F-Abs) 
  29] #argfun-sum#*(fold(/\x./\y.add(x, y), _|_, X), z) >= /\x.add(z, x)  because [30], by (F-Abs) 
  30] #argfun-sum#*(fold(/\x./\y.add(x, y), _|_, X), z, u) >= add(z, u)  because #argfun-sum# > add, [31] and [33], by (Copy) 
  31] #argfun-sum#*(fold(/\x./\y.add(x, y), _|_, X), z, u) >= z  because [32], by (Select) 
  32] z >= z  by (Var) 
  33] #argfun-sum#*(fold(/\x./\y.add(x, y), _|_, X), z, u) >= u  because [34], by (Select) 
  34] u >= u  by (Var) 
  35] #argfun-sum#*(fold(/\x./\y.add(x, y), _|_, X)) >= _|_  by (Bot) 
  36] #argfun-sum#*(fold(/\x./\y.add(x, y), _|_, X)) >= X  because [37], by (Select) 
  37] fold(/\x./\y.add(x, y), _|_, X) >= X  because [38], by (Star) 
  38] fold*(/\x./\y.add(x, y), _|_, X) >= X  because [39], by (Select) 
  39] X >= X  by (Meta) 

  40] #argfun-prod#(fold(/\x./\y.mul(x, y), _|_, X)) >= fold(/\x./\y.mul(x, y), _|_, X)  because [41], by (Star) 
  41] #argfun-prod#*(fold(/\x./\y.mul(x, y), _|_, X)) >= fold(/\x./\y.mul(x, y), _|_, X)  because #argfun-prod# > fold, [42], [49] and [50], by (Copy) 
  42] #argfun-prod#*(fold(/\x./\y.mul(x, y), _|_, X)) >= /\x./\y.mul(x, y)  because [43], by (F-Abs) 
  43] #argfun-prod#*(fold(/\x./\y.mul(x, y), _|_, X), z) >= /\x.mul(z, x)  because [44], by (F-Abs) 
  44] #argfun-prod#*(fold(/\x./\y.mul(x, y), _|_, X), z, u) >= mul(z, u)  because #argfun-prod# > mul, [45] and [47], by (Copy) 
  45] #argfun-prod#*(fold(/\x./\y.mul(x, y), _|_, X), z, u) >= z  because [46], by (Select) 
  46] z >= z  by (Var) 
  47] #argfun-prod#*(fold(/\x./\y.mul(x, y), _|_, X), z, u) >= u  because [48], by (Select) 
  48] u >= u  by (Var) 
  49] #argfun-prod#*(fold(/\x./\y.mul(x, y), _|_, X)) >= _|_  by (Bot) 
  50] #argfun-prod#*(fold(/\x./\y.mul(x, y), _|_, X)) >= X  because [51], by (Select) 
  51] fold(/\x./\y.mul(x, y), _|_, X) >= X  because [52], by (Star) 
  52] fold*(/\x./\y.mul(x, y), _|_, X) >= X  because [53], by (Select) 
  53] X >= X  by (Meta) 

By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_1, R_0) by ({}, R_0).  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.
[Kop13]  C. Kop.  Static Dependency Pairs with Accessibility.  Unpublished manuscript, http://cl-informatik.uibk.ac.at/users/kop/static.pdf, 2013.
[KusIsoSakBla09]  K. Kusakari, Y. Isogai, M. Sakai, and F. Blanqui.  Static Dependency Pair Method Based On Strong Computability for Higher-Order Rewrite Systems.  In volume 92(10) of IEICE Transactions on Information and Systems.  2007--2015, 2009.