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 place the elements of P in a dependency graph approximation G (see e.g. [Kop12, Thm. 7.27, 7.29], as follows:

    * 0 : 0 
    * 1 : 1 
    * 2 :  
    * 3 : 1 
    * 4 : 2, 3, 4, 5 
    * 5 : 0 
    * 6 : 6 
    * 7 :  
    * 8 : 7, 8, 9 
    * 9 : 7, 8, 9 

This graph has the following strongly connected components:

  P_1:

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

  P_2:

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

  P_3:

    d#(s(X), s(Y)) =#> d#(s(X), sub(Y, X))   

  P_4:

    len#(cons(X, Y)) =#> len#(Y)   

  P_5:

    filter#(F, cons(X, Y)) =#> filter#(F, Y)   
    filter#(F, cons(X, Y)) =#> filter#(F, Y)   

By [Kop12, Thm. 7.31], we may replace any dependency pair problem (P_0, R_0, m, f) by (P_1, R_0, m, f), (P_2, R_0, m, f), (P_3, R_0, m, f), (P_4, R_0, m, f) and (P_5, R_0, m, f).

Thus, the original system is terminating if each of (P_1, R_0, static, formative), (P_2, R_0, static, formative), (P_3, R_0, static, formative), (P_4, R_0, static, formative) and (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:

  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]] = _|_ 
  [[len(x_1)]] = x_1 
  [[nil]] = _|_ 
  [[sub(x_1, x_2)]] = x_1 
  [[true]] = _|_ 

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

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) 
  filter#(F, cons(X, Y)) > filter#(F, Y) 
  if(_|_, X, Y) >= X 
  if(_|_, X, Y) >= Y 
  X >= X 
  s(X) >= 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), Y)) 
  _|_ >= _|_ 
  cons(X, Y) >= s(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 (Star) 
  2] filter#*(F, cons(X, Y)) >= filter#(F, Y)  because filter# in Mul, [3] and [4], by (Stat) 
  3] F >= F  by (Meta) 
  4] cons(X, Y) > Y  because [5], by definition 
  5] cons*(X, Y) >= Y  because [6], by (Select) 
  6] Y >= Y  by (Meta) 

  7] filter#(F, cons(X, Y)) > filter#(F, Y)  because [8], by definition 
  8] filter#*(F, cons(X, Y)) >= filter#(F, Y)  because filter# in Mul, [3] and [4], by (Stat) 

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

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

  15] X >= X  by (Meta) 

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

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

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

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

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

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

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

  48] cons(X, Y) >= s(Y)  because [49], by (Star) 
  49] cons*(X, Y) >= s(Y)  because cons > s 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(@_{o -> o}(F, X), cons(X, filter(F, Y)), filter(F, Y))  because [54], by (Star) 
  54] filter*(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, filter(F, Y)), filter(F, Y))  because filter > if, [55], [61] and [62], by (Copy) 
  55] filter*(F, cons(X, Y)) >= @_{o -> o}(F, X)  because filter > @_{o -> o}, [56] and [57], by (Copy) 
  56] filter*(F, cons(X, Y)) >= F  because [3], by (Select) 
  57] filter*(F, cons(X, Y)) >= X  because [58], by (Select) 
  58] cons(X, Y) >= X  because [59], by (Star) 
  59] cons*(X, Y) >= X  because [60], by (Select) 
  60] X >= X  by (Meta) 
  61] filter*(F, cons(X, Y)) >= cons(X, filter(F, Y))  because filter > cons, [57] and [62], by (Copy) 
  62] filter*(F, cons(X, Y)) >= filter(F, Y)  because filter in Mul, [3] and [4], 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 each of (P_1, R_0, static, formative), (P_2, R_0, static, formative), (P_3, R_0, static, formative), (P_4, R_0, static, formative) and (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]] = _|_ 
  [[d(x_1, x_2)]] = d(x_2, x_1) 
  [[false]] = _|_ 
  [[filter#(x_1, x_2)]] = filter#(x_2, x_1) 
  [[nil]] = _|_ 
  [[sub(x_1, x_2)]] = sub(x_1) 
  [[true]] = _|_ 

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

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(_|_, 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] 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 [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] gtr(_|_, X) >= _|_  by (Bot) 

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

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

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

  36] d(s(X), s(Y)) >= if(gtr(X, Y), _|_, d(s(X), sub(Y)))  because [37], by (Star) 
  37] d*(s(X), s(Y)) >= if(gtr(X, Y), _|_, d(s(X), sub(Y)))  because d > if, [38], [47] and [48], by (Copy) 
  38] d*(s(X), s(Y)) >= gtr(X, Y)  because d > gtr, [39] and [43], by (Copy) 
  39] d*(s(X), s(Y)) >= X  because [40], by (Select) 
  40] s(X) >= X  because [41], by (Star) 
  41] s*(X) >= X  because [42], by (Select) 
  42] X >= X  by (Meta) 
  43] d*(s(X), s(Y)) >= Y  because [44], by (Select) 
  44] s(Y) >= Y  because [45], by (Star) 
  45] s*(Y) >= Y  because [46], by (Select) 
  46] Y >= Y  by (Meta) 
  47] d*(s(X), s(Y)) >= _|_  by (Bot) 
  48] d*(s(X), s(Y)) >= d(s(X), sub(Y))  because [49], [52] and [55], by (Stat) 
  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 [46], by (Select) 
  52] d*(s(X), s(Y)) >= s(X)  because [53], by (Select) 
  53] s(X) >= s(X)  because s in Mul and [54], by (Fun) 
  54] X >= X  by (Meta) 
  55] d*(s(X), s(Y)) >= sub(Y)  because d > sub and [43], by (Copy) 

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

  57] len(cons(X, Y)) >= s(len(Y))  because [58], by (Star) 
  58] len*(cons(X, Y)) >= s(len(Y))  because len > s and [59], by (Copy) 
  59] len*(cons(X, Y)) >= len(Y)  because len in Mul and [60], by (Stat) 
  60] cons(X, Y) > Y  because [61], by definition 
  61] cons*(X, Y) >= Y  because [62], by (Select) 
  62] Y >= Y  by (Meta) 

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

  64] filter(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, filter(F, Y)), filter(F, Y))  because [65], by (Star) 
  65] filter*(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, filter(F, Y)), filter(F, Y))  because filter > if, [66], [72] and [73], by (Copy) 
  66] filter*(F, cons(X, Y)) >= @_{o -> o}(F, X)  because filter > @_{o -> o}, [67] and [68], by (Copy) 
  67] filter*(F, cons(X, Y)) >= F  because [7], by (Select) 
  68] filter*(F, cons(X, Y)) >= X  because [69], by (Select) 
  69] cons(X, Y) >= X  because [70], by (Star) 
  70] cons*(X, Y) >= X  because [71], by (Select) 
  71] X >= X  by (Meta) 
  72] filter*(F, cons(X, Y)) >= cons(X, filter(F, Y))  because filter > cons, [68] and [73], by (Copy) 
  73] filter*(F, cons(X, Y)) >= filter(F, Y)  because filter in Mul, [74] and [3], by (Stat) 
  74] 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.

