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 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) 
  plus#(s(X), Y) >? plus#(X, Y) 
  times#(s(X), Y) >? plus#(times(X, Y), Y) 
  times#(s(X), Y) >? times#(X, Y) 
  sum#(X) >? fold#(/\x./\y.add(x, y), 0, X) 
  prod#(X) >? fold#(/\x./\y.mul(x, y), s(0), X) 
  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( 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)) 
  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]] = _|_ 
  [[fold#(x_1, x_2, x_3)]] = fold#(x_2) 
  [[plus#(x_1, x_2)]] = _|_ 
  [[prod(x_1)]] = x_1 
  [[prod#(x_1)]] = prod# 
  [[sum(x_1)]] = x_1 
  [[times#(x_1, x_2)]] = x_1 

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

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

  fold#(X) >= fold#(X) 
  _|_ >= _|_ 
  s(X) >= _|_ 
  s(X) > X 
  #argfun-sum##(fold#(_|_)) >= fold#(_|_) 
  #argfun-prod##(fold#(s(_|_))) >= fold#(s(_|_)) 
  fold(F, X, nil) >= X 
  fold(F, X, cons(Y, Z)) >= @_{o -> o}(@_{o -> o -> o}(F, Y), fold(F, X, Z)) 
  plus(_|_, X) >= X 
  plus(s(X), Y) >= s(plus(X, Y)) 
  times(_|_, X) >= _|_ 
  times(s(X), Y) >= plus(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), s(_|_), X)) >= fold(/\x./\y.mul(x, y), s(_|_), X) 

With these choices, we have:

  1] fold#(X) >= fold#(X)  because fold# in Mul and [2], by (Fun) 
  2] X >= X  by (Meta) 

  3] _|_ >= _|_  by (Bot) 

  4] s(X) >= _|_  by (Bot) 

  5] s(X) > X  because [6], by definition 
  6] s*(X) >= X  because [7], by (Select) 
  7] X >= X  by (Meta) 

  8] #argfun-sum##(fold#(_|_)) >= fold#(_|_)  because #argfun-sum## = fold#, #argfun-sum## in Mul and [9], by (Fun) 
  9] fold#(_|_) >= _|_  by (Bot) 

  10] #argfun-prod##(fold#(s(_|_))) >= fold#(s(_|_))  because [11], by (Star) 
  11] #argfun-prod##*(fold#(s(_|_))) >= fold#(s(_|_))  because [12], by (Select) 
  12] fold#(s(_|_)) >= fold#(s(_|_))  because fold# in Mul and [13], by (Fun) 
  13] s(_|_) >= s(_|_)  because s in Mul and [14], by (Fun) 
  14] _|_ >= _|_  by (Bot) 

  15] fold(F, X, nil) >= X  because [16], by (Star) 
  16] fold*(F, X, nil) >= X  because [17], by (Select) 
  17] X >= X  by (Meta) 

  18] fold(F, X, cons(Y, Z)) >= @_{o -> o}(@_{o -> o -> o}(F, Y), fold(F, X, Z))  because [19], by (Star) 
  19] fold*(F, X, cons(Y, Z)) >= @_{o -> o}(@_{o -> o -> o}(F, Y), fold(F, X, Z))  because fold > @_{o -> o}, [20] and [27], by (Copy) 
  20] fold*(F, X, cons(Y, Z)) >= @_{o -> o -> o}(F, Y)  because fold > @_{o -> o -> o}, [21] and [23], by (Copy) 
  21] fold*(F, X, cons(Y, Z)) >= F  because [22], by (Select) 
  22] F >= F  by (Meta) 
  23] fold*(F, X, cons(Y, Z)) >= Y  because [24], by (Select) 
  24] cons(Y, Z) >= Y  because [25], by (Star) 
  25] cons*(Y, Z) >= Y  because [26], by (Select) 
  26] Y >= Y  by (Meta) 
  27] fold*(F, X, cons(Y, Z)) >= fold(F, X, Z)  because fold in Mul, [28], [2] and [29], by (Stat) 
  28] F >= F  by (Meta) 
  29] cons(Y, Z) > Z  because [30], by definition 
  30] cons*(Y, Z) >= Z  because [31], by (Select) 
  31] Z >= Z  by (Meta) 

  32] plus(_|_, X) >= X  because [33], by (Star) 
  33] plus*(_|_, X) >= X  because [34], by (Select) 
  34] X >= X  by (Meta) 

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

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

  43] times(s(X), Y) >= plus(times(X, Y), Y)  because [44], by (Star) 
  44] times*(s(X), Y) >= plus(times(X, Y), Y)  because times > plus, [45] and [48], by (Copy) 
  45] times*(s(X), Y) >= times(X, Y)  because times in Mul, [46] and [47], by (Stat) 
  46] s(X) > X  because [6], by definition 
  47] Y >= Y  by (Meta) 
  48] times*(s(X), Y) >= Y  because [47], by (Select) 

  49] #argfun-sum#(fold(/\x./\y.add(x, y), _|_, X)) >= fold(/\x./\y.add(x, y), _|_, X)  because [50], by (Star) 
  50] #argfun-sum#*(fold(/\x./\y.add(x, y), _|_, X)) >= fold(/\x./\y.add(x, y), _|_, X)  because #argfun-sum# > fold, [51], [58] and [59], by (Copy) 
  51] #argfun-sum#*(fold(/\x./\y.add(x, y), _|_, X)) >= /\x./\y.add(x, y)  because [52], by (F-Abs) 
  52] #argfun-sum#*(fold(/\x./\y.add(x, y), _|_, X), z) >= /\x.add(z, x)  because [53], by (F-Abs) 
  53] #argfun-sum#*(fold(/\x./\y.add(x, y), _|_, X), z, u) >= add(z, u)  because #argfun-sum# > add, [54] and [56], by (Copy) 
  54] #argfun-sum#*(fold(/\x./\y.add(x, y), _|_, X), z, u) >= z  because [55], by (Select) 
  55] z >= z  by (Var) 
  56] #argfun-sum#*(fold(/\x./\y.add(x, y), _|_, X), z, u) >= u  because [57], by (Select) 
  57] u >= u  by (Var) 
  58] #argfun-sum#*(fold(/\x./\y.add(x, y), _|_, X)) >= _|_  by (Bot) 
  59] #argfun-sum#*(fold(/\x./\y.add(x, y), _|_, X)) >= X  because [60], by (Select) 
  60] fold(/\x./\y.add(x, y), _|_, X) >= X  because [61], by (Star) 
  61] fold*(/\x./\y.add(x, y), _|_, X) >= X  because [62], by (Select) 
  62] X >= X  by (Meta) 

  63] #argfun-prod#(fold(/\x./\y.mul(x, y), s(_|_), X)) >= fold(/\x./\y.mul(x, y), s(_|_), X)  because [64], by (Star) 
  64] #argfun-prod#*(fold(/\x./\y.mul(x, y), s(_|_), X)) >= fold(/\x./\y.mul(x, y), s(_|_), X)  because [65], by (Select) 
  65] fold(/\x./\y.mul(x, y), s(_|_), X) >= fold(/\x./\y.mul(x, y), s(_|_), X)  because fold in Mul, [66], [13] and [71], by (Fun) 
  66] /\x./\z.mul(x, z) >= /\x./\z.mul(x, z)  because [67], by (Abs) 
  67] /\z.mul(y, z) >= /\z.mul(y, z)  because [68], by (Abs) 
  68] mul(y, x) >= mul(y, x)  because mul in Mul, [69] and [70], by (Fun) 
  69] y >= y  by (Var) 
  70] x >= x  by (Var) 
  71] X >= X  by (Meta) 

