We consider the system Applicative_first_order_05__11.

  Alphabet:

    !facminus : [a * a] --> a 
    !facplus : [a * a] --> a 
    !factimes : [a * a] --> a 
    0 : [] --> a 
    1 : [] --> a 
    2 : [] --> a 
    D : [a] --> a 
    cons : [c * d] --> d 
    constant : [] --> a 
    div : [a * a] --> a 
    false : [] --> b 
    filter : [c -> b * d] --> d 
    filter2 : [b * c -> b * c * d] --> d 
    ln : [a] --> a 
    map : [c -> c * d] --> d 
    minus : [a] --> a 
    nil : [] --> d 
    pow : [a * a] --> a 
    t : [] --> a 
    true : [] --> b 

  Rules:

    D(t) => 1 
    D(constant) => 0 
    D(!facplus(x, y)) => !facplus(D(x), D(y)) 
    D(!factimes(x, y)) => !facplus(!factimes(y, D(x)), !factimes(x, D(y))) 
    D(!facminus(x, y)) => !facminus(D(x), D(y)) 
    D(minus(x)) => minus(D(x)) 
    D(div(x, y)) => !facminus(div(D(x), y), div(!factimes(x, D(y)), pow(y, 2))) 
    D(ln(x)) => div(D(x), x) 
    D(pow(x, y)) => !facplus(!factimes(!factimes(y, pow(x, !facminus(y, 1))), D(x)), !factimes(!factimes(pow(x, y), ln(x)), D(y))) 
    map(f, nil) => nil 
    map(f, cons(x, y)) => cons(f x, map(f, y)) 
    filter(f, nil) => nil 
    filter(f, cons(x, y)) => filter2(f x, f, x, y) 
    filter2(true, f, x, y) => cons(x, filter(f, y)) 
    filter2(false, f, x, y) => filter(f, y) 

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]).

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

  Dependency Pairs P_0:

    0] D#(!facplus(X, Y)) =#> D#(X)   
    1] D#(!facplus(X, Y)) =#> D#(Y)   
    2] D#(!factimes(X, Y)) =#> D#(X)   
    3] D#(!factimes(X, Y)) =#> D#(Y)   
    4] D#(!facminus(X, Y)) =#> D#(X)   
    5] D#(!facminus(X, Y)) =#> D#(Y)   
    6] D#(minus(X)) =#> D#(X)   
    7] D#(div(X, Y)) =#> D#(X)   
    8] D#(div(X, Y)) =#> D#(Y)   
    9] D#(ln(X)) =#> D#(X)   
    10] D#(pow(X, Y)) =#> D#(X)   
    11] D#(pow(X, Y)) =#> D#(Y)   
    12] map#(F, cons(X, Y)) =#> map#(F, Y)   
    13] filter#(F, cons(X, Y)) =#> filter2#(F X, F, X, Y)   
    14] filter2#(true, F, X, Y) =#> filter#(F, Y)   
    15] filter2#(false, F, X, Y) =#> filter#(F, Y)   

  Rules R_0:

    D(t) => 1 
    D(constant) => 0 
    D(!facplus(X, Y)) => !facplus(D(X), D(Y)) 
    D(!factimes(X, Y)) => !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) 
    D(!facminus(X, Y)) => !facminus(D(X), D(Y)) 
    D(minus(X)) => minus(D(X)) 
    D(div(X, Y)) => !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) 
    D(ln(X)) => div(D(X), X) 
    D(pow(X, Y)) => !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) 
    map(F, nil) => nil 
    map(F, cons(X, Y)) => cons(F X, map(F, Y)) 
    filter(F, nil) => nil 
    filter(F, cons(X, Y)) => filter2(F X, F, X, Y) 
    filter2(true, F, X, Y) => cons(X, filter(F, Y)) 
    filter2(false, F, X, Y) => filter(F, Y) 

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:

  D#(!facplus(X, Y)) >? D#(X) 
  D#(!facplus(X, Y)) >? D#(Y) 
  D#(!factimes(X, Y)) >? D#(X) 
  D#(!factimes(X, Y)) >? D#(Y) 
  D#(!facminus(X, Y)) >? D#(X) 
  D#(!facminus(X, Y)) >? D#(Y) 
  D#(minus(X)) >? D#(X) 
  D#(div(X, Y)) >? D#(X) 
  D#(div(X, Y)) >? D#(Y) 
  D#(ln(X)) >? D#(X) 
  D#(pow(X, Y)) >? D#(X) 
  D#(pow(X, Y)) >? D#(Y) 
  map#(F, cons(X, Y)) >? map#(F, Y) 
  filter#(F, cons(X, Y)) >? filter2#(F X, F, X, Y) 
  filter2#(true, F, X, Y) >? filter#(F, Y) 
  filter2#(false, F, X, Y) >? filter#(F, Y) 
  D(t) >= 1 
  D(constant) >= 0 
  D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) 
  D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) 
  D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) 
  D(minus(X)) >= minus(D(X)) 
  D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) 
  D(ln(X)) >= div(D(X), X) 
  D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) 
  map(F, nil) >= nil 
  map(F, cons(X, Y)) >= cons(F X, map(F, Y)) 
  filter(F, nil) >= nil 
  filter(F, cons(X, Y)) >= filter2(F X, F, X, Y) 
  filter2(true, F, X, Y) >= cons(X, filter(F, Y)) 
  filter2(false, F, X, Y) >= filter(F, Y) 

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

The following interpretation satisfies the requirements:

  !facminus = \y0y1.0 
  !facplus = \y0y1.0 
  !factimes = \y0y1.0 
  0 = 0 
  1 = 0 
  2 = 0 
  D = \y0.0 
  D# = \y0.0 
  cons = \y0y1.2 + y1 
  constant = 3 
  div = \y0y1.0 
  false = 3 
  filter = \G0y1.y1 
  filter2 = \y0G1y2y3.2 + y3 
  filter2# = \y0G1y2y3.2y3G1(y3) 
  filter# = \G0y1.2y1G0(y1) 
  ln = \y0.0 
  map = \G0y1.2y1 
  map# = \G0y1.y1 
  minus = \y0.0 
  nil = 1 
  pow = \y0y1.0 
  t = 3 
  true = 3 

