We consider the system Applicative_05__Ex7_9.

  Alphabet:

    0 : [] --> a 
    cons : [b * c] --> c 
    d : [a * a] --> c 
    false : [] --> c 
    filter : [b -> c * c] --> c 
    gtr : [a * a] --> c 
    if : [c * c * c] --> c 
    len : [c] --> a 
    nil : [] --> c 
    s : [a] --> a 
    sub : [a * a] --> a 
    true : [] --> c 

  Rules:

    if(true, x, y) => x 
    if(false, x, y) => y 
    sub(x, 0) => x 
    sub(s(x), s(y)) => sub(x, y) 
    gtr(0, x) => false 
    gtr(s(x), 0) => true 
    gtr(s(x), s(y)) => gtr(x, y) 
    d(x, 0) => true 
    d(s(x), s(y)) => if(gtr(x, y), false, d(s(x), sub(y, x))) 
    len(nil) => 0 
    len(cons(x, y)) => s(len(y)) 
    filter(f, nil) => nil 
    filter(f, cons(x, y)) => if(f x, cons(x, filter(f, 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] sub#(s(X), s(Y)) =#> sub#(X, Y)   
    1] gtr#(s(X), s(Y)) =#> gtr#(X, Y)   
    2] d#(s(X), s(Y)) =#> if#(gtr(X, Y), false, d(s(X), sub(Y, X)))   
    3] d#(s(X), s(Y)) =#> gtr#(X, Y)   
    4] d#(s(X), s(Y)) =#> d#(s(X), sub(Y, X))   
    5] d#(s(X), s(Y)) =#> sub#(Y, X)   
    6] len#(cons(X, Y)) =#> len#(Y)   
    7] filter#(F, cons(X, Y)) =#> if#(F X, cons(X, filter(F, Y)), filter(F, Y))   
    8] filter#(F, cons(X, Y)) =#> filter#(F, Y)   
    9] filter#(F, cons(X, Y)) =#> filter#(F, Y)   

  Rules R_0:

    if(true, X, Y) => X 
    if(false, X, Y) => Y 
    sub(X, 0) => X 
    sub(s(X), s(Y)) => sub(X, Y) 
    gtr(0, X) => false 
    gtr(s(X), 0) => true 
    gtr(s(X), s(Y)) => gtr(X, Y) 
    d(X, 0) => true 
    d(s(X), s(Y)) => if(gtr(X, Y), false, d(s(X), sub(Y, X))) 
    len(nil) => 0 
    len(cons(X, Y)) => s(len(Y)) 
    filter(F, nil) => nil 
    filter(F, cons(X, Y)) => if(F X, cons(X, filter(F, 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:

  sub#(s(X), s(Y)) >? sub#(X, Y) 
  gtr#(s(X), s(Y)) >? gtr#(X, Y) 
  d#(s(X), s(Y)) >? if#(gtr(X, Y), false, d(s(X), sub(Y, X))) 
  d#(s(X), s(Y)) >? gtr#(X, Y) 
  d#(s(X), s(Y)) >? d#(s(X), sub(Y, X)) 
  d#(s(X), s(Y)) >? sub#(Y, X) 
  len#(cons(X, Y)) >? len#(Y) 
  filter#(F, cons(X, Y)) >? if#(F X, cons(X, filter(F, Y)), filter(F, Y)) 
  filter#(F, cons(X, Y)) >? filter#(F, Y) 
  filter#(F, cons(X, Y)) >? filter#(F, Y) 
  if(true, X, Y) >= X 
  if(false, X, Y) >= Y 
  sub(X, 0) >= X 
  sub(s(X), s(Y)) >= sub(X, Y) 
  gtr(0, X) >= false 
  gtr(s(X), 0) >= true 
  gtr(s(X), s(Y)) >= gtr(X, Y) 
  d(X, 0) >= true 
  d(s(X), s(Y)) >= if(gtr(X, Y), false, d(s(X), sub(Y, X))) 
  len(nil) >= 0 
  len(cons(X, Y)) >= s(len(Y)) 
  filter(F, nil) >= nil 
  filter(F, cons(X, Y)) >= if(F X, cons(X, filter(F, Y)), filter(F, Y)) 

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

The following interpretation satisfies the requirements:

  0 = 0 
  cons = \y0y1.2y1 
  d = \y0y1.0 
  d# = \y0y1.3 
  false = 0 
  filter = \G0y1.0 
  filter# = \G0y1.3 
  gtr = \y0y1.0 
  gtr# = \y0y1.0 
  if = \y0y1y2.y1 + y2 
  if# = \y0y1y2.0 
  len = \y0.2y0 
  len# = \y0.0 
  nil = 0 
  s = \y0.y0 
  sub = \y0y1.y0 
  sub# = \y0y1.0 
  true = 0 

Using this interpretation, the requirements translate to:

  [[sub#(s(_x0), s(_x1))]] = 0 >= 0 = [[sub#(_x0, _x1)]] 
  [[gtr#(s(_x0), s(_x1))]] = 0 >= 0 = [[gtr#(_x0, _x1)]] 
  [[d#(s(_x0), s(_x1))]] = 3 > 0 = [[if#(gtr(_x0, _x1), false, d(s(_x0), sub(_x1, _x0)))]] 
  [[d#(s(_x0), s(_x1))]] = 3 > 0 = [[gtr#(_x0, _x1)]] 
  [[d#(s(_x0), s(_x1))]] = 3 >= 3 = [[d#(s(_x0), sub(_x1, _x0))]] 
  [[d#(s(_x0), s(_x1))]] = 3 > 0 = [[sub#(_x1, _x0)]] 
  [[len#(cons(_x0, _x1))]] = 0 >= 0 = [[len#(_x1)]] 
  [[filter#(_F0, cons(_x1, _x2))]] = 3 > 0 = [[if#(_F0 _x1, cons(_x1, filter(_F0, _x2)), filter(_F0, _x2))]] 
  [[filter#(_F0, cons(_x1, _x2))]] = 3 >= 3 = [[filter#(_F0, _x2)]] 
  [[filter#(_F0, cons(_x1, _x2))]] = 3 >= 3 = [[filter#(_F0, _x2)]] 
  [[if(true, _x0, _x1)]] = x0 + x1 >= x0 = [[_x0]] 
  [[if(false, _x0, _x1)]] = x0 + x1 >= x1 = [[_x1]] 
  [[sub(_x0, 0)]] = x0 >= x0 = [[_x0]] 
  [[sub(s(_x0), s(_x1))]] = x0 >= x0 = [[sub(_x0, _x1)]] 
  [[gtr(0, _x0)]] = 0 >= 0 = [[false]] 
  [[gtr(s(_x0), 0)]] = 0 >= 0 = [[true]] 
  [[gtr(s(_x0), s(_x1))]] = 0 >= 0 = [[gtr(_x0, _x1)]] 
  [[d(_x0, 0)]] = 0 >= 0 = [[true]] 
  [[d(s(_x0), s(_x1))]] = 0 >= 0 = [[if(gtr(_x0, _x1), false, d(s(_x0), sub(_x1, _x0)))]] 
  [[len(nil)]] = 0 >= 0 = [[0]] 
  [[len(cons(_x0, _x1))]] = 4x1 >= 2x1 = [[s(len(_x1))]] 
  [[filter(_F0, nil)]] = 0 >= 0 = [[nil]] 
  [[filter(_F0, cons(_x1, _x2))]] = 0 >= 0 = [[if(_F0 _x1, cons(_x1, filter(_F0, _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:

  sub#(s(X), s(Y)) =#> sub#(X, Y)   
  gtr#(s(X), s(Y)) =#> gtr#(X, Y)   
  d#(s(X), s(Y)) =#> d#(s(X), sub(Y, X))   
  len#(cons(X, Y)) =#> len#(Y)   
  filter#(F, cons(X, Y)) =#> filter#(F, Y)   
  filter#(F, cons(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:

  sub#(s(X), s(Y)) >? sub#(X, Y) 
  gtr#(s(X), s(Y)) >? gtr#(X, Y) 
  d#(s(X), s(Y)) >? d#(s(X), sub(Y, X)) 
  len#(cons(X, Y)) >? len#(Y) 
  filter#(F, cons(X, Y)) >? filter#(F, Y) 
  filter#(F, cons(X, Y)) >? filter#(F, Y) 
  if(true, X, Y) >= X 
  if(false, X, Y) >= Y 
  sub(X, 0) >= X 
  sub(s(X), s(Y)) >= sub(X, Y) 
  gtr(0, X) >= false 
  gtr(s(X), 0) >= true 
  gtr(s(X), s(Y)) >= gtr(X, Y) 
  d(X, 0) >= true 
  d(s(X), s(Y)) >= if(gtr(X, Y), false, d(s(X), sub(Y, X))) 
  len(nil) >= 0 
  len(cons(X, Y)) >= s(len(Y)) 
  filter(F, nil) >= nil 
  filter(F, cons(X, Y)) >= if(F X, cons(X, filter(F, 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]] = _|_ 
  [[d#(x_1, x_2)]] = x_2 
  [[false]] = _|_ 
  [[filter#(x_1, x_2)]] = _|_ 
  [[gtr(x_1, x_2)]] = _|_ 
  [[gtr#(x_1, x_2)]] = gtr# 
  [[len#(x_1)]] = _|_ 
  [[nil]] = _|_ 
  [[sub(x_1, x_2)]] = sub(x_1) 
  [[sub#(x_1, x_2)]] = _|_ 
  [[true]] = _|_ 

We choose Lex = {} and Mul = {@_{o -> o}, cons, d, filter, gtr#, if, len, s, sub}, and the following precedence: d > filter > cons > gtr# > if > len = s > @_{o -> o} > sub

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

  _|_ >= _|_ 
  gtr# >= gtr# 
  s(X) > sub(X) 
  _|_ >= _|_ 
  _|_ >= _|_ 
  _|_ >= _|_ 
  if(_|_, X, Y) >= X 
  if(_|_, X, Y) >= Y 
  sub(X) >= X 
  sub(s(X)) >= sub(X) 
  _|_ >= _|_ 
  _|_ >= _|_ 
  _|_ >= _|_ 
  d(X, _|_) >= _|_ 
  d(s(X), s(Y)) >= if(_|_, _|_, d(s(X), sub(Y))) 
  len(_|_) >= _|_ 
  len(cons(X, Y)) >= s(len(Y)) 
  filter(F, _|_) >= _|_ 
  filter(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, filter(F, Y)), filter(F, Y)) 

With these choices, we have:

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

  2] gtr# >= gtr#  because gtr# in Mul, by (Fun) 

  3] s(X) > sub(X)  because [4], by definition 
  4] s*(X) >= sub(X)  because s > sub and [5], by (Copy) 
  5] s*(X) >= X  because [6], by (Select) 
  6] X >= X  by (Meta) 

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

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

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

  10] if(_|_, X, Y) >= X  because [11], by (Star) 
  11] if*(_|_, X, Y) >= X  because [12], by (Select) 
  12] X >= X  by (Meta) 

  13] if(_|_, X, Y) >= Y  because [14], by (Star) 
  14] if*(_|_, X, Y) >= Y  because [15], by (Select) 
  15] Y >= Y  by (Meta) 

  16] sub(X) >= X  because [17], by (Star) 
  17] sub*(X) >= X  because [18], by (Select) 
  18] X >= X  by (Meta) 

  19] sub(s(X)) >= sub(X)  because [20], by (Star) 
  20] sub*(s(X)) >= sub(X)  because [21], by (Select) 
  21] s(X) >= sub(X)  because [22], by (Star) 
  22] s*(X) >= sub(X)  because s > sub and [23], by (Copy) 
  23] s*(X) >= X  because [24], by (Select) 
  24] X >= X  by (Meta) 

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

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

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

  28] d(X, _|_) >= _|_  by (Bot) 

  29] d(s(X), s(Y)) >= if(_|_, _|_, d(s(X), sub(Y)))  because [30], by (Star) 
  30] d*(s(X), s(Y)) >= if(_|_, _|_, d(s(X), sub(Y)))  because d > if, [31], [32] and [33], by (Copy) 
  31] d*(s(X), s(Y)) >= _|_  by (Bot) 
  32] d*(s(X), s(Y)) >= _|_  by (Bot) 
  33] d*(s(X), s(Y)) >= d(s(X), sub(Y))  because d in Mul, [34] and [36], by (Stat) 
  34] s(X) >= s(X)  because s in Mul and [35], by (Fun) 
  35] X >= X  by (Meta) 
  36] s(Y) > sub(Y)  because [4], by definition 

  37] len(_|_) >= _|_  by (Bot) 

  38] len(cons(X, Y)) >= s(len(Y))  because len = s, len in Mul and [39], by (Fun) 
  39] cons(X, Y) >= len(Y)  because [40], by (Star) 
  40] cons*(X, Y) >= len(Y)  because cons > len and [41], by (Copy) 
  41] cons*(X, Y) >= Y  because [42], by (Select) 
  42] Y >= Y  by (Meta) 

  43] filter(F, _|_) >= _|_  by (Bot) 

  44] filter(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, filter(F, Y)), filter(F, Y))  because [45], by (Star) 
  45] filter*(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, filter(F, Y)), filter(F, Y))  because filter > if, [46], [53] and [54], by (Copy) 
  46] filter*(F, cons(X, Y)) >= @_{o -> o}(F, X)  because filter > @_{o -> o}, [47] and [49], by (Copy) 
  47] filter*(F, cons(X, Y)) >= F  because [48], by (Select) 
  48] F >= F  by (Meta) 
  49] filter*(F, cons(X, Y)) >= X  because [50], by (Select) 
  50] cons(X, Y) >= X  because [51], by (Star) 
  51] cons*(X, Y) >= X  because [52], by (Select) 
  52] X >= X  by (Meta) 
  53] filter*(F, cons(X, Y)) >= cons(X, filter(F, Y))  because filter > cons, [49] and [54], by (Copy) 
  54] filter*(F, cons(X, Y)) >= filter(F, Y)  because filter in Mul, [55] and [56], by (Stat) 
  55] F >= F  by (Meta) 
  56] cons(X, Y) > Y  because [57], by definition 
  57] cons*(X, Y) >= Y  because [58], by (Select) 
  58] 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_1, R_0, static, formative) by (P_2, R_0, static, formative), where P_2 consists of:

  sub#(s(X), s(Y)) =#> sub#(X, Y)   
  gtr#(s(X), s(Y)) =#> gtr#(X, Y)   
  len#(cons(X, Y)) =#> len#(Y)   
  filter#(F, cons(X, Y)) =#> filter#(F, Y)   
  filter#(F, cons(X, Y)) =#> filter#(F, 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:

  sub#(s(X), s(Y)) >? sub#(X, Y) 
  gtr#(s(X), s(Y)) >? gtr#(X, Y) 
  len#(cons(X, Y)) >? len#(Y) 
  filter#(F, cons(X, Y)) >? filter#(F, Y) 
  filter#(F, cons(X, Y)) >? filter#(F, Y) 
  if(true, X, Y) >= X 
  if(false, X, Y) >= Y 
  sub(X, 0) >= X 
  sub(s(X), s(Y)) >= sub(X, Y) 
  gtr(0, X) >= false 
  gtr(s(X), 0) >= true 
  gtr(s(X), s(Y)) >= gtr(X, Y) 
  d(X, 0) >= true 
  d(s(X), s(Y)) >= if(gtr(X, Y), false, d(s(X), sub(Y, X))) 
  len(nil) >= 0 
  len(cons(X, Y)) >= s(len(Y)) 
  filter(F, nil) >= nil 
  filter(F, cons(X, Y)) >= if(F X, cons(X, filter(F, 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]] = _|_ 
  [[false]] = _|_ 
  [[filter#(x_1, x_2)]] = filter# 
  [[gtr(x_1, x_2)]] = _|_ 
  [[nil]] = _|_ 
  [[sub(x_1, x_2)]] = x_1 
  [[true]] = _|_ 

We choose Lex = {} and Mul = {@_{o -> o}, cons, d, filter, filter#, gtr#, if, len, len#, s, sub#}, and the following precedence: sub# > gtr# > filter# > filter > @_{o -> o} > cons > d > if > len = s > len#

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

  sub#(s(X), s(Y)) >= sub#(X, Y) 
  gtr#(s(X), s(Y)) >= gtr#(X, Y) 
  len#(cons(X, Y)) > len#(Y) 
  filter# >= filter# 
  filter# >= filter# 
  if(_|_, X, Y) >= X 
  if(_|_, X, Y) >= Y 
  X >= X 
  s(X) >= X 
  _|_ >= _|_ 
  _|_ >= _|_ 
  _|_ >= _|_ 
  d(X, _|_) >= _|_ 
  d(s(X), s(Y)) >= if(_|_, _|_, d(s(X), Y)) 
  len(_|_) >= _|_ 
  len(cons(X, Y)) >= s(len(Y)) 
  filter(F, _|_) >= _|_ 
  filter(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, filter(F, Y)), filter(F, Y)) 

With these choices, we have:

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

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

  16] len#(cons(X, Y)) > len#(Y)  because [17], by definition 
  17] len#*(cons(X, Y)) >= len#(Y)  because [18], by (Select) 
  18] cons(X, Y) >= len#(Y)  because [19], by (Star) 
  19] cons*(X, Y) >= len#(Y)  because cons > len# and [20], by (Copy) 
  20] cons*(X, Y) >= Y  because [21], by (Select) 
  21] Y >= Y  by (Meta) 

  22] filter# >= filter#  because filter# in Mul, by (Fun) 

  23] filter# >= filter#  because filter# in Mul, by (Fun) 

  24] if(_|_, X, Y) >= X  because [25], by (Star) 
  25] if*(_|_, X, Y) >= X  because [26], by (Select) 
  26] X >= X  by (Meta) 

  27] if(_|_, X, Y) >= Y  because [28], by (Star) 
  28] if*(_|_, X, Y) >= Y  because [29], by (Select) 
  29] Y >= Y  by (Meta) 

  30] X >= X  by (Meta) 

  31] s(X) >= X  because [3], by (Star) 

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

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

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

  35] d(X, _|_) >= _|_  by (Bot) 

  36] d(s(X), s(Y)) >= if(_|_, _|_, d(s(X), Y))  because [37], by (Star) 
  37] d*(s(X), s(Y)) >= if(_|_, _|_, d(s(X), Y))  because d > if, [38], [39] and [40], by (Copy) 
  38] d*(s(X), s(Y)) >= _|_  by (Bot) 
  39] d*(s(X), s(Y)) >= _|_  by (Bot) 
  40] d*(s(X), s(Y)) >= d(s(X), Y)  because d in Mul, [41] and [43], by (Stat) 
  41] s(X) >= s(X)  because s in Mul and [42], by (Fun) 
  42] X >= X  by (Meta) 
  43] s(Y) > Y  because [44], by definition 
  44] s*(Y) >= Y  because [45], by (Select) 
  45] Y >= Y  by (Meta) 

  46] len(_|_) >= _|_  by (Bot) 

  47] len(cons(X, Y)) >= s(len(Y))  because len = s, len in Mul and [48], by (Fun) 
  48] cons(X, Y) >= len(Y)  because [49], by (Star) 
  49] cons*(X, Y) >= len(Y)  because cons > len and [20], by (Copy) 

  50] filter(F, _|_) >= _|_  by (Bot) 

  51] filter(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, filter(F, Y)), filter(F, Y))  because [52], by (Star) 
  52] filter*(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, filter(F, Y)), filter(F, Y))  because filter > if, [53], [60] and [61], by (Copy) 
  53] filter*(F, cons(X, Y)) >= @_{o -> o}(F, X)  because filter > @_{o -> o}, [54] and [56], by (Copy) 
  54] filter*(F, cons(X, Y)) >= F  because [55], by (Select) 
  55] F >= F  by (Meta) 
  56] filter*(F, cons(X, Y)) >= X  because [57], by (Select) 
  57] cons(X, Y) >= X  because [58], by (Star) 
  58] cons*(X, Y) >= X  because [59], by (Select) 
  59] X >= X  by (Meta) 
  60] filter*(F, cons(X, Y)) >= cons(X, filter(F, Y))  because filter > cons, [56] and [61], by (Copy) 
  61] filter*(F, cons(X, Y)) >= filter(F, Y)  because filter in Mul, [62] and [63], by (Stat) 
  62] F >= F  by (Meta) 
  63] cons(X, Y) > Y  because [64], by definition 
  64] cons*(X, Y) >= Y  because [65], by (Select) 
  65] 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:

  sub#(s(X), s(Y)) =#> sub#(X, Y)   
  gtr#(s(X), s(Y)) =#> gtr#(X, Y)   
  filter#(F, cons(X, Y)) =#> filter#(F, Y)   
  filter#(F, cons(X, Y)) =#> filter#(F, 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:

  sub#(s(X), s(Y)) >? sub#(X, Y) 
  gtr#(s(X), s(Y)) >? gtr#(X, Y) 
  filter#(F, cons(X, Y)) >? filter#(F, Y) 
  filter#(F, cons(X, Y)) >? filter#(F, Y) 
  if(true, X, Y) >= X 
  if(false, X, Y) >= Y 
  sub(X, 0) >= X 
  sub(s(X), s(Y)) >= sub(X, Y) 
  gtr(0, X) >= false 
  gtr(s(X), 0) >= true 
  gtr(s(X), s(Y)) >= gtr(X, Y) 
  d(X, 0) >= true 
  d(s(X), s(Y)) >= if(gtr(X, Y), false, d(s(X), sub(Y, X))) 
  len(nil) >= 0 
  len(cons(X, Y)) >= s(len(Y)) 
  filter(F, nil) >= nil 
  filter(F, cons(X, Y)) >= if(F X, cons(X, filter(F, 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]] = _|_ 
  [[false]] = _|_ 
  [[filter#(x_1, x_2)]] = filter#(x_2) 
  [[gtr(x_1, x_2)]] = _|_ 
  [[if(x_1, x_2, x_3)]] = if(x_2, x_3) 
  [[nil]] = _|_ 
  [[sub(x_1, x_2)]] = x_1 
  [[true]] = _|_ 

We choose Lex = {} and Mul = {@_{o -> o}, cons, d, filter, filter#, gtr#, if, len, s, sub#}, and the following precedence: gtr# > filter > cons > filter# > @_{o -> o} > d > if > s > sub# > len

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

  sub#(s(X), s(Y)) > sub#(X, Y) 
  gtr#(s(X), s(Y)) >= gtr#(X, Y) 
  filter#(cons(X, Y)) >= filter#(Y) 
  filter#(cons(X, Y)) >= filter#(Y) 
  if(X, Y) >= X 
  if(X, Y) >= Y 
  X >= X 
  s(X) >= X 
  _|_ >= _|_ 
  _|_ >= _|_ 
  _|_ >= _|_ 
  d(X, _|_) >= _|_ 
  d(s(X), s(Y)) >= if(_|_, d(s(X), Y)) 
  len(_|_) >= _|_ 
  len(cons(X, Y)) >= s(len(Y)) 
  filter(F, _|_) >= _|_ 
  filter(F, cons(X, Y)) >= if(cons(X, filter(F, Y)), filter(F, Y)) 

With these choices, we have:

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

  9] gtr#(s(X), s(Y)) >= gtr#(X, Y)  because gtr# in Mul, [10] and [13], by (Fun) 
  10] s(X) >= X  because [11], by (Star) 
  11] s*(X) >= X  because [12], by (Select) 
  12] X >= X  by (Meta) 
  13] s(Y) >= Y  because [14], by (Star) 
  14] s*(Y) >= Y  because [15], by (Select) 
  15] Y >= Y  by (Meta) 

  16] filter#(cons(X, Y)) >= filter#(Y)  because [17], by (Star) 
  17] filter#*(cons(X, Y)) >= filter#(Y)  because [18], by (Select) 
  18] cons(X, Y) >= filter#(Y)  because [19], by (Star) 
  19] cons*(X, Y) >= filter#(Y)  because cons > filter# and [20], by (Copy) 
  20] cons*(X, Y) >= Y  because [21], by (Select) 
  21] Y >= Y  by (Meta) 

  22] filter#(cons(X, Y)) >= filter#(Y)  because [17], by (Star) 

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

  26] if(X, Y) >= Y  because [27], by (Star) 
  27] if*(X, Y) >= Y  because [28], by (Select) 
  28] Y >= Y  by (Meta) 

  29] X >= X  by (Meta) 

  30] s(X) >= X  because [4], by (Star) 

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

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

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

  34] d(X, _|_) >= _|_  by (Bot) 

  35] d(s(X), s(Y)) >= if(_|_, d(s(X), Y))  because [36], by (Star) 
  36] d*(s(X), s(Y)) >= if(_|_, d(s(X), Y))  because d > if, [37] and [38], by (Copy) 
  37] d*(s(X), s(Y)) >= _|_  by (Bot) 
  38] d*(s(X), s(Y)) >= d(s(X), Y)  because d in Mul, [39] and [41], by (Stat) 
  39] s(X) >= s(X)  because s in Mul and [40], by (Fun) 
  40] X >= X  by (Meta) 
  41] s(Y) > Y  because [42], by definition 
  42] s*(Y) >= Y  because [43], by (Select) 
  43] Y >= Y  by (Meta) 

  44] len(_|_) >= _|_  by (Bot) 

  45] len(cons(X, Y)) >= s(len(Y))  because [46], by (Star) 
  46] len*(cons(X, Y)) >= s(len(Y))  because [47], by (Select) 
  47] cons(X, Y) >= s(len(Y))  because [48], by (Star) 
  48] cons*(X, Y) >= s(len(Y))  because cons > s and [49], by (Copy) 
  49] cons*(X, Y) >= len(Y)  because cons > len and [50], by (Copy) 
  50] cons*(X, Y) >= Y  because [51], by (Select) 
  51] Y >= Y  by (Meta) 

  52] filter(F, _|_) >= _|_  by (Bot) 

  53] filter(F, cons(X, Y)) >= if(cons(X, filter(F, Y)), filter(F, Y))  because [54], by (Star) 
  54] filter*(F, cons(X, Y)) >= if(cons(X, filter(F, Y)), filter(F, Y))  because filter > if, [55] and [60], by (Copy) 
  55] filter*(F, cons(X, Y)) >= cons(X, filter(F, Y))  because filter > cons, [56] and [60], by (Copy) 
  56] filter*(F, cons(X, Y)) >= X  because [57], by (Select) 
  57] cons(X, Y) >= X  because [58], by (Star) 
  58] cons*(X, Y) >= X  because [59], by (Select) 
  59] X >= X  by (Meta) 
  60] filter*(F, cons(X, Y)) >= filter(F, Y)  because filter in Mul, [61] and [62], by (Stat) 
  61] F >= F  by (Meta) 
  62] cons(X, Y) > Y  because [20], by definition 

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:

  gtr#(s(X), s(Y)) =#> gtr#(X, Y)   
  filter#(F, cons(X, Y)) =#> filter#(F, Y)   
  filter#(F, cons(X, Y)) =#> filter#(F, 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:

  gtr#(s(X), s(Y)) >? gtr#(X, Y) 
  filter#(F, cons(X, Y)) >? filter#(F, Y) 
  filter#(F, cons(X, Y)) >? filter#(F, Y) 
  if(true, X, Y) >= X 
  if(false, X, Y) >= Y 
  sub(X, 0) >= X 
  sub(s(X), s(Y)) >= sub(X, Y) 
  gtr(0, X) >= false 
  gtr(s(X), 0) >= true 
  gtr(s(X), s(Y)) >= gtr(X, Y) 
  d(X, 0) >= true 
  d(s(X), s(Y)) >= if(gtr(X, Y), false, d(s(X), sub(Y, X))) 
  len(nil) >= 0 
  len(cons(X, Y)) >= s(len(Y)) 
  filter(F, nil) >= nil 
  filter(F, cons(X, Y)) >= if(F X, cons(X, filter(F, 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]] = _|_ 
  [[false]] = _|_ 
  [[gtr(x_1, x_2)]] = _|_ 
  [[sub(x_1, x_2)]] = sub(x_1) 
  [[true]] = _|_ 

We choose Lex = {} and Mul = {@_{o -> o}, cons, d, filter, filter#, gtr#, if, len, nil, s, sub}, and the following precedence: filter# > gtr# > filter > @_{o -> o} > d > if > nil > len > s > sub > cons

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

  gtr#(s(X), s(Y)) >= gtr#(X, Y) 
  filter#(F, cons(X, Y)) >= filter#(F, Y) 
  filter#(F, cons(X, Y)) > filter#(F, Y) 
  if(_|_, X, Y) >= X 
  if(_|_, X, Y) >= Y 
  sub(X) >= X 
  sub(s(X)) >= sub(X) 
  _|_ >= _|_ 
  _|_ >= _|_ 
  _|_ >= _|_ 
  d(X, _|_) >= _|_ 
  d(s(X), s(Y)) >= if(_|_, _|_, d(s(X), sub(Y))) 
  len(nil) >= _|_ 
  len(cons(X, Y)) >= s(len(Y)) 
  filter(F, nil) >= nil 
  filter(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, filter(F, Y)), filter(F, Y)) 

With these choices, we have:

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

  8] filter#(F, cons(X, Y)) >= filter#(F, Y)  because [9], by (Star) 
  9] filter#*(F, cons(X, Y)) >= filter#(F, Y)  because filter# in Mul, [10] and [11], by (Stat) 
  10] F >= F  by (Meta) 
  11] cons(X, Y) > Y  because [12], by definition 
  12] cons*(X, Y) >= Y  because [13], by (Select) 
  13] Y >= Y  by (Meta) 

  14] filter#(F, cons(X, Y)) > filter#(F, Y)  because [15], by definition 
  15] filter#*(F, cons(X, Y)) >= filter#(F, Y)  because filter# in Mul, [10] and [11], by (Stat) 

  16] if(_|_, X, Y) >= X  because [17], by (Star) 
  17] if*(_|_, X, Y) >= X  because [18], by (Select) 
  18] X >= X  by (Meta) 

  19] if(_|_, X, Y) >= Y  because [20], by (Star) 
  20] if*(_|_, X, Y) >= Y  because [21], by (Select) 
  21] Y >= Y  by (Meta) 

  22] sub(X) >= X  because [23], by (Star) 
  23] sub*(X) >= X  because [24], by (Select) 
  24] X >= X  by (Meta) 

  25] sub(s(X)) >= sub(X)  because [26], by (Star) 
  26] sub*(s(X)) >= sub(X)  because [27], by (Select) 
  27] s(X) >= sub(X)  because [28], by (Star) 
  28] s*(X) >= sub(X)  because s > sub and [29], by (Copy) 
  29] s*(X) >= X  because [30], by (Select) 
  30] X >= X  by (Meta) 

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

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

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

  34] d(X, _|_) >= _|_  by (Bot) 

  35] d(s(X), s(Y)) >= if(_|_, _|_, d(s(X), sub(Y)))  because [36], by (Star) 
  36] d*(s(X), s(Y)) >= if(_|_, _|_, d(s(X), sub(Y)))  because d > if, [37], [38] and [39], by (Copy) 
  37] d*(s(X), s(Y)) >= _|_  by (Bot) 
  38] d*(s(X), s(Y)) >= _|_  by (Bot) 
  39] d*(s(X), s(Y)) >= d(s(X), sub(Y))  because d in Mul, [40] and [42], by (Stat) 
  40] s(X) >= s(X)  because s in Mul and [41], by (Fun) 
  41] X >= X  by (Meta) 
  42] s(Y) > sub(Y)  because [43], by definition 
  43] s*(Y) >= sub(Y)  because s > sub and [44], by (Copy) 
  44] s*(Y) >= Y  because [45], by (Select) 
  45] Y >= Y  by (Meta) 

  46] len(nil) >= _|_  by (Bot) 

  47] len(cons(X, Y)) >= s(len(Y))  because [48], by (Star) 
  48] len*(cons(X, Y)) >= s(len(Y))  because len > s and [49], by (Copy) 
  49] len*(cons(X, Y)) >= len(Y)  because len in Mul and [50], by (Stat) 
  50] cons(X, Y) > Y  because [51], by definition 
  51] cons*(X, Y) >= Y  because [52], by (Select) 
  52] Y >= Y  by (Meta) 

  53] filter(F, nil) >= nil  because [54], by (Star) 
  54] filter*(F, nil) >= nil  because filter > nil, by (Copy) 

  55] filter(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, filter(F, Y)), filter(F, Y))  because [56], by (Star) 
  56] filter*(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, filter(F, Y)), filter(F, Y))  because filter > if, [57], [63] and [64], by (Copy) 
  57] filter*(F, cons(X, Y)) >= @_{o -> o}(F, X)  because filter > @_{o -> o}, [58] and [59], by (Copy) 
  58] filter*(F, cons(X, Y)) >= F  because [10], by (Select) 
  59] filter*(F, cons(X, Y)) >= X  because [60], by (Select) 
  60] cons(X, Y) >= X  because [61], by (Star) 
  61] cons*(X, Y) >= X  because [62], by (Select) 
  62] X >= X  by (Meta) 
  63] filter*(F, cons(X, Y)) >= cons(X, filter(F, Y))  because filter > cons, [59] and [64], by (Copy) 
  64] filter*(F, cons(X, Y)) >= filter(F, Y)  because filter in Mul, [10] and [11], by (Stat) 

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:

  gtr#(s(X), s(Y)) =#> gtr#(X, Y)   
  filter#(F, cons(X, Y)) =#> filter#(F, 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:

  gtr#(s(X), s(Y)) >? gtr#(X, Y) 
  filter#(F, cons(X, Y)) >? filter#(F, Y) 
  if(true, X, Y) >= X 
  if(false, X, Y) >= Y 
  sub(X, 0) >= X 
  sub(s(X), s(Y)) >= sub(X, Y) 
  gtr(0, X) >= false 
  gtr(s(X), 0) >= true 
  gtr(s(X), s(Y)) >= gtr(X, Y) 
  d(X, 0) >= true 
  d(s(X), s(Y)) >= if(gtr(X, Y), false, d(s(X), sub(Y, X))) 
  len(nil) >= 0 
  len(cons(X, Y)) >= s(len(Y)) 
  filter(F, nil) >= nil 
  filter(F, cons(X, Y)) >= if(F X, cons(X, filter(F, 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]] = _|_ 
  [[false]] = _|_ 
  [[nil]] = _|_ 
  [[sub(x_1, x_2)]] = sub(x_1) 
  [[true]] = _|_ 

We choose Lex = {} and Mul = {@_{o -> o}, cons, d, filter, filter#, gtr, gtr#, if, len, s, sub}, and the following precedence: filter# > gtr# > filter > @_{o -> o} > cons > len > s > d > gtr > if > sub

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

  gtr#(s(X), s(Y)) > gtr#(X, Y) 
  filter#(F, cons(X, Y)) >= filter#(F, Y) 
  if(_|_, X, Y) >= X 
  if(_|_, X, Y) >= Y 
  sub(X) >= X 
  sub(s(X)) >= sub(X) 
  gtr(_|_, X) >= _|_ 
  gtr(s(X), _|_) >= _|_ 
  gtr(s(X), s(Y)) >= gtr(X, Y) 
  d(X, _|_) >= _|_ 
  d(s(X), s(Y)) >= if(gtr(X, Y), _|_, d(s(X), sub(Y))) 
  len(_|_) >= _|_ 
  len(cons(X, Y)) >= s(len(Y)) 
  filter(F, _|_) >= _|_ 
  filter(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, filter(F, Y)), filter(F, Y)) 

With these choices, we have:

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

  9] filter#(F, cons(X, Y)) >= filter#(F, Y)  because [10], by (Star) 
  10] filter#*(F, cons(X, Y)) >= filter#(F, Y)  because filter# in Mul, [11] and [12], by (Stat) 
  11] F >= F  by (Meta) 
  12] cons(X, Y) > Y  because [13], by definition 
  13] cons*(X, Y) >= Y  because [14], by (Select) 
  14] Y >= Y  by (Meta) 

  15] if(_|_, X, Y) >= X  because [16], by (Star) 
  16] if*(_|_, X, Y) >= X  because [17], by (Select) 
  17] X >= X  by (Meta) 

  18] if(_|_, X, Y) >= Y  because [19], by (Star) 
  19] if*(_|_, X, Y) >= Y  because [20], by (Select) 
  20] Y >= Y  by (Meta) 

  21] sub(X) >= X  because [22], by (Star) 
  22] sub*(X) >= X  because [23], by (Select) 
  23] X >= X  by (Meta) 

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

  29] gtr(_|_, X) >= _|_  by (Bot) 

  30] gtr(s(X), _|_) >= _|_  by (Bot) 

  31] gtr(s(X), s(Y)) >= gtr(X, Y)  because [32], by (Star) 
  32] gtr*(s(X), s(Y)) >= gtr(X, Y)  because gtr in Mul, [3] and [6], by (Stat) 

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

  34] d(s(X), s(Y)) >= if(gtr(X, Y), _|_, d(s(X), sub(Y)))  because [35], by (Star) 
  35] d*(s(X), s(Y)) >= if(gtr(X, Y), _|_, d(s(X), sub(Y)))  because d > if, [36], [45] and [46], by (Copy) 
  36] d*(s(X), s(Y)) >= gtr(X, Y)  because d > gtr, [37] and [41], by (Copy) 
  37] d*(s(X), s(Y)) >= X  because [38], by (Select) 
  38] s(X) >= X  because [39], by (Star) 
  39] s*(X) >= X  because [40], by (Select) 
  40] X >= X  by (Meta) 
  41] d*(s(X), s(Y)) >= Y  because [42], by (Select) 
  42] s(Y) >= Y  because [43], by (Star) 
  43] s*(Y) >= Y  because [44], by (Select) 
  44] Y >= Y  by (Meta) 
  45] d*(s(X), s(Y)) >= _|_  by (Bot) 
  46] d*(s(X), s(Y)) >= d(s(X), sub(Y))  because d in Mul, [47] and [49], by (Stat) 
  47] s(X) >= s(X)  because s in Mul and [48], by (Fun) 
  48] X >= X  by (Meta) 
  49] s(Y) > sub(Y)  because [50], by definition 
  50] s*(Y) >= sub(Y)  because s > sub and [51], by (Copy) 
  51] s*(Y) >= Y  because [44], by (Select) 

  52] len(_|_) >= _|_  by (Bot) 

  53] len(cons(X, Y)) >= s(len(Y))  because [54], by (Star) 
  54] len*(cons(X, Y)) >= s(len(Y))  because len > s and [55], by (Copy) 
  55] len*(cons(X, Y)) >= len(Y)  because len in Mul and [56], by (Stat) 
  56] cons(X, Y) > Y  because [57], by definition 
  57] cons*(X, Y) >= Y  because [58], by (Select) 
  58] Y >= Y  by (Meta) 

  59] filter(F, _|_) >= _|_  by (Bot) 

  60] filter(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, filter(F, Y)), filter(F, Y))  because [61], by (Star) 
  61] filter*(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, filter(F, Y)), filter(F, Y))  because filter > if, [62], [68] and [69], by (Copy) 
  62] filter*(F, cons(X, Y)) >= @_{o -> o}(F, X)  because filter > @_{o -> o}, [63] and [64], by (Copy) 
  63] filter*(F, cons(X, Y)) >= F  because [11], by (Select) 
  64] filter*(F, cons(X, Y)) >= X  because [65], by (Select) 
  65] cons(X, Y) >= X  because [66], by (Star) 
  66] cons*(X, Y) >= X  because [67], by (Select) 
  67] X >= X  by (Meta) 
  68] filter*(F, cons(X, Y)) >= cons(X, filter(F, Y))  because filter > cons, [64] and [69], by (Copy) 
  69] filter*(F, cons(X, Y)) >= filter(F, Y)  because filter in Mul, [11] and [12], by (Stat) 

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:

  filter#(F, cons(X, Y)) =#> filter#(F, 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:

  filter#(F, cons(X, Y)) >? filter#(F, Y) 
  if(true, X, Y) >= X 
  if(false, X, Y) >= Y 
  sub(X, 0) >= X 
  sub(s(X), s(Y)) >= sub(X, Y) 
  gtr(0, X) >= false 
  gtr(s(X), 0) >= true 
  gtr(s(X), s(Y)) >= gtr(X, Y) 
  d(X, 0) >= true 
  d(s(X), s(Y)) >= if(gtr(X, Y), false, d(s(X), sub(Y, X))) 
  len(nil) >= 0 
  len(cons(X, Y)) >= s(len(Y)) 
  filter(F, nil) >= nil 
  filter(F, cons(X, Y)) >= if(F X, cons(X, filter(F, 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]] = _|_ 
  [[false]] = _|_ 
  [[filter#(x_1, x_2)]] = filter#(x_2, x_1) 
  [[gtr(x_1, x_2)]] = gtr(x_1) 
  [[nil]] = _|_ 
  [[sub(x_1, x_2)]] = sub(x_1) 
  [[true]] = _|_ 

We choose Lex = {filter#} and Mul = {@_{o -> o}, cons, d, filter, gtr, if, len, s, sub}, and the following precedence: filter# > filter > @_{o -> o} > cons > len > d > gtr > if > s > sub

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

  filter#(F, cons(X, Y)) > filter#(F, Y) 
  if(_|_, X, Y) >= X 
  if(_|_, X, Y) >= Y 
  sub(X) >= X 
  sub(s(X)) >= sub(X) 
  gtr(_|_) >= _|_ 
  gtr(s(X)) >= _|_ 
  gtr(s(X)) >= gtr(X) 
  d(X, _|_) >= _|_ 
  d(s(X), s(Y)) >= if(gtr(X), _|_, d(s(X), sub(Y))) 
  len(_|_) >= _|_ 
  len(cons(X, Y)) >= s(len(Y)) 
  filter(F, _|_) >= _|_ 
  filter(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, filter(F, Y)), filter(F, Y)) 

With these choices, we have:

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

  10] if(_|_, X, Y) >= X  because [11], by (Star) 
  11] if*(_|_, X, Y) >= X  because [12], by (Select) 
  12] X >= X  by (Meta) 

  13] if(_|_, X, Y) >= Y  because [14], by (Star) 
  14] if*(_|_, X, Y) >= Y  because [15], by (Select) 
  15] Y >= Y  by (Meta) 

  16] sub(X) >= X  because [17], by (Star) 
  17] sub*(X) >= X  because [18], by (Select) 
  18] X >= X  by (Meta) 

  19] sub(s(X)) >= sub(X)  because [20], by (Star) 
  20] sub*(s(X)) >= sub(X)  because sub in Mul and [21], by (Stat) 
  21] s(X) > X  because [22], by definition 
  22] s*(X) >= X  because [23], by (Select) 
  23] X >= X  by (Meta) 

  24] gtr(_|_) >= _|_  by (Bot) 

  25] gtr(s(X)) >= _|_  by (Bot) 

  26] gtr(s(X)) >= gtr(X)  because gtr in Mul and [27], by (Fun) 
  27] s(X) >= X  because [28], by (Star) 
  28] s*(X) >= X  because [29], by (Select) 
  29] X >= X  by (Meta) 

  30] d(X, _|_) >= _|_  by (Bot) 

  31] d(s(X), s(Y)) >= if(gtr(X), _|_, d(s(X), sub(Y)))  because [32], by (Star) 
  32] d*(s(X), s(Y)) >= if(gtr(X), _|_, d(s(X), sub(Y)))  because d > if, [33], [38] and [39], by (Copy) 
  33] d*(s(X), s(Y)) >= gtr(X)  because d > gtr and [34], by (Copy) 
  34] d*(s(X), s(Y)) >= X  because [35], by (Select) 
  35] s(X) >= X  because [36], by (Star) 
  36] s*(X) >= X  because [37], by (Select) 
  37] X >= X  by (Meta) 
  38] d*(s(X), s(Y)) >= _|_  by (Bot) 
  39] d*(s(X), s(Y)) >= d(s(X), sub(Y))  because d in Mul, [40] and [42], by (Stat) 
  40] s(X) >= s(X)  because s in Mul and [41], by (Fun) 
  41] X >= X  by (Meta) 
  42] s(Y) > sub(Y)  because [43], by definition 
  43] s*(Y) >= sub(Y)  because s > sub and [44], by (Copy) 
  44] s*(Y) >= Y  because [45], by (Select) 
  45] Y >= Y  by (Meta) 

  46] len(_|_) >= _|_  by (Bot) 

  47] len(cons(X, Y)) >= s(len(Y))  because [48], by (Star) 
  48] len*(cons(X, Y)) >= s(len(Y))  because len > s and [49], by (Copy) 
  49] len*(cons(X, Y)) >= len(Y)  because len in Mul and [50], by (Stat) 
  50] cons(X, Y) > Y  because [51], by definition 
  51] cons*(X, Y) >= Y  because [52], by (Select) 
  52] Y >= Y  by (Meta) 

  53] filter(F, _|_) >= _|_  by (Bot) 

  54] filter(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, filter(F, Y)), filter(F, Y))  because [55], by (Star) 
  55] filter*(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, filter(F, Y)), filter(F, Y))  because filter > if, [56], [62] and [63], by (Copy) 
  56] filter*(F, cons(X, Y)) >= @_{o -> o}(F, X)  because filter > @_{o -> o}, [57] and [58], by (Copy) 
  57] filter*(F, cons(X, Y)) >= F  because [7], by (Select) 
  58] filter*(F, cons(X, Y)) >= X  because [59], by (Select) 
  59] cons(X, Y) >= X  because [60], by (Star) 
  60] cons*(X, Y) >= X  because [61], by (Select) 
  61] X >= X  by (Meta) 
  62] filter*(F, cons(X, Y)) >= cons(X, filter(F, Y))  because filter > cons, [58] and [63], by (Copy) 
  63] filter*(F, cons(X, Y)) >= filter(F, Y)  because filter in Mul, [64] and [3], by (Stat) 
  64] F >= F  by (Meta) 

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