By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_0, R_0, static, formative) by (P_1, R_0, static, formative), where P_1 consists of:

  fold#(F, X, cons(Y, Z)) =#> fold#(F, X, Z)   
  plus#(s(X), Y) =#> plus#(X, Y)   
  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_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) 
  plus#(s(X), Y) >? plus#(X, Y) 
  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) 
  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( 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)) 
  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 
  [[#argfun-sum#(x_1)]] = x_1 
  [[0]] = _|_ 
  [[prod(x_1)]] = x_1 
  [[prod#(x_1)]] = x_1 
  [[sum(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, plus, plus#, s, times, times#}, and the following precedence: #argfun-sum## > cons > mul > add > fold > @_{o -> o} > #argfun-prod## > times# > nil > fold# > times > @_{o -> o -> o} > plus# > plus > s

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) 
  plus#(s(X), Y) >= plus#(X, Y) 
  times#(s(X), Y) >= plus#(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), s(_|_), X)) >= fold#(/\x./\y.mul(x, y), s(_|_), X) 
  fold(F, X, nil) >= X 
  fold(F, X, cons(Y, Z)) >= @_{o -> o}(@_{o -> o -> o}(F, Y), fold(F, X, Z)) 
  plus(_|_, X) >= X 
  plus(s(X), Y) >= s(plus(X, Y)) 
  times(_|_, X) >= _|_ 
  times(s(X), Y) >= plus(times(X, Y), Y) 
  fold(/\x./\y.add(x, y), _|_, X) >= fold(/\x./\y.add(x, y), _|_, X) 
  fold(/\x./\y.mul(x, y), s(_|_), X) >= fold(/\x./\y.mul(x, y), s(_|_), X) 

With these choices, we have:

  1] fold#(F, X, cons(Y, Z)) >= fold#(F, X, Z)  because [2], by (Star) 
  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] plus#(s(X), Y) >= plus#(X, Y)  because plus# in Mul, [9] and [12], by (Fun) 
  9] s(X) >= X  because [10], by (Star) 
  10] s*(X) >= X  because [11], by (Select) 
  11] X >= X  by (Meta) 
  12] Y >= Y  by (Meta) 

  13] times#(s(X), Y) >= plus#(times(X, Y), Y)  because [14], by (Star) 
  14] times#*(s(X), Y) >= plus#(times(X, Y), Y)  because times# > plus#, [15] and [20], by (Copy) 
  15] times#*(s(X), Y) >= times(X, Y)  because times# > times, [16] and [20], by (Copy) 
  16] times#*(s(X), Y) >= X  because [17], by (Select) 
  17] s(X) >= X  because [18], by (Star) 
  18] s*(X) >= X  because [19], by (Select) 
  19] X >= X  by (Meta) 
  20] times#*(s(X), Y) >= Y  because [21], by (Select) 
  21] Y >= Y  by (Meta) 

  22] #argfun-sum##(fold#(/\x./\y.add(x, y), _|_, X)) > fold#(/\x./\y.add(x, y), _|_, X)  because [23], by definition 
  23] #argfun-sum##*(fold#(/\x./\y.add(x, y), _|_, X)) >= fold#(/\x./\y.add(x, y), _|_, X)  because [24], by (Select) 
  24] fold#(/\x./\y.add(x, y), _|_, X) >= fold#(/\x./\y.add(x, y), _|_, X)  because fold# in Mul, [25], [30] and [31], by (Fun) 
  25] /\x./\z.add(x, z) >= /\x./\z.add(x, z)  because [26], by (Abs) 
  26] /\z.add(y, z) >= /\z.add(y, z)  because [27], by (Abs) 
  27] add(y, x) >= add(y, x)  because add in Mul, [28] and [29], by (Fun) 
  28] y >= y  by (Var) 
  29] x >= x  by (Var) 
  30] _|_ >= _|_  by (Bot) 
  31] X >= X  by (Meta) 

  32] #argfun-prod##(fold#(/\x./\y.mul(x, y), s(_|_), X)) >= fold#(/\x./\y.mul(x, y), s(_|_), X)  because [33], by (Star) 
  33] #argfun-prod##*(fold#(/\x./\y.mul(x, y), s(_|_), X)) >= fold#(/\x./\y.mul(x, y), s(_|_), X)  because [34], by (Select) 
  34] fold#(/\x./\y.mul(x, y), s(_|_), X) >= fold#(/\x./\y.mul(x, y), s(_|_), X)  because fold# in Mul, [35], [40] and [41], by (Fun) 
  35] /\x./\z.mul(x, z) >= /\x./\z.mul(x, z)  because [36], by (Abs) 
  36] /\z.mul(y, z) >= /\z.mul(y, z)  because [37], by (Abs) 
  37] mul(y, x) >= mul(y, x)  because mul in Mul, [38] and [39], by (Fun) 
  38] y >= y  by (Var) 
  39] x >= x  by (Var) 
  40] s(_|_) >= s(_|_)  because s in Mul and [30], by (Fun) 
  41] X >= X  by (Meta) 

  42] fold(F, X, nil) >= X  because [43], by (Star) 
  43] fold*(F, X, nil) >= X  because [44], by (Select) 
  44] X >= X  by (Meta) 

  45] fold(F, X, cons(Y, Z)) >= @_{o -> o}(@_{o -> o -> o}(F, Y), fold(F, X, Z))  because [46], by (Star) 
  46] fold*(F, X, cons(Y, Z)) >= @_{o -> o}(@_{o -> o -> o}(F, Y), fold(F, X, Z))  because fold > @_{o -> o}, [47] and [53], by (Copy) 
  47] fold*(F, X, cons(Y, Z)) >= @_{o -> o -> o}(F, Y)  because fold > @_{o -> o -> o}, [48] and [49], by (Copy) 
  48] fold*(F, X, cons(Y, Z)) >= F  because [3], by (Select) 
  49] fold*(F, X, cons(Y, Z)) >= Y  because [50], by (Select) 
  50] cons(Y, Z) >= Y  because [51], by (Star) 
  51] cons*(Y, Z) >= Y  because [52], by (Select) 
  52] Y >= Y  by (Meta) 
  53] fold*(F, X, cons(Y, Z)) >= fold(F, X, Z)  because fold in Mul, [3], [4] and [5], by (Stat) 

  54] plus(_|_, X) >= X  because [55], by (Star) 
  55] plus*(_|_, X) >= X  because [56], by (Select) 
  56] X >= X  by (Meta) 

  57] plus(s(X), Y) >= s(plus(X, Y))  because [58], by (Star) 
  58] plus*(s(X), Y) >= s(plus(X, Y))  because plus > s and [59], by (Copy) 
  59] plus*(s(X), Y) >= plus(X, Y)  because plus in Mul, [60] and [12], by (Stat) 
  60] s(X) > X  because [61], by definition 
  61] s*(X) >= X  because [11], by (Select) 

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

  63] times(s(X), Y) >= plus(times(X, Y), Y)  because [64], by (Star) 
  64] times*(s(X), Y) >= plus(times(X, Y), Y)  because times > plus, [65] and [69], by (Copy) 
  65] times*(s(X), Y) >= times(X, Y)  because times in Mul, [66] and [68], by (Stat) 
  66] s(X) > X  because [67], by definition 
  67] s*(X) >= X  because [19], by (Select) 
  68] Y >= Y  by (Meta) 
  69] times*(s(X), Y) >= Y  because [68], by (Select) 

  70] fold(/\x./\y.add(x, y), _|_, X) >= fold(/\x./\y.add(x, y), _|_, X)  because fold in Mul, [25], [30] and [31], by (Fun) 

  71] fold(/\x./\y.mul(x, y), s(_|_), X) >= fold(/\x./\y.mul(x, y), s(_|_), X)  because fold in Mul, [35], [40] and [41], by (Fun) 

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

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