Using this interpretation, the requirements translate to:

  [[D#(!facplus(_x0, _x1))]] = 0 >= 0 = [[D#(_x0)]] 
  [[D#(!facplus(_x0, _x1))]] = 0 >= 0 = [[D#(_x1)]] 
  [[D#(!factimes(_x0, _x1))]] = 0 >= 0 = [[D#(_x0)]] 
  [[D#(!factimes(_x0, _x1))]] = 0 >= 0 = [[D#(_x1)]] 
  [[D#(!facminus(_x0, _x1))]] = 0 >= 0 = [[D#(_x0)]] 
  [[D#(!facminus(_x0, _x1))]] = 0 >= 0 = [[D#(_x1)]] 
  [[D#(minus(_x0))]] = 0 >= 0 = [[D#(_x0)]] 
  [[D#(div(_x0, _x1))]] = 0 >= 0 = [[D#(_x0)]] 
  [[D#(div(_x0, _x1))]] = 0 >= 0 = [[D#(_x1)]] 
  [[D#(ln(_x0))]] = 0 >= 0 = [[D#(_x0)]] 
  [[D#(pow(_x0, _x1))]] = 0 >= 0 = [[D#(_x0)]] 
  [[D#(pow(_x0, _x1))]] = 0 >= 0 = [[D#(_x1)]] 
  [[map#(_F0, cons(_x1, _x2))]] = 2 + x2 > x2 = [[map#(_F0, _x2)]] 
  [[filter#(_F0, cons(_x1, _x2))]] = 2x2F0(2 + x2) + 4F0(2 + x2) >= 2x2F0(x2) = [[filter2#(_F0 _x1, _F0, _x1, _x2)]] 
  [[filter2#(true, _F0, _x1, _x2)]] = 2x2F0(x2) >= 2x2F0(x2) = [[filter#(_F0, _x2)]] 
  [[filter2#(false, _F0, _x1, _x2)]] = 2x2F0(x2) >= 2x2F0(x2) = [[filter#(_F0, _x2)]] 
  [[D(t)]] = 0 >= 0 = [[1]] 
  [[D(constant)]] = 0 >= 0 = [[0]] 
  [[D(!facplus(_x0, _x1))]] = 0 >= 0 = [[!facplus(D(_x0), D(_x1))]] 
  [[D(!factimes(_x0, _x1))]] = 0 >= 0 = [[!facplus(!factimes(_x1, D(_x0)), !factimes(_x0, D(_x1)))]] 
  [[D(!facminus(_x0, _x1))]] = 0 >= 0 = [[!facminus(D(_x0), D(_x1))]] 
  [[D(minus(_x0))]] = 0 >= 0 = [[minus(D(_x0))]] 
  [[D(div(_x0, _x1))]] = 0 >= 0 = [[!facminus(div(D(_x0), _x1), div(!factimes(_x0, D(_x1)), pow(_x1, 2)))]] 
  [[D(ln(_x0))]] = 0 >= 0 = [[div(D(_x0), _x0)]] 
  [[D(pow(_x0, _x1))]] = 0 >= 0 = [[!facplus(!factimes(!factimes(_x1, pow(_x0, !facminus(_x1, 1))), D(_x0)), !factimes(!factimes(pow(_x0, _x1), ln(_x0)), D(_x1)))]] 
  [[map(_F0, nil)]] = 2 >= 1 = [[nil]] 
  [[map(_F0, cons(_x1, _x2))]] = 4 + 2x2 >= 2 + 2x2 = [[cons(_F0 _x1, map(_F0, _x2))]] 
  [[filter(_F0, nil)]] = 1 >= 1 = [[nil]] 
  [[filter(_F0, cons(_x1, _x2))]] = 2 + x2 >= 2 + x2 = [[filter2(_F0 _x1, _F0, _x1, _x2)]] 
  [[filter2(true, _F0, _x1, _x2)]] = 2 + x2 >= 2 + x2 = [[cons(_x1, filter(_F0, _x2))]] 
  [[filter2(false, _F0, _x1, _x2)]] = 2 + x2 >= x2 = [[filter(_F0, _x2)]] 

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:

  D#(!facplus(X, Y)) =#> D#(X)   
  D#(!facplus(X, Y)) =#> D#(Y)   
  D#(!factimes(X, Y)) =#> D#(X)   
  D#(!factimes(X, Y)) =#> D#(Y)   
  D#(!facminus(X, Y)) =#> D#(X)   
  D#(!facminus(X, Y)) =#> D#(Y)   
  D#(minus(X)) =#> D#(X)   
  D#(div(X, Y)) =#> D#(X)   
  D#(div(X, Y)) =#> D#(Y)   
  D#(ln(X)) =#> D#(X)   
  D#(pow(X, Y)) =#> D#(X)   
  D#(pow(X, Y)) =#> D#(Y)   
  filter#(F, cons(X, Y)) =#> filter2#(F X, F, X, Y)   
  filter2#(true, F, X, Y) =#> filter#(F, Y)   
  filter2#(false, F, X, Y) =#> filter#(F, Y)   

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:

  D#(!facplus(X, Y)) >? D#(X) 
  D#(!facplus(X, Y)) >? D#(Y) 
  D#(!factimes(X, Y)) >? D#(X) 
  D#(!factimes(X, Y)) >? D#(Y) 
  D#(!facminus(X, Y)) >? D#(X) 
  D#(!facminus(X, Y)) >? D#(Y) 
  D#(minus(X)) >? D#(X) 
  D#(div(X, Y)) >? D#(X) 
  D#(div(X, Y)) >? D#(Y) 
  D#(ln(X)) >? D#(X) 
  D#(pow(X, Y)) >? D#(X) 
  D#(pow(X, Y)) >? D#(Y) 
  filter#(F, cons(X, Y)) >? filter2#(F X, F, X, Y) 
  filter2#(true, F, X, Y) >? filter#(F, Y) 
  filter2#(false, F, X, Y) >? filter#(F, Y) 
  D(t) >= 1 
  D(constant) >= 0 
  D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) 
  D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) 
  D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) 
  D(minus(X)) >= minus(D(X)) 
  D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) 
  D(ln(X)) >= div(D(X), X) 
  D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) 
  map(F, nil) >= nil 
  map(F, cons(X, Y)) >= cons(F X, map(F, Y)) 
  filter(F, nil) >= nil 
  filter(F, cons(X, Y)) >= filter2(F X, F, X, Y) 
  filter2(true, F, X, Y) >= cons(X, filter(F, Y)) 
  filter2(false, F, X, Y) >= filter(F, Y) 

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

The following interpretation satisfies the requirements:

  !facminus = \y0y1.0 
  !facplus = \y0y1.0 
  !factimes = \y0y1.0 
  0 = 0 
  1 = 0 
  2 = 0 
  D = \y0.2 
  D# = \y0.0 
  cons = \y0y1.3 + y0 + 2y1 
  constant = 3 
  div = \y0y1.0 
  false = 3 
  filter = \G0y1.y1 + y1G0(y1) 
  filter2 = \y0G1y2y3.2 + y0 + y2 + 2y3 + 2y3G1(y3) 
  filter2# = \y0G1y2y3.1 + 2y3 
  filter# = \G0y1.2y1 
  ln = \y0.0 
  map = \G0y1.y1 + 3y1G0(y1) 
  minus = \y0.0 
  nil = 0 
  pow = \y0y1.0 
  t = 3 
  true = 3 

Using this interpretation, the requirements translate to:

  [[D#(!facplus(_x0, _x1))]] = 0 >= 0 = [[D#(_x0)]] 
  [[D#(!facplus(_x0, _x1))]] = 0 >= 0 = [[D#(_x1)]] 
  [[D#(!factimes(_x0, _x1))]] = 0 >= 0 = [[D#(_x0)]] 
  [[D#(!factimes(_x0, _x1))]] = 0 >= 0 = [[D#(_x1)]] 
  [[D#(!facminus(_x0, _x1))]] = 0 >= 0 = [[D#(_x0)]] 
  [[D#(!facminus(_x0, _x1))]] = 0 >= 0 = [[D#(_x1)]] 
  [[D#(minus(_x0))]] = 0 >= 0 = [[D#(_x0)]] 
  [[D#(div(_x0, _x1))]] = 0 >= 0 = [[D#(_x0)]] 
  [[D#(div(_x0, _x1))]] = 0 >= 0 = [[D#(_x1)]] 
  [[D#(ln(_x0))]] = 0 >= 0 = [[D#(_x0)]] 
  [[D#(pow(_x0, _x1))]] = 0 >= 0 = [[D#(_x0)]] 
  [[D#(pow(_x0, _x1))]] = 0 >= 0 = [[D#(_x1)]] 
  [[filter#(_F0, cons(_x1, _x2))]] = 6 + 2x1 + 4x2 > 1 + 2x2 = [[filter2#(_F0 _x1, _F0, _x1, _x2)]] 
  [[filter2#(true, _F0, _x1, _x2)]] = 1 + 2x2 > 2x2 = [[filter#(_F0, _x2)]] 
  [[filter2#(false, _F0, _x1, _x2)]] = 1 + 2x2 > 2x2 = [[filter#(_F0, _x2)]] 
  [[D(t)]] = 2 >= 0 = [[1]] 
  [[D(constant)]] = 2 >= 0 = [[0]] 
  [[D(!facplus(_x0, _x1))]] = 2 >= 0 = [[!facplus(D(_x0), D(_x1))]] 
  [[D(!factimes(_x0, _x1))]] = 2 >= 0 = [[!facplus(!factimes(_x1, D(_x0)), !factimes(_x0, D(_x1)))]] 
  [[D(!facminus(_x0, _x1))]] = 2 >= 0 = [[!facminus(D(_x0), D(_x1))]] 
  [[D(minus(_x0))]] = 2 >= 0 = [[minus(D(_x0))]] 
  [[D(div(_x0, _x1))]] = 2 >= 0 = [[!facminus(div(D(_x0), _x1), div(!factimes(_x0, D(_x1)), pow(_x1, 2)))]] 
  [[D(ln(_x0))]] = 2 >= 0 = [[div(D(_x0), _x0)]] 
  [[D(pow(_x0, _x1))]] = 2 >= 0 = [[!facplus(!factimes(!factimes(_x1, pow(_x0, !facminus(_x1, 1))), D(_x0)), !factimes(!factimes(pow(_x0, _x1), ln(_x0)), D(_x1)))]] 
  [[map(_F0, nil)]] = 0 >= 0 = [[nil]] 
  [[map(_F0, cons(_x1, _x2))]] = 3 + x1 + 2x2 + 3x1F0(3 + x1 + 2x2) + 6x2F0(3 + x1 + 2x2) + 9F0(3 + x1 + 2x2) >= 3 + 2x2 + F0(x1) + 6x2F0(x2) = [[cons(_F0 _x1, map(_F0, _x2))]] 
  [[filter(_F0, nil)]] = 0 >= 0 = [[nil]] 
  [[filter(_F0, cons(_x1, _x2))]] = 3 + x1 + 2x2 + 2x2F0(3 + x1 + 2x2) + 3F0(3 + x1 + 2x2) + x1F0(3 + x1 + 2x2) >= 2 + x1 + 2x2 + F0(x1) + 2x2F0(x2) = [[filter2(_F0 _x1, _F0, _x1, _x2)]] 
  [[filter2(true, _F0, _x1, _x2)]] = 5 + x1 + 2x2 + 2x2F0(x2) >= 3 + x1 + 2x2 + 2x2F0(x2) = [[cons(_x1, filter(_F0, _x2))]] 
  [[filter2(false, _F0, _x1, _x2)]] = 5 + x1 + 2x2 + 2x2F0(x2) >= x2 + x2F0(x2) = [[filter(_F0, _x2)]] 

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:

  D#(!facplus(X, Y)) =#> D#(X)   
  D#(!facplus(X, Y)) =#> D#(Y)   
  D#(!factimes(X, Y)) =#> D#(X)   
  D#(!factimes(X, Y)) =#> D#(Y)   
  D#(!facminus(X, Y)) =#> D#(X)   
  D#(!facminus(X, Y)) =#> D#(Y)   
  D#(minus(X)) =#> D#(X)   
  D#(div(X, Y)) =#> D#(X)   
  D#(div(X, Y)) =#> D#(Y)   
  D#(ln(X)) =#> D#(X)   
  D#(pow(X, Y)) =#> D#(X)   
  D#(pow(X, Y)) =#> D#(Y)   

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:

  D#(!facplus(X, Y)) >? D#(X) 
  D#(!facplus(X, Y)) >? D#(Y) 
  D#(!factimes(X, Y)) >? D#(X) 
  D#(!factimes(X, Y)) >? D#(Y) 
  D#(!facminus(X, Y)) >? D#(X) 
  D#(!facminus(X, Y)) >? D#(Y) 
  D#(minus(X)) >? D#(X) 
  D#(div(X, Y)) >? D#(X) 
  D#(div(X, Y)) >? D#(Y) 
  D#(ln(X)) >? D#(X) 
  D#(pow(X, Y)) >? D#(X) 
  D#(pow(X, Y)) >? D#(Y) 
  D(t) >= 1 
  D(constant) >= 0 
  D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) 
  D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) 
  D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) 
  D(minus(X)) >= minus(D(X)) 
  D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) 
  D(ln(X)) >= div(D(X), X) 
  D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) 
  map(F, nil) >= nil 
  map(F, cons(X, Y)) >= cons(F X, map(F, Y)) 
  filter(F, nil) >= nil 
  filter(F, cons(X, Y)) >= filter2(F X, F, X, Y) 
  filter2(true, F, X, Y) >= cons(X, filter(F, Y)) 
  filter2(false, F, X, Y) >= filter(F, Y) 

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]] = _|_ 
  [[1]] = _|_ 
  [[2]] = _|_ 
  [[filter(x_1, x_2)]] = filter(x_2) 
  [[filter2(x_1, x_2, x_3, x_4)]] = filter2(x_3, x_4) 
  [[minus(x_1)]] = x_1 
  [[nil]] = _|_ 

We choose Lex = {} and Mul = {!facminus, !facplus, !factimes, @_{o -> o}, D, D#, cons, constant, div, false, filter, filter2, ln, map, pow, t, true}, and the following precedence: false > t > constant > D > map > filter = filter2 > div > @_{o -> o} > cons > ln > pow > !factimes > !facplus > D# > !facminus > true

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

  D#(!facplus(X, Y)) >= D#(X) 
  D#(!facplus(X, Y)) >= D#(Y) 
  D#(!factimes(X, Y)) >= D#(X) 
  D#(!factimes(X, Y)) >= D#(Y) 
  D#(!facminus(X, Y)) >= D#(X) 
  D#(!facminus(X, Y)) > D#(Y) 
  D#(X) >= D#(X) 
  D#(div(X, Y)) >= D#(X) 
  D#(div(X, Y)) >= D#(Y) 
  D#(ln(X)) >= D#(X) 
  D#(pow(X, Y)) >= D#(X) 
  D#(pow(X, Y)) >= D#(Y) 
  D(t) >= _|_ 
  D(constant) >= _|_ 
  D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) 
  D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) 
  D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) 
  D(X) >= D(X) 
  D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, _|_))) 
  D(ln(X)) >= div(D(X), X) 
  D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, _|_))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) 
  map(F, _|_) >= _|_ 
  map(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) 
  filter(_|_) >= _|_ 
  filter(cons(X, Y)) >= filter2(X, Y) 
  filter2(X, Y) >= cons(X, filter(Y)) 
  filter2(X, Y) >= filter(Y) 

With these choices, we have:

  1] D#(!facplus(X, Y)) >= D#(X)  because D# in Mul and [2], by (Fun) 
  2] !facplus(X, Y) >= X  because [3], by (Star) 
  3] !facplus*(X, Y) >= X  because [4], by (Select) 
  4] X >= X  by (Meta) 

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

  9] D#(!factimes(X, Y)) >= D#(X)  because D# in Mul and [10], by (Fun) 
  10] !factimes(X, Y) >= X  because [11], by (Star) 
  11] !factimes*(X, Y) >= X  because [12], by (Select) 
  12] X >= X  by (Meta) 

  13] D#(!factimes(X, Y)) >= D#(Y)  because D# in Mul and [14], by (Fun) 
  14] !factimes(X, Y) >= Y  because [15], by (Star) 
  15] !factimes*(X, Y) >= Y  because [16], by (Select) 
  16] Y >= Y  by (Meta) 

  17] D#(!facminus(X, Y)) >= D#(X)  because D# in Mul and [18], by (Fun) 
  18] !facminus(X, Y) >= X  because [19], by (Star) 
  19] !facminus*(X, Y) >= X  because [20], by (Select) 
  20] X >= X  by (Meta) 

  21] D#(!facminus(X, Y)) > D#(Y)  because [22], by definition 
  22] D#*(!facminus(X, Y)) >= D#(Y)  because D# in Mul and [23], by (Stat) 
  23] !facminus(X, Y) > Y  because [24], by definition 
  24] !facminus*(X, Y) >= Y  because [25], by (Select) 
  25] Y >= Y  by (Meta) 

  26] D#(X) >= D#(X)  because D# in Mul and [27], by (Fun) 
  27] X >= X  by (Meta) 

  28] D#(div(X, Y)) >= D#(X)  because D# in Mul and [29], by (Fun) 
  29] div(X, Y) >= X  because [30], by (Star) 
  30] div*(X, Y) >= X  because [31], by (Select) 
  31] X >= X  by (Meta) 

  32] D#(div(X, Y)) >= D#(Y)  because D# in Mul and [33], by (Fun) 
  33] div(X, Y) >= Y  because [34], by (Star) 
  34] div*(X, Y) >= Y  because [35], by (Select) 
  35] Y >= Y  by (Meta) 

  36] D#(ln(X)) >= D#(X)  because D# in Mul and [37], by (Fun) 
  37] ln(X) >= X  because [38], by (Star) 
  38] ln*(X) >= X  because [39], by (Select) 
  39] X >= X  by (Meta) 

  40] D#(pow(X, Y)) >= D#(X)  because D# in Mul and [41], by (Fun) 
  41] pow(X, Y) >= X  because [42], by (Star) 
  42] pow*(X, Y) >= X  because [43], by (Select) 
  43] X >= X  by (Meta) 

  44] D#(pow(X, Y)) >= D#(Y)  because D# in Mul and [45], by (Fun) 
  45] pow(X, Y) >= Y  because [46], by (Star) 
  46] pow*(X, Y) >= Y  because [47], by (Select) 
  47] Y >= Y  by (Meta) 

  48] D(t) >= _|_  by (Bot) 

  49] D(constant) >= _|_  by (Bot) 

  50] D(!facplus(X, Y)) >= !facplus(D(X), D(Y))  because [51], by (Star) 
  51] D*(!facplus(X, Y)) >= !facplus(D(X), D(Y))  because D > !facplus, [52] and [55], by (Copy) 
  52] D*(!facplus(X, Y)) >= D(X)  because D in Mul and [53], by (Stat) 
  53] !facplus(X, Y) > X  because [54], by definition 
  54] !facplus*(X, Y) >= X  because [4], by (Select) 
  55] D*(!facplus(X, Y)) >= D(Y)  because D in Mul and [56], by (Stat) 
  56] !facplus(X, Y) > Y  because [57], by definition 
  57] !facplus*(X, Y) >= Y  because [8], by (Select) 

  58] D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y)))  because [59], by (Star) 
  59] D*(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y)))  because D > !facplus, [60] and [65], by (Copy) 
  60] D*(!factimes(X, Y)) >= !factimes(Y, D(X))  because D > !factimes, [61] and [62], by (Copy) 
  61] D*(!factimes(X, Y)) >= Y  because [14], by (Select) 
  62] D*(!factimes(X, Y)) >= D(X)  because D in Mul and [63], by (Stat) 
  63] !factimes(X, Y) > X  because [64], by definition 
  64] !factimes*(X, Y) >= X  because [12], by (Select) 
  65] D*(!factimes(X, Y)) >= !factimes(X, D(Y))  because D > !factimes, [66] and [67], by (Copy) 
  66] D*(!factimes(X, Y)) >= X  because [10], by (Select) 
  67] D*(!factimes(X, Y)) >= D(Y)  because D in Mul and [68], by (Stat) 
  68] !factimes(X, Y) > Y  because [69], by definition 
  69] !factimes*(X, Y) >= Y  because [16], by (Select) 

  70] D(!facminus(X, Y)) >= !facminus(D(X), D(Y))  because [71], by (Star) 
  71] D*(!facminus(X, Y)) >= !facminus(D(X), D(Y))  because D > !facminus, [72] and [75], by (Copy) 
  72] D*(!facminus(X, Y)) >= D(X)  because D in Mul and [73], by (Stat) 
  73] !facminus(X, Y) > X  because [74], by definition 
  74] !facminus*(X, Y) >= X  because [20], by (Select) 
  75] D*(!facminus(X, Y)) >= D(Y)  because D in Mul and [23], by (Stat) 

  76] D(X) >= D(X)  because D in Mul and [27], by (Fun) 

  77] D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, _|_)))  because [78], by (Star) 
  78] D*(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, _|_)))  because D > !facminus, [79] and [84], by (Copy) 
  79] D*(div(X, Y)) >= div(D(X), Y)  because D > div, [80] and [83], by (Copy) 
  80] D*(div(X, Y)) >= D(X)  because D in Mul and [81], by (Stat) 
  81] div(X, Y) > X  because [82], by definition 
  82] div*(X, Y) >= X  because [31], by (Select) 
  83] D*(div(X, Y)) >= Y  because [33], by (Select) 
  84] D*(div(X, Y)) >= div(!factimes(X, D(Y)), pow(Y, _|_))  because D > div, [85] and [90], by (Copy) 
  85] D*(div(X, Y)) >= !factimes(X, D(Y))  because D > !factimes, [86] and [87], by (Copy) 
  86] D*(div(X, Y)) >= X  because [29], by (Select) 
  87] D*(div(X, Y)) >= D(Y)  because D in Mul and [88], by (Stat) 
  88] div(X, Y) > Y  because [89], by definition 
  89] div*(X, Y) >= Y  because [35], by (Select) 
  90] D*(div(X, Y)) >= pow(Y, _|_)  because [91], by (Select) 
  91] div(X, Y) >= pow(Y, _|_)  because [92], by (Star) 
  92] div*(X, Y) >= pow(Y, _|_)  because div > pow, [89] and [93], by (Copy) 
  93] div*(X, Y) >= _|_  by (Bot) 

  94] D(ln(X)) >= div(D(X), X)  because [95], by (Star) 
  95] D*(ln(X)) >= div(D(X), X)  because D > div, [96] and [99], by (Copy) 
  96] D*(ln(X)) >= D(X)  because D in Mul and [97], by (Stat) 
  97] ln(X) > X  because [98], by definition 
  98] ln*(X) >= X  because [39], by (Select) 
  99] D*(ln(X)) >= X  because [37], by (Select) 

  100] D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, _|_))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y)))  because [101], by (Star) 
  101] D*(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, _|_))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y)))  because D > !facplus, [102] and [115], by (Copy) 
  102] D*(pow(X, Y)) >= !factimes(!factimes(Y, pow(X, !facminus(Y, _|_))), D(X))  because D > !factimes, [103] and [112], by (Copy) 
  103] D*(pow(X, Y)) >= !factimes(Y, pow(X, !facminus(Y, _|_)))  because D > !factimes, [104] and [105], by (Copy) 
  104] D*(pow(X, Y)) >= Y  because [45], by (Select) 
  105] D*(pow(X, Y)) >= pow(X, !facminus(Y, _|_))  because D > pow, [106] and [107], by (Copy) 
  106] D*(pow(X, Y)) >= X  because [41], by (Select) 
  107] D*(pow(X, Y)) >= !facminus(Y, _|_)  because [108], by (Select) 
  108] pow(X, Y) >= !facminus(Y, _|_)  because [109], by (Star) 
  109] pow*(X, Y) >= !facminus(Y, _|_)  because pow > !facminus, [110] and [111], by (Copy) 
  110] pow*(X, Y) >= Y  because [47], by (Select) 
  111] pow*(X, Y) >= _|_  by (Bot) 
  112] D*(pow(X, Y)) >= D(X)  because D in Mul and [113], by (Stat) 
  113] pow(X, Y) > X  because [114], by definition 
  114] pow*(X, Y) >= X  because [43], by (Select) 
  115] D*(pow(X, Y)) >= !factimes(!factimes(pow(X, Y), ln(X)), D(Y))  because D > !factimes, [116] and [119], by (Copy) 
  116] D*(pow(X, Y)) >= !factimes(pow(X, Y), ln(X))  because D > !factimes, [117] and [118], by (Copy) 
  117] D*(pow(X, Y)) >= pow(X, Y)  because D > pow, [106] and [104], by (Copy) 
  118] D*(pow(X, Y)) >= ln(X)  because D > ln and [106], by (Copy) 
  119] D*(pow(X, Y)) >= D(Y)  because D in Mul and [120], by (Stat) 
  120] pow(X, Y) > Y  because [110], by definition 

  121] map(F, _|_) >= _|_  by (Bot) 

  122] map(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y))  because [123], by (Star) 
  123] map*(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y))  because map > cons, [124] and [131], by (Copy) 
  124] map*(F, cons(X, Y)) >= @_{o -> o}(F, X)  because map > @_{o -> o}, [125] and [127], by (Copy) 
  125] map*(F, cons(X, Y)) >= F  because [126], by (Select) 
  126] F >= F  by (Meta) 
  127] map*(F, cons(X, Y)) >= X  because [128], by (Select) 
  128] cons(X, Y) >= X  because [129], by (Star) 
  129] cons*(X, Y) >= X  because [130], by (Select) 
  130] X >= X  by (Meta) 
  131] map*(F, cons(X, Y)) >= map(F, Y)  because map in Mul, [132] and [133], by (Stat) 
  132] F >= F  by (Meta) 
  133] cons(X, Y) > Y  because [134], by definition 
  134] cons*(X, Y) >= Y  because [135], by (Select) 
  135] Y >= Y  by (Meta) 

  136] filter(_|_) >= _|_  by (Bot) 

  137] filter(cons(X, Y)) >= filter2(X, Y)  because [138], by (Star) 
  138] filter*(cons(X, Y)) >= filter2(X, Y)  because filter = filter2, filter in Mul, [139] and [142], by (Stat) 
  139] cons(X, Y) > X  because [140], by definition 
  140] cons*(X, Y) >= X  because [141], by (Select) 
  141] X >= X  by (Meta) 
  142] cons(X, Y) > Y  because [143], by definition 
  143] cons*(X, Y) >= Y  because [144], by (Select) 
  144] Y >= Y  by (Meta) 

  145] filter2(X, Y) >= cons(X, filter(Y))  because [146], by (Star) 
  146] filter2*(X, Y) >= cons(X, filter(Y))  because filter2 > cons, [147] and [149], by (Copy) 
  147] filter2*(X, Y) >= X  because [148], by (Select) 
  148] X >= X  by (Meta) 
  149] filter2*(X, Y) >= filter(Y)  because filter2 = filter, filter2 in Mul and [150], by (Stat) 
  150] Y >= Y  by (Meta) 

  151] filter2(X, Y) >= filter(Y)  because [152], by (Star) 
  152] filter2*(X, Y) >= filter(Y)  because filter2 = filter, filter2 in Mul and [153], by (Stat) 
  153] Y >= Y  by (Meta) 

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

  D#(!facplus(X, Y)) =#> D#(X)   
  D#(!facplus(X, Y)) =#> D#(Y)   
  D#(!factimes(X, Y)) =#> D#(X)   
  D#(!factimes(X, Y)) =#> D#(Y)   
  D#(!facminus(X, Y)) =#> D#(X)   
  D#(minus(X)) =#> D#(X)   
  D#(div(X, Y)) =#> D#(X)   
  D#(div(X, Y)) =#> D#(Y)   
  D#(ln(X)) =#> D#(X)   
  D#(pow(X, Y)) =#> D#(X)   
  D#(pow(X, Y)) =#> D#(Y)   

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:

  D#(!facplus(X, Y)) >? D#(X) 
  D#(!facplus(X, Y)) >? D#(Y) 
  D#(!factimes(X, Y)) >? D#(X) 
  D#(!factimes(X, Y)) >? D#(Y) 
  D#(!facminus(X, Y)) >? D#(X) 
  D#(minus(X)) >? D#(X) 
  D#(div(X, Y)) >? D#(X) 
  D#(div(X, Y)) >? D#(Y) 
  D#(ln(X)) >? D#(X) 
  D#(pow(X, Y)) >? D#(X) 
  D#(pow(X, Y)) >? D#(Y) 
  D(t) >= 1 
  D(constant) >= 0 
  D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) 
  D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) 
  D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) 
  D(minus(X)) >= minus(D(X)) 
  D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) 
  D(ln(X)) >= div(D(X), X) 
  D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) 
  map(F, nil) >= nil 
  map(F, cons(X, Y)) >= cons(F X, map(F, Y)) 
  filter(F, nil) >= nil 
  filter(F, cons(X, Y)) >= filter2(F X, F, X, Y) 
  filter2(true, F, X, Y) >= cons(X, filter(F, Y)) 
  filter2(false, F, X, Y) >= filter(F, Y) 

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:

  [[!facminus(x_1, x_2)]] = x_1 
  [[0]] = _|_ 
  [[1]] = _|_ 
  [[2]] = _|_ 
  [[cons(x_1, x_2)]] = _|_ 
  [[filter(x_1, x_2)]] = _|_ 
  [[filter2(x_1, x_2, x_3, x_4)]] = _|_ 
  [[minus(x_1)]] = x_1 
  [[nil]] = _|_ 