Thus, the original system is terminating if each of (P_1, R_0, static, formative), (P_2, R_0, static, formative), (P_3, R_0, static, formative) and (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:

  len#(cons(X, Y)) >? len#(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 = {len#} and Mul = {@_{o -> o}, cons, d, filter, gtr, if, len, s, sub}, and the following precedence: filter > @_{o -> o} > len > len# > cons > s > sub > d > gtr > if

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

  len#(cons(X, Y)) > len#(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] len#(cons(X, Y)) > len#(Y)  because [2], by definition 
  2] len#*(cons(X, Y)) >= len#(Y)  because [3] and [6], 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] len#*(cons(X, Y)) >= Y  because [7], by (Select) 
  7] cons(X, Y) >= Y  because [4], by (Star) 

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

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

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

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

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

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

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

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

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

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

  51] len(cons(X, Y)) >= s(len(Y))  because [52], by (Star) 
  52] len*(cons(X, Y)) >= s(len(Y))  because len > s and [53], by (Copy) 
  53] len*(cons(X, Y)) >= len(Y)  because len in Mul and [3], by (Stat) 

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

  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], [64] and [65], by (Copy) 
  57] filter*(F, cons(X, Y)) >= @_{o -> o}(F, X)  because filter > @_{o -> o}, [58] and [60], by (Copy) 
  58] filter*(F, cons(X, Y)) >= F  because [59], by (Select) 
  59] F >= F  by (Meta) 
  60] filter*(F, cons(X, Y)) >= X  because [61], by (Select) 
  61] cons(X, Y) >= X  because [62], by (Star) 
  62] cons*(X, Y) >= X  because [63], by (Select) 
  63] X >= X  by (Meta) 
  64] filter*(F, cons(X, Y)) >= cons(X, filter(F, Y))  because filter > cons, [60] and [65], by (Copy) 
  65] filter*(F, cons(X, Y)) >= filter(F, Y)  because filter in Mul, [66] and [67], by (Stat) 
  66] F >= F  by (Meta) 
  67] cons(X, Y) > Y  because [68], by definition 
  68] cons*(X, Y) >= Y  because [69], by (Select) 
  69] Y >= Y  by (Meta) 

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

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

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

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

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

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

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

  d#(s(X), s(Y)) > d#(s(X), sub(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(_|_, d(s(X), sub(Y))) 
  nil >= _|_ 
  cons(X, Y) >= s(Y) 
  filter(F, nil) >= nil 
  filter(F, cons(X, Y)) >= if(cons(X, filter(F, Y)), filter(F, Y)) 

