We consider the system h01.

  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 
    xap : [a -> c -> c * a] --> c -> c 
    yap : [c -> c * c] --> c 

  Rules:

    fold(/\x./\y.yap(xap(f, x), y), z) nil => z 
    fold(/\x./\y.yap(xap(f, x), y), z) cons(u, v) => yap(xap(f, u), fold(/\w./\x'.yap(xap(f, w), x'), z) v) 
    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(/\x./\y.yap(xap(add, x), y), 0) 
    prod => fold(/\x./\y.yap(xap(mul, x), y), s(0)) 
    xap(f, x) => f x 
    yap(f, x) => f x 

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

Symbol xap is an encoding for application that is only used in innocuous ways.  We can simplify the program (without losing non-termination) by removing it.  This gives:

  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 
    yap : [c -> c * c] --> c 

  Rules:

    fold(/\x./\y.yap(F(x), y), X) nil => X 
    fold(/\x./\y.yap(F(x), y), X) cons(Y, Z) => yap(F(Y), fold(/\z./\u.yap(F(z), u), 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(/\x./\y.yap(add(x), y), 0) 
    prod => fold(/\x./\y.yap(mul(x), y), s(0)) 
    yap(F, X) => F X 

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

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

  fold(/\x./\y.yap(F(x), y), X) nil >? X 
  fold(/\x./\y.yap(F(x), y), X) cons(Y, Z) >? yap(F(Y), fold(/\z./\u.yap(F(z), u), 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(/\x./\y.yap(add(x), y), 0) 
  prod >? fold(/\x./\y.yap(mul(x), y), s(0)) 
  yap(F, X) >? F X 

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

Argument functions:

  [[0]] = _|_ 

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

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

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

With these choices, we have:

  1] @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), nil) >= X  because [2], by (Star) 
  2] @_{o -> o}*(fold(/\x./\y.yap(F(x), y), X), nil) >= X  because [3], by (Select) 
  3] fold(/\x./\y.yap(F(x), y), X) @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), nil) >= X  because [4] 
  4] fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), nil)) >= X  because [5], by (Select) 
  5] X >= X  by (Meta) 

  6] @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), cons(Y, Z)) >= yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z))  because [7], by (Star) 
  7] @_{o -> o}*(fold(/\x./\y.yap(F(x), y), X), cons(Y, Z)) >= yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z))  because [8], by (Select) 
  8] fold(/\x./\y.yap(F(x), y), X) @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z)) >= yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z))  because [9] 
  9] fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z))) >= yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z))  because fold > yap, [10] and [18], by (Copy) 
  10] fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z))) >= F(Y)  because [11], by (Select) 
  11] /\x.yap(F(fold*(/\y./\z.yap(F(y), z), X, @_{o -> o}*(fold(/\u./\v.yap(F(u), v), X), cons(Y, Z)))), x) >= F(Y)  because [12], by (Eta)[Kop13:2] 
  12] F(fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z)))) >= F(Y)  because [13], by (Meta) 
  13] fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z))) >= Y  because [14], by (Select) 
  14] @_{o -> o}*(fold(/\x./\y.yap(F(x), y), X), cons(Y, Z)) >= Y  because [15], by (Select) 
  15] cons(Y, Z) >= Y  because [16], by (Star) 
  16] cons*(Y, Z) >= Y  because [17], by (Select) 
  17] Y >= Y  by (Meta) 
  18] fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z))) >= @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z)  because [19], by (Select) 
  19] @_{o -> o}*(fold(/\x./\y.yap(F(x), y), X), cons(Y, Z)) >= @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z)  because @_{o -> o} in Mul, [20] and [28], by (Stat) 
  20] fold(/\x./\y.yap(F(x), y), X) >= fold(/\x./\y.yap(F(x), y), X)  because fold in Mul, [21] and [27], by (Fun) 
  21] /\x./\z.yap(F(x), z) >= /\x./\z.yap(F(x), z)  because [22], by (Abs) 
  22] /\z.yap(F(y), z) >= /\z.yap(F(y), z)  because [23], by (Abs) 
  23] yap(F(y), x) >= yap(F(y), x)  because yap in Mul, [24] and [26], by (Fun) 
  24] F(y) >= F(y)  because [25], by (Meta) 
  25] y >= y  by (Var) 
  26] x >= x  by (Var) 
  27] X >= X  by (Meta) 
  28] cons(Y, Z) > Z  because [29], by definition 
  29] cons*(Y, Z) >= Z  because [30], by (Select) 
  30] Z >= Z  by (Meta) 

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

  34] plus(s(X), Y) >= s(plus(X, Y))  because [35], by (Star) 
  35] plus*(s(X), Y) >= s(plus(X, Y))  because plus > s and [36], by (Copy) 
  36] plus*(s(X), Y) >= plus(X, Y)  because plus 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(_|_, X) >= _|_  by (Bot) 

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

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

  61] prod >= fold(/\x./\y.yap(mul(x), y), s(_|_))  because [62], by (Star) 
  62] prod* >= fold(/\x./\y.yap(mul(x), y), s(_|_))  because prod > fold, [63] and [71], by (Copy) 
  63] prod* >= /\y./\z.yap(mul(y), z)  because [64], by (F-Abs) 
  64] prod*(x) >= /\z.yap(mul(x), z)  because [65], by (F-Abs) 
  65] prod*(x, y) >= yap(mul(x), y)  because prod > yap, [66] and [69], by (Copy) 
  66] prod*(x, y) >= mul(x)  because prod > mul and [67], by (Copy) 
  67] prod*(x, y) >= x  because [68], by (Select) 
  68] x >= x  by (Var) 
  69] prod*(x, y) >= y  because [70], by (Select) 
  70] y >= y  by (Var) 
  71] prod* >= s(_|_)  because prod > s and [72], by (Copy) 
  72] prod* >= _|_  by (Bot) 

  73] yap(F, X) >= @_{o -> o}(F, X)  because [74], by (Star) 
  74] yap*(F, X) >= @_{o -> o}(F, X)  because yap > @_{o -> o}, [75] and [77], by (Copy) 
  75] yap*(F, X) >= F  because [76], by (Select) 
  76] F >= F  by (Meta) 
  77] yap*(F, X) >= X  because [78], by (Select) 
  78] X >= X  by (Meta) 