We choose Lex = {} and Mul = {!facplus, !factimes, @_{o -> o}, D, D#, constant, div, false, ln, map, pow, t, true}, and the following precedence: constant > @_{o -> o} > map > pow > ln > t > true > D > !facplus > div > !factimes > D# > false

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

  D#(!facplus(X, Y)) >= D#(X) 
  D#(!facplus(X, Y)) > D#(Y) 
  D#(!factimes(X, Y)) >= D#(X) 
  D#(!factimes(X, Y)) >= D#(Y) 
  D#(X) >= D#(X) 
  D#(X) >= D#(X) 
  D#(div(X, Y)) >= D#(X) 
  D#(div(X, Y)) >= D#(Y) 
  D#(ln(X)) >= D#(X) 
  D#(pow(X, Y)) >= D#(X) 
  D#(pow(X, Y)) >= D#(Y) 
  D(t) >= _|_ 
  D(constant) >= _|_ 
  D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) 
  D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) 
  D(X) >= D(X) 
  D(X) >= D(X) 
  D(div(X, Y)) >= div(D(X), Y) 
  D(ln(X)) >= div(D(X), X) 
  D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, Y)), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) 
  map(F, _|_) >= _|_ 
  map(F, _|_) >= _|_ 
  _|_ >= _|_ 
  _|_ >= _|_ 
  _|_ >= _|_ 
  _|_ >= _|_ 