With these choices, we have:

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

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

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

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

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

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

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

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

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

  30] d(s(X), s(Y)) >= if(_|_, d(s(X), sub(Y)))  because [31], by (Star) 
  31] d*(s(X), s(Y)) >= if(_|_, d(s(X), sub(Y)))  because d > if, [32] and [33], by (Copy) 
  32] d*(s(X), s(Y)) >= _|_  by (Bot) 
  33] d*(s(X), s(Y)) >= d(s(X), sub(Y))  because d in Mul, [3] and [5], by (Stat) 

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

  35] cons(X, Y) >= s(Y)  because [36], by (Star) 
  36] cons*(X, Y) >= s(Y)  because cons > s and [37], by (Copy) 
  37] cons*(X, Y) >= Y  because [38], by (Select) 
  38] Y >= Y  by (Meta) 

  39] filter(F, nil) >= nil  because [40], by (Star) 
  40] filter*(F, nil) >= nil  because filter > nil, by (Copy) 

  41] filter(F, cons(X, Y)) >= if(cons(X, filter(F, Y)), filter(F, Y))  because [42], by (Star) 
  42] filter*(F, cons(X, Y)) >= if(cons(X, filter(F, Y)), filter(F, Y))  because filter > if, [43] and [48], by (Copy) 
  43] filter*(F, cons(X, Y)) >= cons(X, filter(F, Y))  because filter > cons, [44] and [48], by (Copy) 
  44] filter*(F, cons(X, Y)) >= X  because [45], by (Select) 
  45] cons(X, Y) >= X  because [46], by (Star) 
  46] cons*(X, Y) >= X  because [47], by (Select) 
  47] X >= X  by (Meta) 
  48] filter*(F, cons(X, Y)) >= filter(F, Y)  because filter in Mul, [49] and [50], by (Stat) 
  49] F >= F  by (Meta) 
  50] cons(X, Y) > Y  because [51], by definition 
  51] cons*(X, Y) >= Y  because [52], by (Select) 
  52] Y >= Y  by (Meta) 

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

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

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

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

  gtr#(s(X), s(Y)) >? gtr#(X, 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]] = _|_ 
  [[gtr(x_1, x_2)]] = _|_ 
  [[nil]] = _|_ 
  [[sub(x_1, x_2)]] = sub(x_1) 
  [[true]] = _|_ 

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

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) 
  if(_|_, X, Y) >= X 
  if(_|_, X, Y) >= Y 
  sub(X) >= X 
  sub(s(X)) >= sub(X) 
  _|_ >= _|_ 
  _|_ >= _|_ 
  _|_ >= _|_ 
  _|_ >= _|_ 
  s(X) >= if(_|_, _|_, sub(X)) 
  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 [3], [6] and [8], by (Stat) 
  3] s(X) > X  because [4], by definition 
  4] s*(X) >= X  because [5], by (Select) 
  5] X >= X  by (Meta) 
  6] gtr#*(s(X), s(Y)) >= X  because [7], by (Select) 
  7] s(X) >= X  because [4], by (Star) 
  8] gtr#*(s(X), s(Y)) >= Y  because [9], by (Select) 
  9] s(Y) >= Y  because [10], by (Star) 
  10] s*(Y) >= Y  because [11], by (Select) 
  11] Y >= Y  by (Meta) 

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

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

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

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

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

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

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

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

  31] s(X) >= if(_|_, _|_, sub(X))  because [32], by (Star) 
  32] s*(X) >= if(_|_, _|_, sub(X))  because s > if, [33], [34] and [35], by (Copy) 
  33] s*(X) >= _|_  by (Bot) 
  34] s*(X) >= _|_  by (Bot) 
  35] s*(X) >= sub(X)  because s > sub and [36], by (Copy) 
  36] s*(X) >= X  because [37], by (Select) 
  37] X >= X  by (Meta) 

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

  39] len(cons(X, Y)) >= s(len(Y))  because [40], by (Star) 
  40] len*(cons(X, Y)) >= s(len(Y))  because [41], by (Select) 
  41] cons(X, Y) >= s(len(Y))  because [42], by (Star) 
  42] cons*(X, Y) >= s(len(Y))  because cons > s and [43], by (Copy) 
  43] cons*(X, Y) >= len(Y)  because cons > len and [44], by (Copy) 
  44] cons*(X, Y) >= Y  because [45], by (Select) 
  45] Y >= Y  by (Meta) 

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

  47] filter(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, filter(F, Y)), filter(F, Y))  because [48], by (Star) 
  48] filter*(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, filter(F, Y)), filter(F, Y))  because filter > if, [49], [56] and [57], by (Copy) 
  49] filter*(F, cons(X, Y)) >= @_{o -> o}(F, X)  because filter > @_{o -> o}, [50] and [52], by (Copy) 
  50] filter*(F, cons(X, Y)) >= F  because [51], by (Select) 
  51] F >= F  by (Meta) 
  52] filter*(F, cons(X, Y)) >= X  because [53], by (Select) 
  53] cons(X, Y) >= X  because [54], by (Star) 
  54] cons*(X, Y) >= X  because [55], by (Select) 
  55] X >= X  by (Meta) 
  56] filter*(F, cons(X, Y)) >= cons(X, filter(F, Y))  because filter > cons, [52] and [57], by (Copy) 
  57] filter*(F, cons(X, Y)) >= filter(F, Y)  because filter in Mul, [58] and [59], by (Stat) 
  58] F >= F  by (Meta) 
  59] cons(X, Y) > Y  because [60], by definition 
  60] cons*(X, Y) >= Y  because [61], by (Select) 
  61] Y >= Y  by (Meta) 

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

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

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

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

  sub#(s(X), s(Y)) >? sub#(X, 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]] = _|_ 
  [[len(x_1)]] = x_1 
  [[nil]] = _|_ 
  [[sub(x_1, x_2)]] = x_1 
  [[sub#(x_1, x_2)]] = sub#(x_2, x_1) 
  [[true]] = _|_ 

We choose Lex = {sub#} and Mul = {@_{o -> o}, cons, d, filter, gtr, if, s}, and the following precedence: filter > @_{o -> o} > cons > 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:

  sub#(s(X), s(Y)) > sub#(X, Y) 
  if(_|_, X, Y) >= X 
  if(_|_, X, Y) >= Y 
  X >= X 
  s(X) >= 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), Y)) 
  _|_ >= _|_ 
  cons(X, Y) >= s(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 [2], by definition 
  2] sub#*(s(X), s(Y)) >= sub#(X, Y)  because [3], [6] and [10], by (Stat) 
  3] s(Y) > Y  because [4], by definition 
  4] s*(Y) >= Y  because [5], by (Select) 
  5] Y >= Y  by (Meta) 
  6] sub#*(s(X), s(Y)) >= X  because [7], by (Select) 
  7] s(X) >= X  because [8], by (Star) 
  8] s*(X) >= X  because [9], by (Select) 
  9] X >= X  by (Meta) 
  10] sub#*(s(X), s(Y)) >= Y  because [11], by (Select) 
  11] s(Y) >= Y  because [4], by (Star) 

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

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

  18] X >= X  by (Meta) 

  19] s(X) >= X  because [8], by (Star) 

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

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

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

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

  31] d(s(X), s(Y)) >= if(gtr(X, Y), _|_, d(s(X), Y))  because [32], by (Star) 
  32] d*(s(X), s(Y)) >= if(gtr(X, Y), _|_, d(s(X), Y))  because d > if, [33], [42] and [43], by (Copy) 
  33] d*(s(X), s(Y)) >= gtr(X, Y)  because d > gtr, [34] and [38], 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)) >= Y  because [39], by (Select) 
  39] s(Y) >= Y  because [40], by (Star) 
  40] s*(Y) >= Y  because [41], by (Select) 
  41] Y >= Y  by (Meta) 
  42] d*(s(X), s(Y)) >= _|_  by (Bot) 
  43] d*(s(X), s(Y)) >= d(s(X), Y)  because d in Mul, [44] and [46], by (Stat) 
  44] s(X) >= s(X)  because s in Mul and [45], by (Fun) 
  45] X >= X  by (Meta) 
  46] s(Y) > Y  because [47], by definition 
  47] s*(Y) >= Y  because [41], by (Select) 

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

  49] cons(X, Y) >= s(Y)  because [50], by (Star) 
  50] cons*(X, Y) >= s(Y)  because cons > s and [51], by (Copy) 
  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], [63] and [64], by (Copy) 
  56] filter*(F, cons(X, Y)) >= @_{o -> o}(F, X)  because filter > @_{o -> o}, [57] and [59], by (Copy) 
  57] filter*(F, cons(X, Y)) >= F  because [58], by (Select) 
  58] F >= F  by (Meta) 
  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, [65] and [66], by (Stat) 
  65] F >= F  by (Meta) 
  66] cons(X, Y) > Y  because [67], by definition 
  67] cons*(X, Y) >= Y  because [68], by (Select) 
  68] Y >= Y  by (Meta) 

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

As all dependency pair problems were succesfully simplified with sound (and complete) processors until nothing remained, we conclude termination.


+++ Citations +++

[Kop12]  C. Kop.  Higher Order Termination.  PhD Thesis, 2012.
[Kop13]  C. Kop.  Static Dependency Pairs with Accessibility.  Unpublished manuscript, http://cl-informatik.uibk.ac.at/users/kop/static.pdf, 2013.
[KusIsoSakBla09]  K. Kusakari, Y. Isogai, M. Sakai, and F. Blanqui.  Static Dependency Pair Method Based On Strong Computability for Higher-Order Rewrite Systems.  In volume 92(10) of IEICE Transactions on Information and Systems.  2007--2015, 2009.