We can thus remove the following rules:

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

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

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

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

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

Argument functions:

  [[0]] = _|_ 
  [[s(x_1)]] = x_1 

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

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

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

With these choices, we have:

  1] @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), nil) >= X  because [2], by (Star) 
  2] @_{o -> o}*(fold(/\x./\y.yap(F(x), y), X), nil) >= X  because [3], by (Select) 
  3] fold(/\x./\y.yap(F(x), y), X) @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), nil) >= X  because [4] 
  4] fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), nil)) >= X  because [5], by (Select) 
  5] X >= X  by (Meta) 

  6] @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), cons(Y, Z)) >= yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z))  because [7], by (Star) 
  7] @_{o -> o}*(fold(/\x./\y.yap(F(x), y), X), cons(Y, Z)) >= yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z))  because [8], by (Select) 
  8] fold(/\x./\y.yap(F(x), y), X) @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z)) >= yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z))  because [9] 
  9] fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z))) >= yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z))  because [10], by (Select) 
  10] @_{o -> o}*(fold(/\x./\y.yap(F(x), y), X), cons(Y, Z)) >= yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z))  because [11], by (Select) 
  11] fold(/\x./\y.yap(F(x), y), X) @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z)) >= yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z))  because [12] 
  12] fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z))) >= yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z))  because [13], by (Select) 
  13] yap(F(fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z)))), fold*(/\v./\w.yap(F(v), w), X, @_{o -> o}*(fold(/\x'./\y'.yap(F(x'), y'), X), cons(Y, Z)))) >= yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z))  because yap in Mul, [14] and [20], by (Fun) 
  14] F(fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z)))) >= F(Y)  because [15], by (Meta) 
  15] fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z))) >= Y  because [16], by (Select) 
  16] @_{o -> o}*(fold(/\x./\y.yap(F(x), y), X), cons(Y, Z)) >= Y  because [17], by (Select) 
  17] cons(Y, Z) >= Y  because [18], by (Star) 
  18] cons*(Y, Z) >= Y  because [19], by (Select) 
  19] Y >= Y  by (Meta) 
  20] fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z))) >= @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z)  because [21], by (Select) 
  21] @_{o -> o}*(fold(/\x./\y.yap(F(x), y), X), cons(Y, Z)) >= @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z)  because @_{o -> o} in Mul, [22] and [30], by (Stat) 
  22] fold(/\x./\y.yap(F(x), y), X) >= fold(/\x./\y.yap(F(x), y), X)  because fold in Mul, [23] and [29], by (Fun) 
  23] /\x./\z.yap(F(x), z) >= /\x./\z.yap(F(x), z)  because [24], by (Abs) 
  24] /\z.yap(F(y), z) >= /\z.yap(F(y), z)  because [25], by (Abs) 
  25] yap(F(y), x) >= yap(F(y), x)  because yap in Mul, [26] and [28], by (Fun) 
  26] F(y) >= F(y)  because [27], by (Meta) 
  27] y >= y  by (Var) 
  28] x >= x  by (Var) 
  29] X >= X  by (Meta) 
  30] cons(Y, Z) > Z  because [31], by definition 
  31] cons*(Y, Z) >= Z  because [32], by (Select) 
  32] Z >= Z  by (Meta) 

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

  36] plus(X, Y) >= plus(X, Y)  because plus in Mul, [37] and [38], by (Fun) 
  37] X >= X  by (Meta) 
  38] Y >= Y  by (Meta) 

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

  40] sum >= fold(/\x./\y.yap(add(x), y), _|_)  because [41], by (Star) 
  41] sum* >= fold(/\x./\y.yap(add(x), y), _|_)  because sum > fold, [42] and [50], by (Copy) 
  42] sum* >= /\y./\z.yap(add(y), z)  because [43], by (F-Abs) 
  43] sum*(x) >= /\z.yap(add(x), z)  because [44], by (F-Abs) 
  44] sum*(x, y) >= yap(add(x), y)  because sum > yap, [45] and [48], by (Copy) 
  45] sum*(x, y) >= add(x)  because sum > add and [46], by (Copy) 
  46] sum*(x, y) >= x  because [47], by (Select) 
  47] x >= x  by (Var) 
  48] sum*(x, y) >= y  because [49], by (Select) 
  49] y >= y  by (Var) 
  50] sum* >= _|_  by (Bot) 

  51] prod >= fold(/\x./\y.yap(mul(x), y), _|_)  because [52], by (Star) 
  52] prod* >= fold(/\x./\y.yap(mul(x), y), _|_)  because prod > fold, [53] and [61], by (Copy) 
  53] prod* >= /\y./\z.yap(mul(y), z)  because [54], by (F-Abs) 
  54] prod*(x) >= /\z.yap(mul(x), z)  because [55], by (F-Abs) 
  55] prod*(x, y) >= yap(mul(x), y)  because prod > yap, [56] and [59], by (Copy) 
  56] prod*(x, y) >= mul(x)  because prod > mul and [57], by (Copy) 
  57] prod*(x, y) >= x  because [58], by (Select) 
  58] x >= x  by (Var) 
  59] prod*(x, y) >= y  because [60], by (Select) 
  60] y >= y  by (Var) 
  61] prod* >= _|_  by (Bot) 

  62] yap(F, X) > @_{o -> o}(F, X)  because [63], by definition 
  63] yap*(F, X) >= @_{o -> o}(F, X)  because yap > @_{o -> o}, [64] and [66], by (Copy) 
  64] yap*(F, X) >= F  because [65], by (Select) 
  65] F >= F  by (Meta) 
  66] yap*(F, X) >= X  because [67], by (Select) 
  67] X >= X  by (Meta) 