With these choices, we have:

  1] D#(!facplus(X, Y)) >= D#(X)  because D# in Mul and [2], by (Fun) 
  2] !facplus(X, Y) >= X  because [3], by (Star) 
  3] !facplus*(X, Y) >= X  because [4], by (Select) 
  4] X >= X  by (Meta) 

  5] D#(!facplus(X, Y)) > D#(Y)  because [6], by definition 
  6] D#*(!facplus(X, Y)) >= D#(Y)  because D# in Mul and [7], by (Stat) 
  7] !facplus(X, Y) > Y  because [8], by definition 
  8] !facplus*(X, Y) >= Y  because [9], by (Select) 
  9] Y >= Y  by (Meta) 

  10] D#(!factimes(X, Y)) >= D#(X)  because D# in Mul and [11], by (Fun) 
  11] !factimes(X, Y) >= X  because [12], by (Star) 
  12] !factimes*(X, Y) >= X  because [13], by (Select) 
  13] X >= X  by (Meta) 

  14] D#(!factimes(X, Y)) >= D#(Y)  because D# in Mul and [15], by (Fun) 
  15] !factimes(X, Y) >= Y  because [16], by (Star) 
  16] !factimes*(X, Y) >= Y  because [17], by (Select) 
  17] Y >= Y  by (Meta) 

  18] D#(X) >= D#(X)  because D# in Mul and [19], by (Fun) 
  19] X >= X  by (Meta) 

  20] D#(X) >= D#(X)  because D# in Mul and [21], by (Fun) 
  21] X >= X  by (Meta) 

  22] D#(div(X, Y)) >= D#(X)  because D# in Mul and [23], by (Fun) 
  23] div(X, Y) >= X  because [24], by (Star) 
  24] div*(X, Y) >= X  because [25], by (Select) 
  25] X >= X  by (Meta) 

  26] D#(div(X, Y)) >= D#(Y)  because [27], by (Star) 
  27] D#*(div(X, Y)) >= D#(Y)  because [28], by (Select) 
  28] div(X, Y) >= D#(Y)  because [29], by (Star) 
  29] div*(X, Y) >= D#(Y)  because div > D# and [30], by (Copy) 
  30] div*(X, Y) >= Y  because [31], by (Select) 
  31] Y >= Y  by (Meta) 

  32] D#(ln(X)) >= D#(X)  because D# in Mul and [33], by (Fun) 
  33] ln(X) >= X  because [34], by (Star) 
  34] ln*(X) >= X  because [35], by (Select) 
  35] X >= X  by (Meta) 

  36] D#(pow(X, Y)) >= D#(X)  because D# in Mul and [37], by (Fun) 
  37] pow(X, Y) >= X  because [38], by (Star) 
  38] pow*(X, Y) >= X  because [39], by (Select) 
  39] X >= X  by (Meta) 

  40] D#(pow(X, Y)) >= D#(Y)  because [41], by (Star) 
  41] D#*(pow(X, Y)) >= D#(Y)  because [42], by (Select) 
  42] pow(X, Y) >= D#(Y)  because [43], by (Star) 
  43] pow*(X, Y) >= D#(Y)  because pow > D# and [44], by (Copy) 
  44] pow*(X, Y) >= Y  because [45], by (Select) 
  45] Y >= Y  by (Meta) 

  46] D(t) >= _|_  by (Bot) 

  47] D(constant) >= _|_  by (Bot) 

  48] D(!facplus(X, Y)) >= !facplus(D(X), D(Y))  because [49], by (Star) 
  49] D*(!facplus(X, Y)) >= !facplus(D(X), D(Y))  because D > !facplus, [50] and [53], by (Copy) 
  50] D*(!facplus(X, Y)) >= D(X)  because D in Mul and [51], by (Stat) 
  51] !facplus(X, Y) > X  because [52], by definition 
  52] !facplus*(X, Y) >= X  because [4], by (Select) 
  53] D*(!facplus(X, Y)) >= D(Y)  because D in Mul and [7], by (Stat) 

  54] D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y)))  because [55], by (Star) 
  55] D*(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y)))  because D > !facplus, [56] and [61], by (Copy) 
  56] D*(!factimes(X, Y)) >= !factimes(Y, D(X))  because D > !factimes, [57] and [58], by (Copy) 
  57] D*(!factimes(X, Y)) >= Y  because [15], by (Select) 
  58] D*(!factimes(X, Y)) >= D(X)  because D in Mul and [59], by (Stat) 
  59] !factimes(X, Y) > X  because [60], by definition 
  60] !factimes*(X, Y) >= X  because [13], by (Select) 
  61] D*(!factimes(X, Y)) >= !factimes(X, D(Y))  because D > !factimes, [62] and [63], by (Copy) 
  62] D*(!factimes(X, Y)) >= X  because [11], by (Select) 
  63] D*(!factimes(X, Y)) >= D(Y)  because D in Mul and [64], by (Stat) 
  64] !factimes(X, Y) > Y  because [65], by definition 
  65] !factimes*(X, Y) >= Y  because [17], by (Select) 

  66] D(X) >= D(X)  because D in Mul and [19], by (Fun) 

  67] D(X) >= D(X)  because D in Mul and [21], by (Fun) 

  68] D(div(X, Y)) >= div(D(X), Y)  because [69], by (Star) 
  69] D*(div(X, Y)) >= div(D(X), Y)  because D > div, [70] and [73], by (Copy) 
  70] D*(div(X, Y)) >= D(X)  because D in Mul and [71], by (Stat) 
  71] div(X, Y) > X  because [72], by definition 
  72] div*(X, Y) >= X  because [25], by (Select) 
  73] D*(div(X, Y)) >= Y  because [74], by (Select) 
  74] div(X, Y) >= Y  because [30], by (Star) 

  75] D(ln(X)) >= div(D(X), X)  because [76], by (Star) 
  76] D*(ln(X)) >= div(D(X), X)  because D > div, [77] and [80], by (Copy) 
  77] D*(ln(X)) >= D(X)  because D in Mul and [78], by (Stat) 
  78] ln(X) > X  because [79], by definition 
  79] ln*(X) >= X  because [35], by (Select) 
  80] D*(ln(X)) >= X  because [33], by (Select) 

  81] D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, Y)), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y)))  because [82], by (Star) 
  82] D*(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, Y)), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y)))  because D > !facplus, [83] and [95], by (Copy) 
  83] D*(pow(X, Y)) >= !factimes(!factimes(Y, pow(X, Y)), D(X))  because D > !factimes, [84] and [91], by (Copy) 
  84] D*(pow(X, Y)) >= !factimes(Y, pow(X, Y))  because D > !factimes, [85] and [87], by (Copy) 
  85] D*(pow(X, Y)) >= Y  because [86], by (Select) 
  86] pow(X, Y) >= Y  because [44], by (Star) 
  87] D*(pow(X, Y)) >= pow(X, Y)  because [88], by (Select) 
  88] pow(X, Y) >= pow(X, Y)  because pow in Mul, [89] and [90], by (Fun) 
  89] X >= X  by (Meta) 
  90] Y >= Y  by (Meta) 
  91] D*(pow(X, Y)) >= D(X)  because [92], by (Select) 
  92] pow(X, Y) >= D(X)  because [93], by (Star) 
  93] pow*(X, Y) >= D(X)  because pow > D and [94], by (Copy) 
  94] pow*(X, Y) >= X  because [89], by (Select) 
  95] D*(pow(X, Y)) >= !factimes(!factimes(pow(X, Y), ln(X)), D(Y))  because D > !factimes, [96] and [102], by (Copy) 
  96] D*(pow(X, Y)) >= !factimes(pow(X, Y), ln(X))  because D > !factimes, [97] and [99], by (Copy) 
  97] D*(pow(X, Y)) >= pow(X, Y)  because [98], by (Select) 
  98] pow(X, Y) >= pow(X, Y)  because pow in Mul, [89] and [90], by (Fun) 
  99] D*(pow(X, Y)) >= ln(X)  because [100], by (Select) 
  100] pow(X, Y) >= ln(X)  because [101], by (Star) 
  101] pow*(X, Y) >= ln(X)  because pow > ln and [94], by (Copy) 
  102] D*(pow(X, Y)) >= D(Y)  because [103], by (Select) 
  103] pow(X, Y) >= D(Y)  because [104], by (Star) 
  104] pow*(X, Y) >= D(Y)  because pow > D and [44], by (Copy) 

  105] map(F, _|_) >= _|_  by (Bot) 

  106] map(F, _|_) >= _|_  by (Bot) 

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

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

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

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

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:

  D#(!facplus(X, Y)) =#> D#(X)   
  D#(!factimes(X, Y)) =#> D#(X)   
  D#(!factimes(X, Y)) =#> D#(Y)   
  D#(!facminus(X, Y)) =#> D#(X)   
  D#(minus(X)) =#> D#(X)   
  D#(div(X, Y)) =#> D#(X)   
  D#(div(X, Y)) =#> D#(Y)   
  D#(ln(X)) =#> D#(X)   
  D#(pow(X, Y)) =#> D#(X)   
  D#(pow(X, Y)) =#> D#(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:

  D#(!facplus(X, Y)) >? D#(X) 
  D#(!factimes(X, Y)) >? D#(X) 
  D#(!factimes(X, Y)) >? D#(Y) 
  D#(!facminus(X, Y)) >? D#(X) 
  D#(minus(X)) >? D#(X) 
  D#(div(X, Y)) >? D#(X) 
  D#(div(X, Y)) >? D#(Y) 
  D#(ln(X)) >? D#(X) 
  D#(pow(X, Y)) >? D#(X) 
  D#(pow(X, Y)) >? D#(Y) 
  D(t) >= 1 
  D(constant) >= 0 
  D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) 
  D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) 
  D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) 
  D(minus(X)) >= minus(D(X)) 
  D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) 
  D(ln(X)) >= div(D(X), X) 
  D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) 
  map(F, nil) >= nil 
  map(F, cons(X, Y)) >= cons(F X, map(F, Y)) 
  filter(F, nil) >= nil 
  filter(F, cons(X, Y)) >= filter2(F X, F, X, Y) 
  filter2(true, F, X, Y) >= cons(X, filter(F, Y)) 
  filter2(false, F, X, Y) >= filter(F, Y) 

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