Thus, the original system is terminating if (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:

  fold#(F, X, cons(Y, Z)) >? fold#(F, X, Z) 
  plus#(s(X), Y) >? plus#(X, Y) 
  times#(s(X), Y) >? plus#(times(X, Y), Y) 
  prod#(X) >? fold#(/\x./\y.mul(x, y), s(0), X) 
  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( 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 
  [[0]] = _|_ 
  [[add(x_1, x_2)]] = x_2 
  [[fold#(x_1, x_2, x_3)]] = fold#(x_3, x_2, x_1) 
  [[mul(x_1, x_2)]] = mul(x_1) 
  [[prod(x_1)]] = x_1 
  [[prod#(x_1)]] = x_1 
  [[sum(x_1)]] = x_1 

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

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) 
  plus#(s(X), Y) >= plus#(X, Y) 
  times#(s(X), Y) > plus#(times(X, Y), Y) 
  fold#(/\x./\y.mul(x), s(_|_), X) >= fold#(/\x./\y.mul(x), s(_|_), X) 
  fold(F, X, nil) >= X 
  fold(F, X, cons(Y, Z)) >= @_{o -> o}(@_{o -> o -> o}(F, Y), fold(F, X, Z)) 
  plus(_|_, X) >= X 
  plus(s(X), Y) >= s(plus(X, Y)) 
  times(_|_, X) >= _|_ 
  times(s(X), Y) >= plus(times(X, Y), Y) 
  #argfun-sum#(fold(/\x./\y.y, _|_, X)) >= fold(/\x./\y.y, _|_, X) 
  #argfun-prod#(fold(/\x./\y.mul(x), s(_|_), X)) >= fold(/\x./\y.mul(x), s(_|_), X) 

With these choices, we have:

  1] fold#(F, X, cons(Y, Z)) >= fold#(F, X, Z)  because [2], [3] and [4], by (Fun) 
  2] F >= F  by (Meta) 
  3] X >= X  by (Meta) 
  4] cons(Y, Z) >= Z  because [5], by (Star) 
  5] cons*(Y, Z) >= Z  because [6], by (Select) 
  6] Z >= Z  by (Meta) 

  7] plus#(s(X), Y) >= plus#(X, Y)  because [8], by (Star) 
  8] plus#*(s(X), Y) >= plus#(X, Y)  because plus# in Mul, [9] and [12], by (Stat) 
  9] s(X) > X  because [10], by definition 
  10] s*(X) >= X  because [11], by (Select) 
  11] X >= X  by (Meta) 
  12] Y >= Y  by (Meta) 

  13] times#(s(X), Y) > plus#(times(X, Y), Y)  because [14], by definition 
  14] times#*(s(X), Y) >= plus#(times(X, Y), Y)  because times# > plus#, [15] and [20], by (Copy) 
  15] times#*(s(X), Y) >= times(X, Y)  because times# > times, [16] and [20], by (Copy) 
  16] times#*(s(X), Y) >= X  because [17], by (Select) 
  17] s(X) >= X  because [18], by (Star) 
  18] s*(X) >= X  because [19], by (Select) 
  19] X >= X  by (Meta) 
  20] times#*(s(X), Y) >= Y  because [21], by (Select) 
  21] Y >= Y  by (Meta) 

  22] fold#(/\x./\y.mul(x), s(_|_), X) >= fold#(/\x./\y.mul(x), s(_|_), X)  because [23], [27] and [29], by (Fun) 
  23] /\x./\z.mul(x) >= /\x./\z.mul(x)  because [24], by (Abs) 
  24] /\x.mul(y) >= /\x.mul(y)  because [25], by (Abs) 
  25] mul(y) >= mul(y)  because mul in Mul and [26], by (Fun) 
  26] y >= y  by (Var) 
  27] s(_|_) >= s(_|_)  because s in Mul and [28], by (Fun) 
  28] _|_ >= _|_  by (Bot) 
  29] X >= X  by (Meta) 

  30] fold(F, X, nil) >= X  because [31], by (Star) 
  31] fold*(F, X, nil) >= X  because [32], by (Select) 
  32] X >= X  by (Meta) 

  33] fold(F, X, cons(Y, Z)) >= @_{o -> o}(@_{o -> o -> o}(F, Y), fold(F, X, Z))  because [34], by (Star) 
  34] fold*(F, X, cons(Y, Z)) >= @_{o -> o}(@_{o -> o -> o}(F, Y), fold(F, X, Z))  because fold > @_{o -> o}, [35] and [41], by (Copy) 
  35] fold*(F, X, cons(Y, Z)) >= @_{o -> o -> o}(F, Y)  because fold > @_{o -> o -> o}, [36] and [37], by (Copy) 
  36] fold*(F, X, cons(Y, Z)) >= F  because [2], by (Select) 
  37] fold*(F, X, cons(Y, Z)) >= Y  because [38], by (Select) 
  38] cons(Y, Z) >= Y  because [39], by (Star) 
  39] cons*(Y, Z) >= Y  because [40], by (Select) 
  40] Y >= Y  by (Meta) 
  41] fold*(F, X, cons(Y, Z)) >= fold(F, X, Z)  because fold in Mul, [2], [3] and [42], by (Stat) 
  42] cons(Y, Z) > Z  because [43], by definition 
  43] cons*(Y, Z) >= Z  because [6], by (Select) 

  44] plus(_|_, X) >= X  because [45], by (Star) 
  45] plus*(_|_, X) >= X  because [46], by (Select) 
  46] X >= X  by (Meta) 

  47] plus(s(X), Y) >= s(plus(X, Y))  because [48], by (Star) 
  48] plus*(s(X), Y) >= s(plus(X, Y))  because plus > s and [49], by (Copy) 
  49] plus*(s(X), Y) >= plus(X, Y)  because plus in Mul, [9] and [12], by (Stat) 

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

  51] times(s(X), Y) >= plus(times(X, Y), Y)  because [52], by (Star) 
  52] times*(s(X), Y) >= plus(times(X, Y), Y)  because times > plus, [53] and [57], by (Copy) 
  53] times*(s(X), Y) >= times(X, Y)  because times in Mul, [54] and [56], by (Stat) 
  54] s(X) > X  because [55], by definition 
  55] s*(X) >= X  because [19], by (Select) 
  56] Y >= Y  by (Meta) 
  57] times*(s(X), Y) >= Y  because [56], by (Select) 

  58] #argfun-sum#(fold(/\x./\y.y, _|_, X)) >= fold(/\x./\y.y, _|_, X)  because [59], by (Star) 
  59] #argfun-sum#*(fold(/\x./\y.y, _|_, X)) >= fold(/\x./\y.y, _|_, X)  because #argfun-sum# > fold, [60], [64] and [65], by (Copy) 
  60] #argfun-sum#*(fold(/\x./\y.y, _|_, X)) >= /\x./\y.y  because [61], by (F-Abs) 
  61] #argfun-sum#*(fold(/\x./\y.y, _|_, X), z) >= /\x.x  because [62], by (F-Abs) 
  62] #argfun-sum#*(fold(/\x./\y.y, _|_, X), z, u) >= u  because [63], by (Select) 
  63] u >= u  by (Var) 
  64] #argfun-sum#*(fold(/\x./\y.y, _|_, X)) >= _|_  by (Bot) 
  65] #argfun-sum#*(fold(/\x./\y.y, _|_, X)) >= X  because [66], by (Select) 
  66] fold(/\x./\y.y, _|_, X) >= X  because [67], by (Star) 
  67] fold*(/\x./\y.y, _|_, X) >= X  because [68], by (Select) 
  68] X >= X  by (Meta) 

  69] #argfun-prod#(fold(/\x./\y.mul(x), s(_|_), X)) >= fold(/\x./\y.mul(x), s(_|_), X)  because [70], by (Star) 
  70] #argfun-prod#*(fold(/\x./\y.mul(x), s(_|_), X)) >= fold(/\x./\y.mul(x), s(_|_), X)  because [71], by (Select) 
  71] fold(/\x./\y.mul(x), s(_|_), X) >= fold(/\x./\y.mul(x), s(_|_), X)  because fold in Mul, [23], [27] and [29], by (Fun) 

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

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