We can thus remove the following rules:

  plus(0, X) => X 
  yap(F, X) => F X 

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

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

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

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

Argument functions:

  [[0]] = _|_ 
  [[s(x_1)]] = x_1 

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

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

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

With these choices, we have:

  1] @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), nil) > X  because [2], by definition 
  2] @_{o -> o}*(fold(/\x./\y.yap(F(x), y), X), nil) >= X  because [3], by (Select) 
  3] fold(/\x./\y.yap(F(x), y), X) @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), nil) >= X  because [4] 
  4] fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), nil)) >= X  because [5], by (Select) 
  5] X >= X  by (Meta) 

  6] @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), cons(Y, Z)) >= yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z))  because [7], by (Star) 
  7] @_{o -> o}*(fold(/\x./\y.yap(F(x), y), X), cons(Y, Z)) >= yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z))  because [8], by (Select) 
  8] fold(/\x./\y.yap(F(x), y), X) @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z)) >= yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z))  because [9] 
  9] fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z))) >= yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z))  because [10], by (Select) 
  10] yap(F(fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z)))), fold*(/\v./\w.yap(F(v), w), X, @_{o -> o}*(fold(/\x'./\y'.yap(F(x'), y'), X), cons(Y, Z)))) >= yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z))  because yap in Mul, [11] and [17], by (Fun) 
  11] F(fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z)))) >= F(Y)  because [12], by (Meta) 
  12] fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z))) >= Y  because [13], by (Select) 
  13] @_{o -> o}*(fold(/\x./\y.yap(F(x), y), X), cons(Y, Z)) >= Y  because [14], by (Select) 
  14] cons(Y, Z) >= Y  because [15], by (Star) 
  15] cons*(Y, Z) >= Y  because [16], by (Select) 
  16] Y >= Y  by (Meta) 
  17] fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z))) >= @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z)  because [18], by (Select) 
  18] @_{o -> o}*(fold(/\x./\y.yap(F(x), y), X), cons(Y, Z)) >= @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z)  because @_{o -> o} in Mul, [19] and [27], by (Stat) 
  19] fold(/\x./\y.yap(F(x), y), X) >= fold(/\x./\y.yap(F(x), y), X)  because fold in Mul, [20] and [26], by (Fun) 
  20] /\x./\z.yap(F(x), z) >= /\x./\z.yap(F(x), z)  because [21], by (Abs) 
  21] /\z.yap(F(y), z) >= /\z.yap(F(y), z)  because [22], by (Abs) 
  22] yap(F(y), x) >= yap(F(y), x)  because yap in Mul, [23] and [25], by (Fun) 
  23] F(y) >= F(y)  because [24], by (Meta) 
  24] y >= y  by (Var) 
  25] x >= x  by (Var) 
  26] X >= X  by (Meta) 
  27] cons(Y, Z) > Z  because [28], by definition 
  28] cons*(Y, Z) >= Z  because [29], by (Select) 
  29] Z >= Z  by (Meta) 

  30] plus(X, Y) >= plus(X, Y)  because plus in Mul, [31] and [32], by (Fun) 
  31] X >= X  by (Meta) 
  32] Y >= Y  by (Meta) 

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

  34] sum >= fold(/\x./\y.yap(add(x), y), _|_)  because [35], by (Star) 
  35] sum* >= fold(/\x./\y.yap(add(x), y), _|_)  because sum > fold, [36] and [44], by (Copy) 
  36] sum* >= /\y./\z.yap(add(y), z)  because [37], by (F-Abs) 
  37] sum*(x) >= /\z.yap(add(x), z)  because [38], by (F-Abs) 
  38] sum*(x, y) >= yap(add(x), y)  because sum > yap, [39] and [42], by (Copy) 
  39] sum*(x, y) >= add(x)  because sum > add and [40], by (Copy) 
  40] sum*(x, y) >= x  because [41], by (Select) 
  41] x >= x  by (Var) 
  42] sum*(x, y) >= y  because [43], by (Select) 
  43] y >= y  by (Var) 
  44] sum* >= _|_  by (Bot) 

  45] prod > fold(/\x./\y.yap(mul(x), y), _|_)  because [46], by definition 
  46] prod* >= fold(/\x./\y.yap(mul(x), y), _|_)  because prod > fold, [47] and [55], by (Copy) 
  47] prod* >= /\y./\z.yap(mul(y), z)  because [48], by (F-Abs) 
  48] prod*(x) >= /\z.yap(mul(x), z)  because [49], by (F-Abs) 
  49] prod*(x, y) >= yap(mul(x), y)  because prod > yap, [50] and [53], by (Copy) 
  50] prod*(x, y) >= mul(x)  because prod > mul and [51], by (Copy) 
  51] prod*(x, y) >= x  because [52], by (Select) 
  52] x >= x  by (Var) 
  53] prod*(x, y) >= y  because [54], by (Select) 
  54] y >= y  by (Var) 
  55] prod* >= _|_  by (Bot) 