The following interpretation satisfies the requirements:

  !facminus = \y0y1.y0 
  !facplus = \y0y1.y0 
  !factimes = \y0y1.y0 + y1 
  0 = 0 
  1 = 0 
  2 = 0 
  D = \y0.2y0 
  D# = \y0.2y0 
  cons = \y0y1.0 
  constant = 3 
  div = \y0y1.y1 + 2y0 
  false = 3 
  filter = \G0y1.0 
  filter2 = \y0G1y2y3.0 
  ln = \y0.3 + 3y0 
  map = \G0y1.0 
  minus = \y0.1 + y0 
  nil = 0 
  pow = \y0y1.y1 + 2y0 
  t = 3 
  true = 3 

Using this interpretation, the requirements translate to:

  [[D#(!facplus(_x0, _x1))]] = 2x0 >= 2x0 = [[D#(_x0)]] 
  [[D#(!factimes(_x0, _x1))]] = 2x0 + 2x1 >= 2x0 = [[D#(_x0)]] 
  [[D#(!factimes(_x0, _x1))]] = 2x0 + 2x1 >= 2x1 = [[D#(_x1)]] 
  [[D#(!facminus(_x0, _x1))]] = 2x0 >= 2x0 = [[D#(_x0)]] 
  [[D#(minus(_x0))]] = 2 + 2x0 > 2x0 = [[D#(_x0)]] 
  [[D#(div(_x0, _x1))]] = 2x1 + 4x0 >= 2x0 = [[D#(_x0)]] 
  [[D#(div(_x0, _x1))]] = 2x1 + 4x0 >= 2x1 = [[D#(_x1)]] 
  [[D#(ln(_x0))]] = 6 + 6x0 > 2x0 = [[D#(_x0)]] 
  [[D#(pow(_x0, _x1))]] = 2x1 + 4x0 >= 2x0 = [[D#(_x0)]] 
  [[D#(pow(_x0, _x1))]] = 2x1 + 4x0 >= 2x1 = [[D#(_x1)]] 
  [[D(t)]] = 6 >= 0 = [[1]] 
  [[D(constant)]] = 6 >= 0 = [[0]] 
  [[D(!facplus(_x0, _x1))]] = 2x0 >= 2x0 = [[!facplus(D(_x0), D(_x1))]] 
  [[D(!factimes(_x0, _x1))]] = 2x0 + 2x1 >= x1 + 2x0 = [[!facplus(!factimes(_x1, D(_x0)), !factimes(_x0, D(_x1)))]] 
  [[D(!facminus(_x0, _x1))]] = 2x0 >= 2x0 = [[!facminus(D(_x0), D(_x1))]] 
  [[D(minus(_x0))]] = 2 + 2x0 >= 1 + 2x0 = [[minus(D(_x0))]] 
  [[D(div(_x0, _x1))]] = 2x1 + 4x0 >= x1 + 4x0 = [[!facminus(div(D(_x0), _x1), div(!factimes(_x0, D(_x1)), pow(_x1, 2)))]] 
  [[D(ln(_x0))]] = 6 + 6x0 >= 5x0 = [[div(D(_x0), _x0)]] 
  [[D(pow(_x0, _x1))]] = 2x1 + 4x0 >= 2x1 + 4x0 = [[!facplus(!factimes(!factimes(_x1, pow(_x0, !facminus(_x1, 1))), D(_x0)), !factimes(!factimes(pow(_x0, _x1), ln(_x0)), D(_x1)))]] 
  [[map(_F0, nil)]] = 0 >= 0 = [[nil]] 
  [[map(_F0, cons(_x1, _x2))]] = 0 >= 0 = [[cons(_F0 _x1, map(_F0, _x2))]] 
  [[filter(_F0, nil)]] = 0 >= 0 = [[nil]] 
  [[filter(_F0, cons(_x1, _x2))]] = 0 >= 0 = [[filter2(_F0 _x1, _F0, _x1, _x2)]] 
  [[filter2(true, _F0, _x1, _x2)]] = 0 >= 0 = [[cons(_x1, filter(_F0, _x2))]] 
  [[filter2(false, _F0, _x1, _x2)]] = 0 >= 0 = [[filter(_F0, _x2)]] 

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:

  D#(!facplus(X, Y)) =#> D#(X)   
  D#(!factimes(X, Y)) =#> D#(X)   
  D#(!factimes(X, Y)) =#> D#(Y)   
  D#(!facminus(X, Y)) =#> D#(X)   
  D#(div(X, Y)) =#> D#(X)   
  D#(div(X, Y)) =#> D#(Y)   
  D#(pow(X, Y)) =#> D#(X)   
  D#(pow(X, Y)) =#> D#(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:

  D#(!facplus(X, Y)) >? D#(X) 
  D#(!factimes(X, Y)) >? D#(X) 
  D#(!factimes(X, Y)) >? D#(Y) 
  D#(!facminus(X, Y)) >? D#(X) 
  D#(div(X, Y)) >? D#(X) 
  D#(div(X, Y)) >? D#(Y) 
  D#(pow(X, Y)) >? D#(X) 
  D#(pow(X, Y)) >? D#(Y) 
  D(t) >= 1 
  D(constant) >= 0 
  D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) 
  D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) 
  D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) 
  D(minus(X)) >= minus(D(X)) 
  D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) 
  D(ln(X)) >= div(D(X), X) 
  D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) 
  map(F, nil) >= nil 
  map(F, cons(X, Y)) >= cons(F X, map(F, Y)) 
  filter(F, nil) >= nil 
  filter(F, cons(X, Y)) >= filter2(F X, F, X, Y) 
  filter2(true, F, X, Y) >= cons(X, filter(F, Y)) 
  filter2(false, F, X, Y) >= filter(F, Y) 

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

The following interpretation satisfies the requirements:

  !facminus = \y0y1.y0 
  !facplus = \y0y1.y0 
  !factimes = \y0y1.y0 + y1 
  0 = 0 
  1 = 0 
  2 = 0 
  D = \y0.2y0 
  D# = \y0.y0 
  cons = \y0y1.0 
  constant = 3 
  div = \y0y1.1 + 2y0 + 2y1 
  false = 3 
  filter = \G0y1.0 
  filter2 = \y0G1y2y3.0 
  ln = \y0.3 + 3y0 
  map = \G0y1.0 
  minus = \y0.0 
  nil = 0 
  pow = \y0y1.y1 + 2y0 
  t = 3 
  true = 3 

Using this interpretation, the requirements translate to:

  [[D#(!facplus(_x0, _x1))]] = x0 >= x0 = [[D#(_x0)]] 
  [[D#(!factimes(_x0, _x1))]] = x0 + x1 >= x0 = [[D#(_x0)]] 
  [[D#(!factimes(_x0, _x1))]] = x0 + x1 >= x1 = [[D#(_x1)]] 
  [[D#(!facminus(_x0, _x1))]] = x0 >= x0 = [[D#(_x0)]] 
  [[D#(div(_x0, _x1))]] = 1 + 2x0 + 2x1 > x0 = [[D#(_x0)]] 
  [[D#(div(_x0, _x1))]] = 1 + 2x0 + 2x1 > x1 = [[D#(_x1)]] 
  [[D#(pow(_x0, _x1))]] = x1 + 2x0 >= x0 = [[D#(_x0)]] 
  [[D#(pow(_x0, _x1))]] = x1 + 2x0 >= x1 = [[D#(_x1)]] 
  [[D(t)]] = 6 >= 0 = [[1]] 
  [[D(constant)]] = 6 >= 0 = [[0]] 
  [[D(!facplus(_x0, _x1))]] = 2x0 >= 2x0 = [[!facplus(D(_x0), D(_x1))]] 
  [[D(!factimes(_x0, _x1))]] = 2x0 + 2x1 >= x1 + 2x0 = [[!facplus(!factimes(_x1, D(_x0)), !factimes(_x0, D(_x1)))]] 
  [[D(!facminus(_x0, _x1))]] = 2x0 >= 2x0 = [[!facminus(D(_x0), D(_x1))]] 
  [[D(minus(_x0))]] = 0 >= 0 = [[minus(D(_x0))]] 
  [[D(div(_x0, _x1))]] = 2 + 4x0 + 4x1 >= 1 + 2x1 + 4x0 = [[!facminus(div(D(_x0), _x1), div(!factimes(_x0, D(_x1)), pow(_x1, 2)))]] 
  [[D(ln(_x0))]] = 6 + 6x0 >= 1 + 6x0 = [[div(D(_x0), _x0)]] 
  [[D(pow(_x0, _x1))]] = 2x1 + 4x0 >= 2x1 + 4x0 = [[!facplus(!factimes(!factimes(_x1, pow(_x0, !facminus(_x1, 1))), D(_x0)), !factimes(!factimes(pow(_x0, _x1), ln(_x0)), D(_x1)))]] 
  [[map(_F0, nil)]] = 0 >= 0 = [[nil]] 
  [[map(_F0, cons(_x1, _x2))]] = 0 >= 0 = [[cons(_F0 _x1, map(_F0, _x2))]] 
  [[filter(_F0, nil)]] = 0 >= 0 = [[nil]] 
  [[filter(_F0, cons(_x1, _x2))]] = 0 >= 0 = [[filter2(_F0 _x1, _F0, _x1, _x2)]] 
  [[filter2(true, _F0, _x1, _x2)]] = 0 >= 0 = [[cons(_x1, filter(_F0, _x2))]] 
  [[filter2(false, _F0, _x1, _x2)]] = 0 >= 0 = [[filter(_F0, _x2)]] 

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

  D#(!facplus(X, Y)) =#> D#(X)   
  D#(!factimes(X, Y)) =#> D#(X)   
  D#(!factimes(X, Y)) =#> D#(Y)   
  D#(!facminus(X, Y)) =#> D#(X)   
  D#(pow(X, Y)) =#> D#(X)   
  D#(pow(X, Y)) =#> D#(Y)   

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

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

  D#(!facplus(X, Y)) >? D#(X) 
  D#(!factimes(X, Y)) >? D#(X) 
  D#(!factimes(X, Y)) >? D#(Y) 
  D#(!facminus(X, Y)) >? D#(X) 
  D#(pow(X, Y)) >? D#(X) 
  D#(pow(X, Y)) >? D#(Y) 
  D(t) >= 1 
  D(constant) >= 0 
  D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) 
  D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) 
  D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) 
  D(minus(X)) >= minus(D(X)) 
  D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) 
  D(ln(X)) >= div(D(X), X) 
  D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) 
  map(F, nil) >= nil 
  map(F, cons(X, Y)) >= cons(F X, map(F, Y)) 
  filter(F, nil) >= nil 
  filter(F, cons(X, Y)) >= filter2(F X, F, X, Y) 
  filter2(true, F, X, Y) >= cons(X, filter(F, Y)) 
  filter2(false, F, X, Y) >= filter(F, Y) 

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

The following interpretation satisfies the requirements:

  !facminus = \y0y1.y0 
  !facplus = \y0y1.y0 
  !factimes = \y0y1.y0 + y1 
  0 = 0 
  1 = 0 
  2 = 0 
  D = \y0.2y0 
  D# = \y0.2y0 
  cons = \y0y1.0 
  constant = 3 
  div = \y0y1.0 
  false = 3 
  filter = \G0y1.0 
  filter2 = \y0G1y2y3.0 
  ln = \y0.3 
  map = \G0y1.0 
  minus = \y0.0 
  nil = 0 
  pow = \y0y1.1 + 2y0 + 2y1 
  t = 3 
  true = 3 

Using this interpretation, the requirements translate to:

  [[D#(!facplus(_x0, _x1))]] = 2x0 >= 2x0 = [[D#(_x0)]] 
  [[D#(!factimes(_x0, _x1))]] = 2x0 + 2x1 >= 2x0 = [[D#(_x0)]] 
  [[D#(!factimes(_x0, _x1))]] = 2x0 + 2x1 >= 2x1 = [[D#(_x1)]] 
  [[D#(!facminus(_x0, _x1))]] = 2x0 >= 2x0 = [[D#(_x0)]] 
  [[D#(pow(_x0, _x1))]] = 2 + 4x0 + 4x1 > 2x0 = [[D#(_x0)]] 
  [[D#(pow(_x0, _x1))]] = 2 + 4x0 + 4x1 > 2x1 = [[D#(_x1)]] 
  [[D(t)]] = 6 >= 0 = [[1]] 
  [[D(constant)]] = 6 >= 0 = [[0]] 
  [[D(!facplus(_x0, _x1))]] = 2x0 >= 2x0 = [[!facplus(D(_x0), D(_x1))]] 
  [[D(!factimes(_x0, _x1))]] = 2x0 + 2x1 >= x1 + 2x0 = [[!facplus(!factimes(_x1, D(_x0)), !factimes(_x0, D(_x1)))]] 
  [[D(!facminus(_x0, _x1))]] = 2x0 >= 2x0 = [[!facminus(D(_x0), D(_x1))]] 
  [[D(minus(_x0))]] = 0 >= 0 = [[minus(D(_x0))]] 
  [[D(div(_x0, _x1))]] = 0 >= 0 = [[!facminus(div(D(_x0), _x1), div(!factimes(_x0, D(_x1)), pow(_x1, 2)))]] 
  [[D(ln(_x0))]] = 6 >= 0 = [[div(D(_x0), _x0)]] 
  [[D(pow(_x0, _x1))]] = 2 + 4x0 + 4x1 >= 1 + 3x1 + 4x0 = [[!facplus(!factimes(!factimes(_x1, pow(_x0, !facminus(_x1, 1))), D(_x0)), !factimes(!factimes(pow(_x0, _x1), ln(_x0)), D(_x1)))]] 
  [[map(_F0, nil)]] = 0 >= 0 = [[nil]] 
  [[map(_F0, cons(_x1, _x2))]] = 0 >= 0 = [[cons(_F0 _x1, map(_F0, _x2))]] 
  [[filter(_F0, nil)]] = 0 >= 0 = [[nil]] 
  [[filter(_F0, cons(_x1, _x2))]] = 0 >= 0 = [[filter2(_F0 _x1, _F0, _x1, _x2)]] 
  [[filter2(true, _F0, _x1, _x2)]] = 0 >= 0 = [[cons(_x1, filter(_F0, _x2))]] 
  [[filter2(false, _F0, _x1, _x2)]] = 0 >= 0 = [[filter(_F0, _x2)]] 

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

  D#(!facplus(X, Y)) =#> D#(X)   
  D#(!factimes(X, Y)) =#> D#(X)   
  D#(!factimes(X, Y)) =#> D#(Y)   
  D#(!facminus(X, Y)) =#> D#(X)   

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

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

  D#(!facplus(X, Y)) >? D#(X) 
  D#(!factimes(X, Y)) >? D#(X) 
  D#(!factimes(X, Y)) >? D#(Y) 
  D#(!facminus(X, Y)) >? D#(X) 
  D(t) >= 1 
  D(constant) >= 0 
  D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) 
  D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) 
  D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) 
  D(minus(X)) >= minus(D(X)) 
  D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) 
  D(ln(X)) >= div(D(X), X) 
  D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) 
  map(F, nil) >= nil 
  map(F, cons(X, Y)) >= cons(F X, map(F, Y)) 
  filter(F, nil) >= nil 
  filter(F, cons(X, Y)) >= filter2(F X, F, X, Y) 
  filter2(true, F, X, Y) >= cons(X, filter(F, Y)) 
  filter2(false, F, X, Y) >= filter(F, Y) 

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

The following interpretation satisfies the requirements:

  !facminus = \y0y1.1 + y0 
  !facplus = \y0y1.y0 
  !factimes = \y0y1.y0 + y1 
  0 = 0 
  1 = 0 
  2 = 0 
  D = \y0.2y0 
  D# = \y0.2y0 
  cons = \y0y1.0 
  constant = 3 
  div = \y0y1.2 
  false = 3 
  filter = \G0y1.2G0(0) 
  filter2 = \y0G1y2y3.2G1(0) 
  ln = \y0.3 
  map = \G0y1.0 
  minus = \y0.0 
  nil = 0 
  pow = \y0y1.1 + y1 + 2y0 
  t = 3 
  true = 3 

Using this interpretation, the requirements translate to:

  [[D#(!facplus(_x0, _x1))]] = 2x0 >= 2x0 = [[D#(_x0)]] 
  [[D#(!factimes(_x0, _x1))]] = 2x0 + 2x1 >= 2x0 = [[D#(_x0)]] 
  [[D#(!factimes(_x0, _x1))]] = 2x0 + 2x1 >= 2x1 = [[D#(_x1)]] 
  [[D#(!facminus(_x0, _x1))]] = 2 + 2x0 > 2x0 = [[D#(_x0)]] 
  [[D(t)]] = 6 >= 0 = [[1]] 
  [[D(constant)]] = 6 >= 0 = [[0]] 
  [[D(!facplus(_x0, _x1))]] = 2x0 >= 2x0 = [[!facplus(D(_x0), D(_x1))]] 
  [[D(!factimes(_x0, _x1))]] = 2x0 + 2x1 >= x1 + 2x0 = [[!facplus(!factimes(_x1, D(_x0)), !factimes(_x0, D(_x1)))]] 
  [[D(!facminus(_x0, _x1))]] = 2 + 2x0 >= 1 + 2x0 = [[!facminus(D(_x0), D(_x1))]] 
  [[D(minus(_x0))]] = 0 >= 0 = [[minus(D(_x0))]] 
  [[D(div(_x0, _x1))]] = 4 >= 3 = [[!facminus(div(D(_x0), _x1), div(!factimes(_x0, D(_x1)), pow(_x1, 2)))]] 
  [[D(ln(_x0))]] = 6 >= 2 = [[div(D(_x0), _x0)]] 
  [[D(pow(_x0, _x1))]] = 2 + 2x1 + 4x0 >= 2 + 2x1 + 4x0 = [[!facplus(!factimes(!factimes(_x1, pow(_x0, !facminus(_x1, 1))), D(_x0)), !factimes(!factimes(pow(_x0, _x1), ln(_x0)), D(_x1)))]] 
  [[map(_F0, nil)]] = 0 >= 0 = [[nil]] 
  [[map(_F0, cons(_x1, _x2))]] = 0 >= 0 = [[cons(_F0 _x1, map(_F0, _x2))]] 
  [[filter(_F0, nil)]] = 2F0(0) >= 0 = [[nil]] 
  [[filter(_F0, cons(_x1, _x2))]] = 2F0(0) >= 2F0(0) = [[filter2(_F0 _x1, _F0, _x1, _x2)]] 
  [[filter2(true, _F0, _x1, _x2)]] = 2F0(0) >= 0 = [[cons(_x1, filter(_F0, _x2))]] 
  [[filter2(false, _F0, _x1, _x2)]] = 2F0(0) >= 2F0(0) = [[filter(_F0, _x2)]] 

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

  D#(!facplus(X, Y)) =#> D#(X)   
  D#(!factimes(X, Y)) =#> D#(X)   
  D#(!factimes(X, Y)) =#> D#(Y)   

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

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

  D#(!facplus(X, Y)) >? D#(X) 
  D#(!factimes(X, Y)) >? D#(X) 
  D#(!factimes(X, Y)) >? D#(Y) 
  D(t) >= 1 
  D(constant) >= 0 
  D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) 
  D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) 
  D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) 
  D(minus(X)) >= minus(D(X)) 
  D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) 
  D(ln(X)) >= div(D(X), X) 
  D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) 
  map(F, nil) >= nil 
  map(F, cons(X, Y)) >= cons(F X, map(F, Y)) 
  filter(F, nil) >= nil 
  filter(F, cons(X, Y)) >= filter2(F X, F, X, Y) 
  filter2(true, F, X, Y) >= cons(X, filter(F, Y)) 
  filter2(false, F, X, Y) >= filter(F, Y) 

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

The following interpretation satisfies the requirements:

  !facminus = \y0y1.0 
  !facplus = \y0y1.y0 
  !factimes = \y0y1.1 + y0 + y1 
  0 = 0 
  1 = 0 
  2 = 0 
  D = \y0.3y0 
  D# = \y0.y0 
  cons = \y0y1.0 
  constant = 3 
  div = \y0y1.0 
  false = 3 
  filter = \G0y1.0 
  filter2 = \y0G1y2y3.0 
  ln = \y0.3 
  map = \G0y1.2G0(y1) 
  minus = \y0.0 
  nil = 0 
  pow = \y0y1.1 + y1 + 2y0 
  t = 3 
  true = 3 

Using this interpretation, the requirements translate to:

  [[D#(!facplus(_x0, _x1))]] = x0 >= x0 = [[D#(_x0)]] 
  [[D#(!factimes(_x0, _x1))]] = 1 + x0 + x1 > x0 = [[D#(_x0)]] 
  [[D#(!factimes(_x0, _x1))]] = 1 + x0 + x1 > x1 = [[D#(_x1)]] 
  [[D(t)]] = 9 >= 0 = [[1]] 
  [[D(constant)]] = 9 >= 0 = [[0]] 
  [[D(!facplus(_x0, _x1))]] = 3x0 >= 3x0 = [[!facplus(D(_x0), D(_x1))]] 
  [[D(!factimes(_x0, _x1))]] = 3 + 3x0 + 3x1 >= 1 + x1 + 3x0 = [[!facplus(!factimes(_x1, D(_x0)), !factimes(_x0, D(_x1)))]] 
  [[D(!facminus(_x0, _x1))]] = 0 >= 0 = [[!facminus(D(_x0), D(_x1))]] 
  [[D(minus(_x0))]] = 0 >= 0 = [[minus(D(_x0))]] 
  [[D(div(_x0, _x1))]] = 0 >= 0 = [[!facminus(div(D(_x0), _x1), div(!factimes(_x0, D(_x1)), pow(_x1, 2)))]] 
  [[D(ln(_x0))]] = 9 >= 0 = [[div(D(_x0), _x0)]] 
  [[D(pow(_x0, _x1))]] = 3 + 3x1 + 6x0 >= 3 + x1 + 5x0 = [[!facplus(!factimes(!factimes(_x1, pow(_x0, !facminus(_x1, 1))), D(_x0)), !factimes(!factimes(pow(_x0, _x1), ln(_x0)), D(_x1)))]] 
  [[map(_F0, nil)]] = 2F0(0) >= 0 = [[nil]] 
  [[map(_F0, cons(_x1, _x2))]] = 2F0(0) >= 0 = [[cons(_F0 _x1, map(_F0, _x2))]] 
  [[filter(_F0, nil)]] = 0 >= 0 = [[nil]] 
  [[filter(_F0, cons(_x1, _x2))]] = 0 >= 0 = [[filter2(_F0 _x1, _F0, _x1, _x2)]] 
  [[filter2(true, _F0, _x1, _x2)]] = 0 >= 0 = [[cons(_x1, filter(_F0, _x2))]] 
  [[filter2(false, _F0, _x1, _x2)]] = 0 >= 0 = [[filter(_F0, _x2)]] 

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

  D#(!facplus(X, Y)) =#> D#(X)   

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

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

  D#(!facplus(X, Y)) >? D#(X) 
  D(t) >= 1 
  D(constant) >= 0 
  D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) 
  D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) 
  D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) 
  D(minus(X)) >= minus(D(X)) 
  D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) 
  D(ln(X)) >= div(D(X), X) 
  D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) 
  map(F, nil) >= nil 
  map(F, cons(X, Y)) >= cons(F X, map(F, Y)) 
  filter(F, nil) >= nil 
  filter(F, cons(X, Y)) >= filter2(F X, F, X, Y) 
  filter2(true, F, X, Y) >= cons(X, filter(F, Y)) 
  filter2(false, F, X, Y) >= filter(F, Y) 

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

The following interpretation satisfies the requirements:

  !facminus = \y0y1.0 
  !facplus = \y0y1.1 + 2y0 
  !factimes = \y0y1.0 
  0 = 0 
  1 = 0 
  2 = 0 
  D = \y0.1 + 2y0 
  D# = \y0.y0 
  cons = \y0y1.0 
  constant = 3 
  div = \y0y1.0 
  false = 3 
  filter = \G0y1.0 
  filter2 = \y0G1y2y3.0 
  ln = \y0.3 
  map = \G0y1.2 
  minus = \y0.0 
  nil = 0 
  pow = \y0y1.0 
  t = 3 
  true = 3 

Using this interpretation, the requirements translate to:

  [[D#(!facplus(_x0, _x1))]] = 1 + 2x0 > x0 = [[D#(_x0)]] 
  [[D(t)]] = 7 >= 0 = [[1]] 
  [[D(constant)]] = 7 >= 0 = [[0]] 
  [[D(!facplus(_x0, _x1))]] = 3 + 4x0 >= 3 + 4x0 = [[!facplus(D(_x0), D(_x1))]] 
  [[D(!factimes(_x0, _x1))]] = 1 >= 1 = [[!facplus(!factimes(_x1, D(_x0)), !factimes(_x0, D(_x1)))]] 
  [[D(!facminus(_x0, _x1))]] = 1 >= 0 = [[!facminus(D(_x0), D(_x1))]] 
  [[D(minus(_x0))]] = 1 >= 0 = [[minus(D(_x0))]] 
  [[D(div(_x0, _x1))]] = 1 >= 0 = [[!facminus(div(D(_x0), _x1), div(!factimes(_x0, D(_x1)), pow(_x1, 2)))]] 
  [[D(ln(_x0))]] = 7 >= 0 = [[div(D(_x0), _x0)]] 
  [[D(pow(_x0, _x1))]] = 1 >= 1 = [[!facplus(!factimes(!factimes(_x1, pow(_x0, !facminus(_x1, 1))), D(_x0)), !factimes(!factimes(pow(_x0, _x1), ln(_x0)), D(_x1)))]] 
  [[map(_F0, nil)]] = 2 >= 0 = [[nil]] 
  [[map(_F0, cons(_x1, _x2))]] = 2 >= 0 = [[cons(_F0 _x1, map(_F0, _x2))]] 
  [[filter(_F0, nil)]] = 0 >= 0 = [[nil]] 
  [[filter(_F0, cons(_x1, _x2))]] = 0 >= 0 = [[filter2(_F0 _x1, _F0, _x1, _x2)]] 
  [[filter2(true, _F0, _x1, _x2)]] = 0 >= 0 = [[cons(_x1, filter(_F0, _x2))]] 
  [[filter2(false, _F0, _x1, _x2)]] = 0 >= 0 = [[filter(_F0, _x2)]] 

By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_9, 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.