Thus, the original system is terminating if (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:

  fold#(F, X, cons(Y, Z)) >? fold#(F, X, Z) 
  plus#(s(X), Y) >? plus#(X, Y) 
  prod#(X) >? fold#(/\x./\y.mul(x, y), s(0), X) 
  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( 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:

  [[fold#(x_1, x_2, x_3)]] = fold# 
  [[plus#(x_1, x_2)]] = _|_ 
  [[prod(x_1)]] = x_1 
  [[prod#(x_1)]] = prod# 
  [[sum(x_1)]] = x_1 

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

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

  fold# >= fold# 
  _|_ >= _|_ 
  #argfun-prod##(fold#) > fold# 
  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] fold# >= fold#  because fold# in Mul, by (Fun) 

  2] _|_ >= _|_  by (Bot) 

  3] #argfun-prod##(fold#) > fold#  because [4], by definition 
  4] #argfun-prod##*(fold#) >= fold#  because #argfun-prod## > fold#, by (Copy) 

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

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

  20] plus(0, X) >= X  because [21], by (Star) 
  21] plus*(0, X) >= X  because [22], by (Select) 
  22] X >= X  by (Meta) 

  23] plus(s(X), Y) >= s(plus(X, Y))  because [24], by (Star) 
  24] plus*(s(X), Y) >= s(plus(X, Y))  because plus > s and [25], by (Copy) 
  25] plus*(s(X), Y) >= plus(X, Y)  because plus in Mul, [26] and [29], by (Stat) 
  26] s(X) > X  because [27], by definition 
  27] s*(X) >= X  because [28], by (Select) 
  28] X >= X  by (Meta) 
  29] Y >= Y  by (Meta) 

  30] times(0, X) >= 0  because [31], by (Star) 
  31] times*(0, X) >= 0  because [32], by (Select) 
  32] 0 >= 0  by (Fun) 

  33] times(s(X), Y) >= plus(times(X, Y), Y)  because [34], by (Star) 
  34] times*(s(X), Y) >= plus(times(X, Y), Y)  because times > plus, [35] and [40], by (Copy) 
  35] times*(s(X), Y) >= times(X, Y)  because times in Mul, [36] and [39], by (Stat) 
  36] s(X) > X  because [37], by definition 
  37] s*(X) >= X  because [38], by (Select) 
  38] X >= X  by (Meta) 
  39] Y >= Y  by (Meta) 
  40] times*(s(X), Y) >= Y  because [39], 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 [53], 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 [51], by (Select) 
  51] fold(/\x./\y.add(x, y), 0, X) >= 0  because [52], by (Star) 
  52] fold*(/\x./\y.add(x, y), 0, X) >= 0  because [32], by (Select) 
  53] #argfun-sum#*(fold(/\x./\y.add(x, y), 0, X)) >= X  because [54], by (Select) 
  54] fold(/\x./\y.add(x, y), 0, X) >= X  because [55], by (Star) 
  55] fold*(/\x./\y.add(x, y), 0, X) >= X  because [56], by (Select) 
  56] X >= X  by (Meta) 

  57] #argfun-prod#(fold(/\x./\y.mul(x, y), s(0), X)) >= fold(/\x./\y.mul(x, y), s(0), X)  because [58], by (Star) 
  58] #argfun-prod#*(fold(/\x./\y.mul(x, y), s(0), X)) >= fold(/\x./\y.mul(x, y), s(0), X)  because #argfun-prod# > fold, [59], [66] and [71], by (Copy) 
  59] #argfun-prod#*(fold(/\x./\y.mul(x, y), s(0), X)) >= /\x./\y.mul(x, y)  because [60], by (F-Abs) 
  60] #argfun-prod#*(fold(/\x./\y.mul(x, y), s(0), X), z) >= /\x.mul(z, x)  because [61], by (F-Abs) 
  61] #argfun-prod#*(fold(/\x./\y.mul(x, y), s(0), X), z, u) >= mul(z, u)  because #argfun-prod# > mul, [62] and [64], by (Copy) 
  62] #argfun-prod#*(fold(/\x./\y.mul(x, y), s(0), X), z, u) >= z  because [63], by (Select) 
  63] z >= z  by (Var) 
  64] #argfun-prod#*(fold(/\x./\y.mul(x, y), s(0), X), z, u) >= u  because [65], by (Select) 
  65] u >= u  by (Var) 
  66] #argfun-prod#*(fold(/\x./\y.mul(x, y), s(0), X)) >= s(0)  because [67], by (Select) 
  67] fold(/\x./\y.mul(x, y), s(0), X) >= s(0)  because [68], by (Star) 
  68] fold*(/\x./\y.mul(x, y), s(0), X) >= s(0)  because [69], by (Select) 
  69] s(0) >= s(0)  because s in Mul and [70], by (Fun) 
  70] 0 >= 0  by (Fun) 
  71] #argfun-prod#*(fold(/\x./\y.mul(x, y), s(0), X)) >= X  because [72], by (Select) 
  72] fold(/\x./\y.mul(x, y), s(0), X) >= X  because [73], by (Star) 
  73] fold*(/\x./\y.mul(x, y), s(0), X) >= X  because [74], by (Select) 
  74] X >= X  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_0, static, formative) by (P_4, R_0, static, formative), where P_4 consists of:

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

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