We can thus remove the following rules:

  fold(/\x./\y.yap(F(x), y), X) nil => X 
  prod => fold(/\x./\y.yap(mul(x), y), s(0)) 

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

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

  fold(/\x./\y.yap(F(x), y), X) cons(Y, Z) >? yap(F(Y), fold(/\z./\u.yap(F(z), u), X) Z) 
  plus(s(X), Y) >? s(plus(X, Y)) 
  times(0, X) >? 0 
  sum >? fold(/\x./\y.yap(add(x), y), 0) 

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

Argument functions:

  [[0]] = _|_ 

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

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

  @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), cons(Y, Z)) >= yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z)) 
  plus(s(X), Y) >= s(plus(X, Y)) 
  times(_|_, X) >= _|_ 
  sum > fold(/\x./\y.yap(add(x), y), _|_) 

With these choices, we have:

  1] @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), cons(Y, Z)) >= yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z))  because [2], by (Star) 
  2] @_{o -> o}*(fold(/\x./\y.yap(F(x), y), X), cons(Y, Z)) >= yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z))  because [3], by (Select) 
  3] fold(/\x./\y.yap(F(x), y), X) @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z)) >= yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z))  because [4] 
  4] fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z))) >= yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z))  because [5], by (Select) 
  5] yap(F(fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z)))), fold*(/\v./\w.yap(F(v), w), X, @_{o -> o}*(fold(/\x'./\y'.yap(F(x'), y'), X), cons(Y, Z)))) >= yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z))  because yap in Mul, [6] and [12], by (Fun) 
  6] F(fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z)))) >= F(Y)  because [7], by (Meta) 
  7] fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z))) >= Y  because [8], by (Select) 
  8] @_{o -> o}*(fold(/\x./\y.yap(F(x), y), 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] fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z))) >= @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z)  because [13], by (Select) 
  13] @_{o -> o}*(fold(/\x./\y.yap(F(x), y), X), cons(Y, Z)) >= @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z)  because @_{o -> o} in Mul, [14] and [22], by (Stat) 
  14] fold(/\x./\y.yap(F(x), y), X) >= fold(/\x./\y.yap(F(x), y), X)  because fold in Mul, [15] and [21], by (Fun) 
  15] /\x./\z.yap(F(x), z) >= /\x./\z.yap(F(x), z)  because [16], by (Abs) 
  16] /\z.yap(F(y), z) >= /\z.yap(F(y), z)  because [17], by (Abs) 
  17] yap(F(y), x) >= yap(F(y), x)  because yap in Mul, [18] and [20], by (Fun) 
  18] F(y) >= F(y)  because [19], by (Meta) 
  19] y >= y  by (Var) 
  20] x >= x  by (Var) 
  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(s(X), Y) >= s(plus(X, Y))  because [26], by (Star) 
  26] plus*(s(X), Y) >= s(plus(X, Y))  because plus > s and [27], by (Copy) 
  27] plus*(s(X), Y) >= plus(X, Y)  because plus in Mul, [28] and [31], by (Stat) 
  28] s(X) > X  because [29], by definition 
  29] s*(X) >= X  because [30], by (Select) 
  30] X >= X  by (Meta) 
  31] Y >= Y  by (Meta) 

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

  33] sum > fold(/\x./\y.yap(add(x), y), _|_)  because [34], by definition 
  34] sum* >= fold(/\x./\y.yap(add(x), y), _|_)  because sum > fold, [35] and [43], by (Copy) 
  35] sum* >= /\y./\z.yap(add(y), z)  because [36], by (F-Abs) 
  36] sum*(x) >= /\z.yap(add(x), z)  because [37], by (F-Abs) 
  37] sum*(x, y) >= yap(add(x), y)  because sum > yap, [38] and [41], by (Copy) 
  38] sum*(x, y) >= add(x)  because sum > add and [39], by (Copy) 
  39] sum*(x, y) >= x  because [40], by (Select) 
  40] x >= x  by (Var) 
  41] sum*(x, y) >= y  because [42], by (Select) 
  42] y >= y  by (Var) 
  43] sum* >= _|_  by (Bot) 