We consider the dependency pair problem (P_4, 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) 
  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:

  [[#argfun-prod#(x_1)]] = x_1 
  [[fold#(x_1, x_2, x_3)]] = x_3 
  [[prod(x_1)]] = x_1 
  [[sum(x_1)]] = x_1 

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

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

  cons(X, Y) > Y 
  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) 
  fold(/\x./\y.mul(x, y), s(0), X) >= fold(/\x./\y.mul(x, y), s(0), X) 

With these choices, we have:

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

  4] plus#(s(X), Y) >= plus#(X, Y)  because plus# in Mul, [5] and [8], by (Fun) 
  5] s(X) >= X  because [6], by (Star) 
  6] s*(X) >= X  because [7], by (Select) 
  7] X >= X  by (Meta) 
  8] Y >= Y  by (Meta) 

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

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

  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 [8], by (Stat) 
  31] s(X) > X  because [32], by definition 
  32] s*(X) >= X  because [7], by (Select) 

  33] times(0, X) >= 0  because [34], by (Star) 
  34] times*(0, X) >= 0  because [35], by (Select) 
  35] 0 >= 0  by (Fun) 

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

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

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

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

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

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

We consider the dependency pair problem (P_5, 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# > add > fold > @_{o -> o} > cons > #argfun-sum# > @_{o -> o -> o} > mul > nil > plus# > times > 0 > plus > s

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 [22], by (Copy) 
  15] fold*(F, X, cons(Y, Z)) >= @_{o -> o -> o}(F, Y)  because fold > @_{o -> o -> o}, [16] and [18], by (Copy) 
  16] fold*(F, X, cons(Y, Z)) >= F  because [17], by (Select) 
  17] F >= F  by (Meta) 
  18] fold*(F, X, cons(Y, Z)) >= Y  because [19], by (Select) 
  19] cons(Y, Z) >= Y  because [20], by (Star) 
  20] cons*(Y, Z) >= Y  because [21], by (Select) 
  21] Y >= Y  by (Meta) 
  22] fold*(F, X, cons(Y, Z)) >= fold(F, X, Z)  because fold in Mul, [23], [24] and [25], by (Stat) 
  23] F >= F  by (Meta) 
  24] X >= X  by (Meta) 
  25] cons(Y, Z) > Z  because [26], by definition 
  26] cons*(Y, Z) >= Z  because [27], by (Select) 
  27] Z >= Z  by (Meta) 

  28] plus(0, X) >= X  because [29], by (Star) 
  29] plus*(0, X) >= X  because [30], by (Select) 
  30] X >= X  by (Meta) 

  31] plus(s(X), Y) >= s(plus(X, Y))  because [32], by (Star) 
  32] plus*(s(X), Y) >= s(plus(X, Y))  because plus > s and [33], by (Copy) 
  33] plus*(s(X), Y) >= plus(X, Y)  because plus in Mul, [3] and [34], by (Stat) 
  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 [44], by (Copy) 
  39] times*(s(X), Y) >= times(X, Y)  because times in Mul, [40] and [43], by (Stat) 
  40] s(X) > X  because [41], by definition 
  41] s*(X) >= X  because [42], by (Select) 
  42] X >= X  by (Meta) 
  43] Y >= Y  by (Meta) 
  44] times*(s(X), Y) >= Y  because [43], by (Select) 

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

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