We can thus remove the following rules:

  sum => fold(/\x./\y.yap(add(x), y), 0) 

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

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

  fold(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >? yap(F(Y), fold(/\z./\u.yap(F(z), u), X, Z)) 
  plus(s(X), Y) >? s(plus(X, Y)) 
  times(0, X) >? 0 

We orient these requirements with a polynomial interpretation in the natural numbers.

The following interpretation satisfies the requirements:

  0 = 0 
  cons = \y0y1.3 + 2y0 + 3y1 
  fold = \G0y1y2.1 + y1 + y2 + 2y2y2G0(y2,y2) + 2G0(y1,y1) 
  plus = \y0y1.2y1 + 3y0 
  s = \y0.3 + y0 
  times = \y0y1.3 + 2y1 + 3y0 
  yap = \G0y1.y1 + G0(0) 

Using this interpretation, the requirements translate to:

  [[fold(/\x./\y.yap(_F0(x), y), _x1, cons(_x2, _x3))]] = 58 + 3x1 + 16x2x2x2 + 54x3x3x3 + 72x2x2 + 72x2x2x3 + 108x2x3x3 + 110x2 + 162x3x3 + 165x3 + 216x2x3 + 2F0(x1,0) + 8x2x2F0(3 + 2x2 + 3x3,0) + 18x3x3F0(3 + 2x2 + 3x3,0) + 18F0(3 + 2x2 + 3x3,0) + 24x2x3F0(3 + 2x2 + 3x3,0) + 24x2F0(3 + 2x2 + 3x3,0) + 36x3F0(3 + 2x2 + 3x3,0) > 1 + x3 + 2x3x3x3 + 3x1 + F0(x2,0) + 2x3x3F0(x3,0) + 2F0(x1,0) = [[yap(_F0(_x2), fold(/\x./\y.yap(_F0(x), y), _x1, _x3))]] 
  [[plus(s(_x0), _x1)]] = 9 + 2x1 + 3x0 > 3 + 2x1 + 3x0 = [[s(plus(_x0, _x1))]] 
  [[times(0, _x0)]] = 3 + 2x0 > 0 = [[0]] 

We can thus remove the following rules:

  fold(/\x./\y.yap(F(x), y), X, cons(Y, Z)) => yap(F(Y), fold(/\z./\u.yap(F(z), u), X, Z)) 
  plus(s(X), Y) => s(plus(X, Y)) 
  times(0, X) => 0 

All rules were succesfully removed.  Thus, termination of the original system has been reduced to termination of the beta-rule, which is well-known to hold.


+++ Citations +++

[Kop12]  C. Kop.  Higher Order Termination.  PhD Thesis, 2012.
[Kop13:2]  C. Kop.  StarHorpo with an Eta-Rule.  Unpublished manuscript, http://cl-informatik.uibk.ac.at/users/kop/etahorpo.pdf, 2013.