We consider the system Applicative_first_order_05__#3.55.

  Alphabet:

    0 : [] --> b 
    add : [b * c] --> c 
    app : [c * c] --> c 
    false : [] --> a 
    filter : [b -> a * c] --> c 
    filter2 : [a * b -> a * b * c] --> c 
    high : [b * c] --> c 
    if!fac6220high : [a * b * c] --> c 
    if!fac6220low : [a * b * c] --> c 
    le : [b * b] --> a 
    low : [b * c] --> c 
    map : [b -> b * c] --> c 
    minus : [b * b] --> b 
    nil : [] --> c 
    quicksort : [c] --> c 
    quot : [b * b] --> b 
    s : [b] --> b 
    true : [] --> a 

  Rules:

    minus(x, 0) => x 
    minus(s(x), s(y)) => minus(x, y) 
    quot(0, s(x)) => 0 
    quot(s(x), s(y)) => s(quot(minus(x, y), s(y))) 
    le(0, x) => true 
    le(s(x), 0) => false 
    le(s(x), s(y)) => le(x, y) 
    app(nil, x) => x 
    app(add(x, y), z) => add(x, app(y, z)) 
    low(x, nil) => nil 
    low(x, add(y, z)) => if!fac6220low(le(y, x), x, add(y, z)) 
    if!fac6220low(true, x, add(y, z)) => add(y, low(x, z)) 
    if!fac6220low(false, x, add(y, z)) => low(x, z) 
    high(x, nil) => nil 
    high(x, add(y, z)) => if!fac6220high(le(y, x), x, add(y, z)) 
    if!fac6220high(true, x, add(y, z)) => high(x, z) 
    if!fac6220high(false, x, add(y, z)) => add(y, high(x, z)) 
    quicksort(nil) => nil 
    quicksort(add(x, y)) => app(quicksort(low(x, y)), add(x, quicksort(high(x, y)))) 
    map(f, nil) => nil 
    map(f, add(x, y)) => add(f x, map(f, y)) 
    filter(f, nil) => nil 
    filter(f, add(x, y)) => filter2(f x, f, x, y) 
    filter2(true, f, x, y) => add(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 dynamic dependency pairs.

After applying [Kop12, Thm. 7.22] to denote collapsing dependency pairs in an extended form, we thus obtain the following dependency pair problem (P_0, R_0, minimal, formative):

  Dependency Pairs P_0:

    0] minus#(s(X), s(Y)) =#> minus#(X, Y)   
    1] quot#(s(X), s(Y)) =#> quot#(minus(X, Y), s(Y))   
    2] quot#(s(X), s(Y)) =#> minus#(X, Y)   
    3] le#(s(X), s(Y)) =#> le#(X, Y)   
    4] app#(add(X, Y), Z) =#> app#(Y, Z)   
    5] low#(X, add(Y, Z)) =#> if!fac6220low#(le(Y, X), X, add(Y, Z))   
    6] low#(X, add(Y, Z)) =#> le#(Y, X)   
    7] if!fac6220low#(true, X, add(Y, Z)) =#> low#(X, Z)   
    8] if!fac6220low#(false, X, add(Y, Z)) =#> low#(X, Z)   
    9] high#(X, add(Y, Z)) =#> if!fac6220high#(le(Y, X), X, add(Y, Z))   
    10] high#(X, add(Y, Z)) =#> le#(Y, X)   
    11] if!fac6220high#(true, X, add(Y, Z)) =#> high#(X, Z)   
    12] if!fac6220high#(false, X, add(Y, Z)) =#> high#(X, Z)   
    13] quicksort#(add(X, Y)) =#> app#(quicksort(low(X, Y)), add(X, quicksort(high(X, Y))))   
    14] quicksort#(add(X, Y)) =#> quicksort#(low(X, Y))   
    15] quicksort#(add(X, Y)) =#> low#(X, Y)   
    16] quicksort#(add(X, Y)) =#> quicksort#(high(X, Y))   
    17] quicksort#(add(X, Y)) =#> high#(X, Y)   
    18] map#(F, add(X, Y)) =#> F(X)   
    19] map#(F, add(X, Y)) =#> map#(F, Y)   
    20] filter#(F, add(X, Y)) =#> filter2#(F X, F, X, Y)   
    21] filter#(F, add(X, Y)) =#> F(X)   
    22] filter2#(true, F, X, Y) =#> filter#(F, Y)   
    23] filter2#(false, F, X, Y) =#> filter#(F, Y)   

  Rules R_0:

    minus(X, 0) => X 
    minus(s(X), s(Y)) => minus(X, Y) 
    quot(0, s(X)) => 0 
    quot(s(X), s(Y)) => s(quot(minus(X, Y), s(Y))) 
    le(0, X) => true 
    le(s(X), 0) => false 
    le(s(X), s(Y)) => le(X, Y) 
    app(nil, X) => X 
    app(add(X, Y), Z) => add(X, app(Y, Z)) 
    low(X, nil) => nil 
    low(X, add(Y, Z)) => if!fac6220low(le(Y, X), X, add(Y, Z)) 
    if!fac6220low(true, X, add(Y, Z)) => add(Y, low(X, Z)) 
    if!fac6220low(false, X, add(Y, Z)) => low(X, Z) 
    high(X, nil) => nil 
    high(X, add(Y, Z)) => if!fac6220high(le(Y, X), X, add(Y, Z)) 
    if!fac6220high(true, X, add(Y, Z)) => high(X, Z) 
    if!fac6220high(false, X, add(Y, Z)) => add(Y, high(X, Z)) 
    quicksort(nil) => nil 
    quicksort(add(X, Y)) => app(quicksort(low(X, Y)), add(X, quicksort(high(X, Y)))) 
    map(F, nil) => nil 
    map(F, add(X, Y)) => add(F X, map(F, Y)) 
    filter(F, nil) => nil 
    filter(F, add(X, Y)) => filter2(F X, F, X, Y) 
    filter2(true, F, X, Y) => add(X, filter(F, Y)) 
    filter2(false, F, X, Y) => filter(F, Y) 

Thus, the original system is terminating if (P_0, R_0, minimal, formative) is finite.

We consider the dependency pair problem (P_0, R_0, minimal, 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 
    * 2 : 0 
    * 3 : 3 
    * 4 : 4 
    * 5 : 7, 8 
    * 6 : 3 
    * 7 : 5, 6 
    * 8 : 5, 6 
    * 9 : 11, 12 
    * 10 : 3 
    * 11 : 9, 10 
    * 12 : 9, 10 
    * 13 : 4 
    * 14 : 13, 14, 15, 16, 17 
    * 15 : 5, 6 
    * 16 : 13, 14, 15, 16, 17 
    * 17 : 9, 10 
    * 18 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 
    * 19 : 18, 19 
    * 20 : 22, 23 
    * 21 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 
    * 22 : 20, 21 
    * 23 : 20, 21 

This graph has the following strongly connected components:

  P_1:

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

  P_2:

    quot#(s(X), s(Y)) =#> quot#(minus(X, Y), s(Y))   

  P_3:

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

  P_4:

    app#(add(X, Y), Z) =#> app#(Y, Z)   

  P_5:

    low#(X, add(Y, Z)) =#> if!fac6220low#(le(Y, X), X, add(Y, Z))   
    if!fac6220low#(true, X, add(Y, Z)) =#> low#(X, Z)   
    if!fac6220low#(false, X, add(Y, Z)) =#> low#(X, Z)   

  P_6:

    high#(X, add(Y, Z)) =#> if!fac6220high#(le(Y, X), X, add(Y, Z))   
    if!fac6220high#(true, X, add(Y, Z)) =#> high#(X, Z)   
    if!fac6220high#(false, X, add(Y, Z)) =#> high#(X, Z)   

  P_7:

    quicksort#(add(X, Y)) =#> quicksort#(low(X, Y))   
    quicksort#(add(X, Y)) =#> quicksort#(high(X, Y))   

  P_8:

    map#(F, add(X, Y)) =#> F(X)   
    map#(F, add(X, Y)) =#> map#(F, Y)   
    filter#(F, add(X, Y)) =#> filter2#(F X, F, X, Y)   
    filter#(F, add(X, Y)) =#> F(X)   
    filter2#(true, F, X, Y) =#> filter#(F, Y)   
    filter2#(false, F, 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), (P_5, R_0, m, f), (P_6, R_0, m, f), (P_7, R_0, m, f) and (P_8, R_0, m, f).

Thus, the original system is terminating if each of (P_1, R_0, minimal, formative), (P_2, R_0, minimal, formative), (P_3, R_0, minimal, formative), (P_4, R_0, minimal, formative), (P_5, R_0, minimal, formative), (P_6, R_0, minimal, formative), (P_7, R_0, minimal, formative) and (P_8, R_0, minimal, formative) is finite.

We consider the dependency pair problem (P_8, R_0, minimal, formative).

We will use the reduction pair processor [Kop12, Thm. 7.16].  As the system is abstraction-simple and the formative flag is set, it suffices to find a tagged reduction pair [Kop12, Def. 6.70].  Thus, we must orient:

  map#(F, add(X, Y)) >? F(X) 
  map#(F, add(X, Y)) >? map#(F, Y) 
  filter#(F, add(X, Y)) >? filter2#(F X, F, X, Y) 
  filter#(F, add(X, Y)) >? F(X) 
  filter2#(true, F, X, Y) >? filter#(F, Y) 
  filter2#(false, F, X, Y) >? filter#(F, Y) 
  minus(X, 0) >= X 
  minus(s(X), s(Y)) >= minus(X, Y) 
  quot(0, s(X)) >= 0 
  quot(s(X), s(Y)) >= s(quot(minus(X, Y), s(Y))) 
  le(0, X) >= true 
  le(s(X), 0) >= false 
  le(s(X), s(Y)) >= le(X, Y) 
  app(nil, X) >= X 
  app(add(X, Y), Z) >= add(X, app(Y, Z)) 
  low(X, nil) >= nil 
  low(X, add(Y, Z)) >= if!fac6220low(le(Y, X), X, add(Y, Z)) 
  if!fac6220low(true, X, add(Y, Z)) >= add(Y, low(X, Z)) 
  if!fac6220low(false, X, add(Y, Z)) >= low(X, Z) 
  high(X, nil) >= nil 
  high(X, add(Y, Z)) >= if!fac6220high(le(Y, X), X, add(Y, Z)) 
  if!fac6220high(true, X, add(Y, Z)) >= high(X, Z) 
  if!fac6220high(false, X, add(Y, Z)) >= add(Y, high(X, Z)) 
  quicksort(nil) >= nil 
  quicksort(add(X, Y)) >= app(quicksort(low(X, Y)), add(X, quicksort(high(X, Y)))) 
  map(F, nil) >= nil 
  map(F, add(X, Y)) >= add(F X, map(F, Y)) 
  filter(F, nil) >= nil 
  filter(F, add(X, Y)) >= filter2(F X, F, X, Y) 
  filter2(true, F, X, Y) >= add(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]] = _|_ 
  [[false]] = _|_ 
  [[filter2(x_1, x_2, x_3, x_4)]] = filter2(x_2, x_4, x_3, x_1) 
  [[filter2#(x_1, x_2, x_3, x_4)]] = filter2#(x_2, x_4) 
  [[high(x_1, x_2)]] = high(x_2) 
  [[if!fac6220high(x_1, x_2, x_3)]] = if!fac6220high(x_3) 
  [[if!fac6220low(x_1, x_2, x_3)]] = if!fac6220low(x_3) 
  [[low(x_1, x_2)]] = low(x_2) 
  [[minus(x_1, x_2)]] = x_1 
  [[nil]] = _|_ 
  [[s(x_1)]] = x_1 
  [[true]] = _|_ 

We choose Lex = {filter, filter2} and Mul = {@_{o -> o}, add, app, filter2#, filter#, high, if!fac6220high, if!fac6220low, le, low, map, map#, quicksort, quot}, and the following precedence: filter = filter2 > le > map > quicksort > app > quot > add = high = if!fac6220high = if!fac6220low = low > filter2# = filter# > map# > @_{o -> o}

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

  map#(F, add(X, Y)) >= @_{o -> o}(F, X) 
  map#(F, add(X, Y)) >= map#(F, Y) 
  filter#(F, add(X, Y)) >= filter2#(F, Y) 
  filter#(F, add(X, Y)) > @_{o -> o}(F, X) 
  filter2#(F, X) >= filter#(F, X) 
  filter2#(F, X) >= filter#(F, X) 
  X >= X 
  X >= X 
  quot(_|_, X) >= _|_ 
  quot(X, Y) >= quot(X, Y) 
  le(_|_, X) >= _|_ 
  le(X, _|_) >= _|_ 
  le(X, Y) >= le(X, Y) 
  app(_|_, X) >= X 
  app(add(X, Y), Z) >= add(X, app(Y, Z)) 
  low(_|_) >= _|_ 
  low(add(X, Y)) >= if!fac6220low(add(X, Y)) 
  if!fac6220low(add(X, Y)) >= add(X, low(Y)) 
  if!fac6220low(add(X, Y)) >= low(Y) 
  high(_|_) >= _|_ 
  high(add(X, Y)) >= if!fac6220high(add(X, Y)) 
  if!fac6220high(add(X, Y)) >= high(Y) 
  if!fac6220high(add(X, Y)) >= add(X, high(Y)) 
  quicksort(_|_) >= _|_ 
  quicksort(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(high(Y)))) 
  map(F, _|_) >= _|_ 
  map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) 
  filter(F, _|_) >= _|_ 
  filter(F, add(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) 
  filter2(_|_, F, X, Y) >= add(X, filter(F, Y)) 
  filter2(_|_, F, X, Y) >= filter(F, Y) 

With these choices, we have:

  1] map#(F, add(X, Y)) >= @_{o -> o}(F, X)  because [2], by (Star) 
  2] map#*(F, add(X, Y)) >= @_{o -> o}(F, X)  because map# > @_{o -> o}, [3] and [5], by (Copy) 
  3] map#*(F, add(X, Y)) >= F  because [4], by (Select) 
  4] F >= F  by (Meta) 
  5] map#*(F, add(X, Y)) >= X  because [6], by (Select) 
  6] add(X, Y) >= X  because [7], by (Star) 
  7] add*(X, Y) >= X  because [8], by (Select) 
  8] X >= X  by (Meta) 

  9] map#(F, add(X, Y)) >= map#(F, Y)  because map# in Mul, [10] and [11], by (Fun) 
  10] F >= F  by (Meta) 
  11] add(X, Y) >= Y  because [12], by (Star) 
  12] add*(X, Y) >= Y  because [13], by (Select) 
  13] Y >= Y  by (Meta) 

  14] filter#(F, add(X, Y)) >= filter2#(F, Y)  because filter# = filter2#, filter# in Mul, [15] and [16], by (Fun) 
  15] F >= F  by (Meta) 
  16] add(X, Y) >= Y  because [17], by (Star) 
  17] add*(X, Y) >= Y  because [18], by (Select) 
  18] Y >= Y  by (Meta) 

  19] filter#(F, add(X, Y)) > @_{o -> o}(F, X)  because [20], by definition 
  20] filter#*(F, add(X, Y)) >= @_{o -> o}(F, X)  because filter# > @_{o -> o}, [21] and [22], by (Copy) 
  21] filter#*(F, add(X, Y)) >= F  because [15], by (Select) 
  22] filter#*(F, add(X, Y)) >= X  because [23], by (Select) 
  23] add(X, Y) >= X  because [24], by (Star) 
  24] add*(X, Y) >= X  because [25], by (Select) 
  25] X >= X  by (Meta) 

  26] filter2#(F, X) >= filter#(F, X)  because filter2# = filter#, filter2# in Mul, [27] and [28], by (Fun) 
  27] F >= F  by (Meta) 
  28] X >= X  by (Meta) 

  29] filter2#(F, X) >= filter#(F, X)  because filter2# = filter#, filter2# in Mul, [30] and [31], by (Fun) 
  30] F >= F  by (Meta) 
  31] X >= X  by (Meta) 

  32] X >= X  by (Meta) 

  33] X >= X  by (Meta) 

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

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

  38] le(_|_, X) >= _|_  by (Bot) 

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

  40] le(X, Y) >= le(X, Y)  because le in Mul, [41] and [42], by (Fun) 
  41] X >= X  by (Meta) 
  42] Y >= Y  by (Meta) 

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

  46] app(add(X, Y), Z) >= add(X, app(Y, Z))  because [47], by (Star) 
  47] app*(add(X, Y), Z) >= add(X, app(Y, Z))  because app > add, [48] and [52], by (Copy) 
  48] app*(add(X, Y), Z) >= X  because [49], by (Select) 
  49] add(X, Y) >= X  because [50], by (Star) 
  50] add*(X, Y) >= X  because [51], by (Select) 
  51] X >= X  by (Meta) 
  52] app*(add(X, Y), Z) >= app(Y, Z)  because app in Mul, [53] and [56], by (Stat) 
  53] add(X, Y) > Y  because [54], by definition 
  54] add*(X, Y) >= Y  because [55], by (Select) 
  55] Y >= Y  by (Meta) 
  56] Z >= Z  by (Meta) 

  57] low(_|_) >= _|_  by (Bot) 

  58] low(add(X, Y)) >= if!fac6220low(add(X, Y))  because low = if!fac6220low, low in Mul and [59], by (Fun) 
  59] add(X, Y) >= add(X, Y)  because add in Mul, [60] and [61], by (Fun) 
  60] X >= X  by (Meta) 
  61] Y >= Y  by (Meta) 

  62] if!fac6220low(add(X, Y)) >= add(X, low(Y))  because [63], by (Star) 
  63] if!fac6220low*(add(X, Y)) >= add(X, low(Y))  because if!fac6220low = add, if!fac6220low in Mul, [64] and [67], by (Stat) 
  64] add(X, Y) > X  because [65], by definition 
  65] add*(X, Y) >= X  because [66], by (Select) 
  66] X >= X  by (Meta) 
  67] add(X, Y) > low(Y)  because [68], by definition 
  68] add*(X, Y) >= low(Y)  because add = low, add in Mul and [69], by (Stat) 
  69] Y >= Y  by (Meta) 

  70] if!fac6220low(add(X, Y)) >= low(Y)  because if!fac6220low = low, if!fac6220low in Mul and [71], by (Fun) 
  71] add(X, Y) >= Y  because [72], by (Star) 
  72] add*(X, Y) >= Y  because [73], by (Select) 
  73] Y >= Y  by (Meta) 

  74] high(_|_) >= _|_  by (Bot) 

  75] high(add(X, Y)) >= if!fac6220high(add(X, Y))  because high = if!fac6220high, high in Mul and [76], by (Fun) 
  76] add(X, Y) >= add(X, Y)  because add in Mul, [77] and [78], by (Fun) 
  77] X >= X  by (Meta) 
  78] Y >= Y  by (Meta) 

  79] if!fac6220high(add(X, Y)) >= high(Y)  because if!fac6220high = high, if!fac6220high in Mul and [80], by (Fun) 
  80] add(X, Y) >= Y  because [81], by (Star) 
  81] add*(X, Y) >= Y  because [82], by (Select) 
  82] Y >= Y  by (Meta) 

  83] if!fac6220high(add(X, Y)) >= add(X, high(Y))  because [84], by (Star) 
  84] if!fac6220high*(add(X, Y)) >= add(X, high(Y))  because if!fac6220high = add, if!fac6220high in Mul, [85] and [88], by (Stat) 
  85] add(X, Y) > X  because [86], by definition 
  86] add*(X, Y) >= X  because [87], by (Select) 
  87] X >= X  by (Meta) 
  88] add(X, Y) > high(Y)  because [89], by definition 
  89] add*(X, Y) >= high(Y)  because add = high, add in Mul and [90], by (Stat) 
  90] Y >= Y  by (Meta) 

  91] quicksort(_|_) >= _|_  by (Bot) 

  92] quicksort(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(high(Y))))  because [93], by (Star) 
  93] quicksort*(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(high(Y))))  because quicksort > app, [94] and [98], by (Copy) 
  94] quicksort*(add(X, Y)) >= quicksort(low(Y))  because quicksort in Mul and [95], by (Stat) 
  95] add(X, Y) > low(Y)  because [96], by definition 
  96] add*(X, Y) >= low(Y)  because add = low, add in Mul and [97], by (Stat) 
  97] Y >= Y  by (Meta) 
  98] quicksort*(add(X, Y)) >= add(X, quicksort(high(Y)))  because quicksort > add, [99] and [103], by (Copy) 
  99] quicksort*(add(X, Y)) >= X  because [100], by (Select) 
  100] add(X, Y) >= X  because [101], by (Star) 
  101] add*(X, Y) >= X  because [102], by (Select) 
  102] X >= X  by (Meta) 
  103] quicksort*(add(X, Y)) >= quicksort(high(Y))  because quicksort in Mul and [104], by (Stat) 
  104] add(X, Y) > high(Y)  because [105], by definition 
  105] add*(X, Y) >= high(Y)  because add = high, add in Mul and [97], by (Stat) 

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

  107] map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y))  because [108], by (Star) 
  108] map*(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y))  because map > add, [109] and [112], by (Copy) 
  109] map*(F, add(X, Y)) >= @_{o -> o}(F, X)  because map > @_{o -> o}, [110] and [111], by (Copy) 
  110] map*(F, add(X, Y)) >= F  because [10], by (Select) 
  111] map*(F, add(X, Y)) >= X  because [6], by (Select) 
  112] map*(F, add(X, Y)) >= map(F, Y)  because map in Mul, [10] and [113], by (Stat) 
  113] add(X, Y) > Y  because [114], by definition 
  114] add*(X, Y) >= Y  because [13], by (Select) 

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

  116] filter(F, add(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y)  because [117], by (Star) 
  117] filter*(F, add(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y)  because filter = filter2, [15], [118], [120], [121], [122] and [123], by (Stat) 
  118] add(X, Y) > Y  because [119], by definition 
  119] add*(X, Y) >= Y  because [18], by (Select) 
  120] filter*(F, add(X, Y)) >= @_{o -> o}(F, X)  because filter > @_{o -> o}, [121] and [122], by (Copy) 
  121] filter*(F, add(X, Y)) >= F  because [15], by (Select) 
  122] filter*(F, add(X, Y)) >= X  because [23], by (Select) 
  123] filter*(F, add(X, Y)) >= Y  because [16], by (Select) 

  124] filter2(_|_, F, X, Y) >= add(X, filter(F, Y))  because [125], by (Star) 
  125] filter2*(_|_, F, X, Y) >= add(X, filter(F, Y))  because filter2 > add, [126] and [128], by (Copy) 
  126] filter2*(_|_, F, X, Y) >= X  because [127], by (Select) 
  127] X >= X  by (Meta) 
  128] filter2*(_|_, F, X, Y) >= filter(F, Y)  because filter2 = filter, [27], [28], [129] and [130], by (Stat) 
  129] filter2*(_|_, F, X, Y) >= F  because [27], by (Select) 
  130] filter2*(_|_, F, X, Y) >= Y  because [28], by (Select) 

  131] filter2(_|_, F, X, Y) >= filter(F, Y)  because [132], by (Star) 
  132] filter2*(_|_, F, X, Y) >= filter(F, Y)  because filter2 = filter, [30], [31], [133] and [134], by (Stat) 
  133] filter2*(_|_, F, X, Y) >= F  because [30], by (Select) 
  134] filter2*(_|_, F, X, Y) >= Y  because [31], by (Select) 

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

  map#(F, add(X, Y)) =#> F(X)   
  map#(F, add(X, Y)) =#> map#(F, Y)   
  filter#(F, add(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 each of (P_1, R_0, minimal, formative), (P_2, R_0, minimal, formative), (P_3, R_0, minimal, formative), (P_4, R_0, minimal, formative), (P_5, R_0, minimal, formative), (P_6, R_0, minimal, formative), (P_7, R_0, minimal, formative) and (P_9, R_0, minimal, formative) is finite.

We consider the dependency pair problem (P_9, R_0, minimal, 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, 2, 3, 4 
    * 1 : 0, 1 
    * 2 : 3, 4 
    * 3 : 2 
    * 4 : 2 

This graph has the following strongly connected components:

  P_10:

    map#(F, add(X, Y)) =#> F(X)   
    map#(F, add(X, Y)) =#> map#(F, Y)   

  P_11:

    filter#(F, add(X, Y)) =#> filter2#(F X, F, X, Y)   
    filter2#(true, F, X, Y) =#> filter#(F, Y)   
    filter2#(false, F, X, Y) =#> filter#(F, Y)   

By [Kop12, Thm. 7.31], we may replace any dependency pair problem (P_9, R_0, m, f) by (P_10, R_0, m, f) and (P_11, R_0, m, f).

Thus, the original system is terminating if each of (P_1, R_0, minimal, formative), (P_2, R_0, minimal, formative), (P_3, R_0, minimal, formative), (P_4, R_0, minimal, formative), (P_5, R_0, minimal, formative), (P_6, R_0, minimal, formative), (P_7, R_0, minimal, formative), (P_10, R_0, minimal, formative) and (P_11, R_0, minimal, formative) is finite.

We consider the dependency pair problem (P_11, R_0, minimal, formative).

We apply the subterm criterion with the following projection function:

  nu(filter2#) = 4 
  nu(filter#) = 2 

Thus, we can orient the dependency pairs as follows:

  nu(filter#(F, add(X, Y))) = add(X, Y) |> Y = nu(filter2#(F X, F, X, Y)) 
  nu(filter2#(true, F, X, Y)) = Y = Y = nu(filter#(F, Y)) 
  nu(filter2#(false, F, X, Y)) = Y = Y = nu(filter#(F, Y)) 

By [Kop12, Thm. 7.35], we may replace a dependency pair problem (P_11, R_0, minimal, f) by (P_12, R_0, minimal, f), where P_12 contains:

  filter2#(true, F, X, Y) =#> filter#(F, Y)   
  filter2#(false, F, X, Y) =#> filter#(F, Y)   

Thus, the original system is terminating if each of (P_1, R_0, minimal, formative), (P_2, R_0, minimal, formative), (P_3, R_0, minimal, formative), (P_4, R_0, minimal, formative), (P_5, R_0, minimal, formative), (P_6, R_0, minimal, formative), (P_7, R_0, minimal, formative), (P_10, R_0, minimal, formative) and (P_12, R_0, minimal, formative) is finite.

We consider the dependency pair problem (P_12, R_0, minimal, 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 :  
    * 1 :  

This graph has no strongly connected components.  By [Kop12, Thm. 7.31], this implies finiteness of the dependency pair problem.

Thus, the original system is terminating if each of (P_1, R_0, minimal, formative), (P_2, R_0, minimal, formative), (P_3, R_0, minimal, formative), (P_4, R_0, minimal, formative), (P_5, R_0, minimal, formative), (P_6, R_0, minimal, formative), (P_7, R_0, minimal, formative) and (P_10, R_0, minimal, formative) is finite.

We consider the dependency pair problem (P_10, R_0, minimal, formative).

We will use the reduction pair processor [Kop12, Thm. 7.16].  As the system is abstraction-simple and the formative flag is set, it suffices to find a tagged reduction pair [Kop12, Def. 6.70].  Thus, we must orient:

  map#(F, add(X, Y)) >? F(X) 
  map#(F, add(X, Y)) >? map#(F, Y) 
  minus(X, 0) >= X 
  minus(s(X), s(Y)) >= minus(X, Y) 
  quot(0, s(X)) >= 0 
  quot(s(X), s(Y)) >= s(quot(minus(X, Y), s(Y))) 
  le(0, X) >= true 
  le(s(X), 0) >= false 
  le(s(X), s(Y)) >= le(X, Y) 
  app(nil, X) >= X 
  app(add(X, Y), Z) >= add(X, app(Y, Z)) 
  low(X, nil) >= nil 
  low(X, add(Y, Z)) >= if!fac6220low(le(Y, X), X, add(Y, Z)) 
  if!fac6220low(true, X, add(Y, Z)) >= add(Y, low(X, Z)) 
  if!fac6220low(false, X, add(Y, Z)) >= low(X, Z) 
  high(X, nil) >= nil 
  high(X, add(Y, Z)) >= if!fac6220high(le(Y, X), X, add(Y, Z)) 
  if!fac6220high(true, X, add(Y, Z)) >= high(X, Z) 
  if!fac6220high(false, X, add(Y, Z)) >= add(Y, high(X, Z)) 
  quicksort(nil) >= nil 
  quicksort(add(X, Y)) >= app(quicksort(low(X, Y)), add(X, quicksort(high(X, Y)))) 
  map(F, nil) >= nil 
  map(F, add(X, Y)) >= add(F X, map(F, Y)) 
  filter(F, nil) >= nil 
  filter(F, add(X, Y)) >= filter2(F X, F, X, Y) 
  filter2(true, F, X, Y) >= add(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]] = _|_ 
  [[filter(x_1, x_2)]] = x_2 
  [[filter2(x_1, x_2, x_3, x_4)]] = filter2(x_3, x_4) 
  [[high(x_1, x_2)]] = x_2 
  [[if!fac6220high(x_1, x_2, x_3)]] = x_3 
  [[if!fac6220low(x_1, x_2, x_3)]] = if!fac6220low(x_3) 
  [[low(x_1, x_2)]] = low(x_2) 
  [[minus(x_1, x_2)]] = x_1 
  [[nil]] = _|_ 
  [[s(x_1)]] = x_1 

We choose Lex = {} and Mul = {@_{o -> o}, add, app, false, filter2, if!fac6220low, le, low, map, map#, quicksort, quot, true}, and the following precedence: map > quicksort > le > app > add = filter2 = if!fac6220low = low > true > false > @_{o -> o} = map# > quot

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

  map#(F, add(X, Y)) > @_{o -> o}(F, X) 
  map#(F, add(X, Y)) >= map#(F, Y) 
  X >= X 
  X >= X 
  quot(_|_, X) >= _|_ 
  quot(X, Y) >= quot(X, Y) 
  le(_|_, X) >= true 
  le(X, _|_) >= false 
  le(X, Y) >= le(X, Y) 
  app(_|_, X) >= X 
  app(add(X, Y), Z) >= add(X, app(Y, Z)) 
  low(_|_) >= _|_ 
  low(add(X, Y)) >= if!fac6220low(add(X, Y)) 
  if!fac6220low(add(X, Y)) >= add(X, low(Y)) 
  if!fac6220low(add(X, Y)) >= low(Y) 
  _|_ >= _|_ 
  add(X, Y) >= add(X, Y) 
  add(X, Y) >= Y 
  add(X, Y) >= add(X, Y) 
  quicksort(_|_) >= _|_ 
  quicksort(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(Y))) 
  map(F, _|_) >= _|_ 
  map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) 
  _|_ >= _|_ 
  add(X, Y) >= filter2(X, Y) 
  filter2(X, Y) >= add(X, Y) 
  filter2(X, Y) >= Y 

With these choices, we have:

  1] map#(F, add(X, Y)) > @_{o -> o}(F, X)  because [2], by definition 
  2] map#*(F, add(X, Y)) >= @_{o -> o}(F, X)  because map# = @_{o -> o}, map# in Mul, [3] and [4], by (Stat) 
  3] F >= F  by (Meta) 
  4] add(X, Y) > X  because [5], by definition 
  5] add*(X, Y) >= X  because [6], by (Select) 
  6] X >= X  by (Meta) 

  7] map#(F, add(X, Y)) >= map#(F, Y)  because map# in Mul, [3] and [8], by (Fun) 
  8] add(X, Y) >= Y  because [9], by (Star) 
  9] add*(X, Y) >= Y  because [10], by (Select) 
  10] Y >= Y  by (Meta) 

  11] X >= X  by (Meta) 

  12] X >= X  by (Meta) 

  13] quot(_|_, X) >= _|_  by (Bot) 

  14] quot(X, Y) >= quot(X, Y)  because quot in Mul, [15] and [16], by (Fun) 
  15] X >= X  by (Meta) 
  16] Y >= Y  by (Meta) 

  17] le(_|_, X) >= true  because [18], by (Star) 
  18] le*(_|_, X) >= true  because le > true, by (Copy) 

  19] le(X, _|_) >= false  because [20], by (Star) 
  20] le*(X, _|_) >= false  because le > false, by (Copy) 

  21] le(X, Y) >= le(X, Y)  because le in Mul, [22] and [23], by (Fun) 
  22] X >= X  by (Meta) 
  23] Y >= Y  by (Meta) 

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

  27] app(add(X, Y), Z) >= add(X, app(Y, Z))  because [28], by (Star) 
  28] app*(add(X, Y), Z) >= add(X, app(Y, Z))  because app > add, [29] and [33], by (Copy) 
  29] app*(add(X, Y), Z) >= X  because [30], by (Select) 
  30] add(X, Y) >= X  because [31], by (Star) 
  31] add*(X, Y) >= X  because [32], by (Select) 
  32] X >= X  by (Meta) 
  33] app*(add(X, Y), Z) >= app(Y, Z)  because app in Mul, [34] and [37], by (Stat) 
  34] add(X, Y) > Y  because [35], by definition 
  35] add*(X, Y) >= Y  because [36], by (Select) 
  36] Y >= Y  by (Meta) 
  37] Z >= Z  by (Meta) 

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

  39] low(add(X, Y)) >= if!fac6220low(add(X, Y))  because low = if!fac6220low, low in Mul and [40], by (Fun) 
  40] add(X, Y) >= add(X, Y)  because add in Mul, [41] and [42], by (Fun) 
  41] X >= X  by (Meta) 
  42] Y >= Y  by (Meta) 

  43] if!fac6220low(add(X, Y)) >= add(X, low(Y))  because [44], by (Star) 
  44] if!fac6220low*(add(X, Y)) >= add(X, low(Y))  because if!fac6220low = add, if!fac6220low in Mul, [45] and [48], by (Stat) 
  45] add(X, Y) > X  because [46], by definition 
  46] add*(X, Y) >= X  because [47], by (Select) 
  47] X >= X  by (Meta) 
  48] add(X, Y) > low(Y)  because [49], by definition 
  49] add*(X, Y) >= low(Y)  because add = low, add in Mul and [50], by (Stat) 
  50] Y >= Y  by (Meta) 

  51] if!fac6220low(add(X, Y)) >= low(Y)  because [52], by (Star) 
  52] if!fac6220low*(add(X, Y)) >= low(Y)  because if!fac6220low = low, if!fac6220low in Mul and [53], by (Stat) 
  53] add(X, Y) > Y  because [54], by definition 
  54] add*(X, Y) >= Y  because [55], by (Select) 
  55] Y >= Y  by (Meta) 

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

  57] add(X, Y) >= add(X, Y)  because add in Mul, [58] and [59], by (Fun) 
  58] X >= X  by (Meta) 
  59] Y >= Y  by (Meta) 

  60] add(X, Y) >= Y  because [61], by (Star) 
  61] add*(X, Y) >= Y  because [62], by (Select) 
  62] Y >= Y  by (Meta) 

  63] add(X, Y) >= add(X, Y)  because add in Mul, [64] and [65], by (Fun) 
  64] X >= X  by (Meta) 
  65] Y >= Y  by (Meta) 

  66] quicksort(_|_) >= _|_  by (Bot) 

  67] quicksort(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(Y)))  because [68], by (Star) 
  68] quicksort*(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(Y)))  because quicksort > app, [69] and [73], by (Copy) 
  69] quicksort*(add(X, Y)) >= quicksort(low(Y))  because quicksort in Mul and [70], by (Stat) 
  70] add(X, Y) > low(Y)  because [71], by definition 
  71] add*(X, Y) >= low(Y)  because add = low, add in Mul and [72], by (Stat) 
  72] Y >= Y  by (Meta) 
  73] quicksort*(add(X, Y)) >= add(X, quicksort(Y))  because quicksort > add, [74] and [78], by (Copy) 
  74] quicksort*(add(X, Y)) >= X  because [75], by (Select) 
  75] add(X, Y) >= X  because [76], by (Star) 
  76] add*(X, Y) >= X  because [77], by (Select) 
  77] X >= X  by (Meta) 
  78] quicksort*(add(X, Y)) >= quicksort(Y)  because quicksort in Mul and [79], by (Stat) 
  79] add(X, Y) > Y  because [80], by definition 
  80] add*(X, Y) >= Y  because [72], by (Select) 

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

  82] map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y))  because [83], by (Star) 
  83] map*(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y))  because map > add, [84] and [88], by (Copy) 
  84] map*(F, add(X, Y)) >= @_{o -> o}(F, X)  because map > @_{o -> o}, [85] and [86], by (Copy) 
  85] map*(F, add(X, Y)) >= F  because [3], by (Select) 
  86] map*(F, add(X, Y)) >= X  because [87], by (Select) 
  87] add(X, Y) >= X  because [5], by (Star) 
  88] map*(F, add(X, Y)) >= map(F, Y)  because map in Mul, [3] and [89], by (Stat) 
  89] add(X, Y) > Y  because [90], by definition 
  90] add*(X, Y) >= Y  because [10], by (Select) 

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

  92] add(X, Y) >= filter2(X, Y)  because add = filter2, add in Mul, [93] and [94], by (Fun) 
  93] X >= X  by (Meta) 
  94] Y >= Y  by (Meta) 

  95] filter2(X, Y) >= add(X, Y)  because filter2 = add, filter2 in Mul, [96] and [97], by (Fun) 
  96] X >= X  by (Meta) 
  97] Y >= Y  by (Meta) 

  98] filter2(X, Y) >= Y  because [99], by (Star) 
  99] filter2*(X, Y) >= Y  because [100], by (Select) 
  100] 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_10, R_0, minimal, formative) by (P_13, R_0, minimal, formative), where P_13 consists of:

  map#(F, add(X, Y)) =#> map#(F, Y)   

Thus, the original system is terminating if each of (P_1, R_0, minimal, formative), (P_2, R_0, minimal, formative), (P_3, R_0, minimal, formative), (P_4, R_0, minimal, formative), (P_5, R_0, minimal, formative), (P_6, R_0, minimal, formative), (P_7, R_0, minimal, formative) and (P_13, R_0, minimal, formative) is finite.

We consider the dependency pair problem (P_13, R_0, minimal, formative).

We apply the subterm criterion with the following projection function:

  nu(map#) = 2 

Thus, we can orient the dependency pairs as follows:

  nu(map#(F, add(X, Y))) = add(X, Y) |> Y = nu(map#(F, Y)) 

By [Kop12, Thm. 7.35], we may replace a dependency pair problem (P_13, R_0, minimal, f) by ({}, R_0, minimal, f).  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, minimal, formative), (P_2, R_0, minimal, formative), (P_3, R_0, minimal, formative), (P_4, R_0, minimal, formative), (P_5, R_0, minimal, formative), (P_6, R_0, minimal, formative) and (P_7, R_0, minimal, formative) is finite.

We consider the dependency pair problem (P_7, R_0, minimal, formative).

We will use the reduction pair processor with usable rules [Kop12, Thm. 7.44].  The usable rules of (P_7, R_0) are:

  le(0, X) => true 
  le(s(X), 0) => false 
  le(s(X), s(Y)) => le(X, Y) 
  low(X, nil) => nil 
  low(X, add(Y, Z)) => if!fac6220low(le(Y, X), X, add(Y, Z)) 
  if!fac6220low(true, X, add(Y, Z)) => add(Y, low(X, Z)) 
  if!fac6220low(false, X, add(Y, Z)) => low(X, Z) 
  high(X, nil) => nil 
  high(X, add(Y, Z)) => if!fac6220high(le(Y, X), X, add(Y, Z)) 
  if!fac6220high(true, X, add(Y, Z)) => high(X, Z) 
  if!fac6220high(false, X, add(Y, Z)) => add(Y, high(X, Z)) 

It suffices to find a standard reduction pair [Kop12, Def. 6.69].  Thus, we must orient:

  quicksort#(add(X, Y)) >? quicksort#(low(X, Y)) 
  quicksort#(add(X, Y)) >? quicksort#(high(X, Y)) 
  le(0, X) >= true 
  le(s(X), 0) >= false 
  le(s(X), s(Y)) >= le(X, Y) 
  low(X, nil) >= nil 
  low(X, add(Y, Z)) >= if!fac6220low(le(Y, X), X, add(Y, Z)) 
  if!fac6220low(true, X, add(Y, Z)) >= add(Y, low(X, Z)) 
  if!fac6220low(false, X, add(Y, Z)) >= low(X, Z) 
  high(X, nil) >= nil 
  high(X, add(Y, Z)) >= if!fac6220high(le(Y, X), X, add(Y, Z)) 
  if!fac6220high(true, X, add(Y, Z)) >= high(X, Z) 
  if!fac6220high(false, X, add(Y, Z)) >= add(Y, high(X, Z)) 

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

The following interpretation satisfies the requirements:

  0 = 3 
  add = \y0y1.1 + y1 
  false = 0 
  high = \y0y1.y1 
  if!fac6220high = \y0y1y2.y2 
  if!fac6220low = \y0y1y2.y2 
  le = \y0y1.0 
  low = \y0y1.y1 
  nil = 0 
  quicksort# = \y0.y0 
  s = \y0.3 
  true = 0 

Using this interpretation, the requirements translate to:

  [[quicksort#(add(_x0, _x1))]] = 1 + x1 > x1 = [[quicksort#(low(_x0, _x1))]] 
  [[quicksort#(add(_x0, _x1))]] = 1 + x1 > x1 = [[quicksort#(high(_x0, _x1))]] 
  [[le(0, _x0)]] = 0 >= 0 = [[true]] 
  [[le(s(_x0), 0)]] = 0 >= 0 = [[false]] 
  [[le(s(_x0), s(_x1))]] = 0 >= 0 = [[le(_x0, _x1)]] 
  [[low(_x0, nil)]] = 0 >= 0 = [[nil]] 
  [[low(_x0, add(_x1, _x2))]] = 1 + x2 >= 1 + x2 = [[if!fac6220low(le(_x1, _x0), _x0, add(_x1, _x2))]] 
  [[if!fac6220low(true, _x0, add(_x1, _x2))]] = 1 + x2 >= 1 + x2 = [[add(_x1, low(_x0, _x2))]] 
  [[if!fac6220low(false, _x0, add(_x1, _x2))]] = 1 + x2 >= x2 = [[low(_x0, _x2)]] 
  [[high(_x0, nil)]] = 0 >= 0 = [[nil]] 
  [[high(_x0, add(_x1, _x2))]] = 1 + x2 >= 1 + x2 = [[if!fac6220high(le(_x1, _x0), _x0, add(_x1, _x2))]] 
  [[if!fac6220high(true, _x0, add(_x1, _x2))]] = 1 + x2 >= x2 = [[high(_x0, _x2)]] 
  [[if!fac6220high(false, _x0, add(_x1, _x2))]] = 1 + x2 >= 1 + x2 = [[add(_x1, high(_x0, _x2))]] 

By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_7, 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, minimal, formative), (P_2, R_0, minimal, formative), (P_3, R_0, minimal, formative), (P_4, R_0, minimal, formative), (P_5, R_0, minimal, formative) and (P_6, R_0, minimal, formative) is finite.

We consider the dependency pair problem (P_6, R_0, minimal, formative).

We apply the subterm criterion with the following projection function:

  nu(high#) = 2 
  nu(if!fac6220high#) = 3 

Thus, we can orient the dependency pairs as follows:

  nu(high#(X, add(Y, Z))) = add(Y, Z) = add(Y, Z) = nu(if!fac6220high#(le(Y, X), X, add(Y, Z))) 
  nu(if!fac6220high#(true, X, add(Y, Z))) = add(Y, Z) |> Z = nu(high#(X, Z)) 
  nu(if!fac6220high#(false, X, add(Y, Z))) = add(Y, Z) |> Z = nu(high#(X, Z)) 

By [Kop12, Thm. 7.35], we may replace a dependency pair problem (P_6, R_0, minimal, f) by (P_14, R_0, minimal, f), where P_14 contains:

  high#(X, add(Y, Z)) =#> if!fac6220high#(le(Y, X), X, add(Y, Z))   

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

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

This graph has no strongly connected components.  By [Kop12, Thm. 7.31], this implies finiteness of the dependency pair problem.

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

We consider the dependency pair problem (P_5, R_0, minimal, formative).

We apply the subterm criterion with the following projection function:

  nu(if!fac6220low#) = 3 
  nu(low#) = 2 

Thus, we can orient the dependency pairs as follows:

  nu(low#(X, add(Y, Z))) = add(Y, Z) = add(Y, Z) = nu(if!fac6220low#(le(Y, X), X, add(Y, Z))) 
  nu(if!fac6220low#(true, X, add(Y, Z))) = add(Y, Z) |> Z = nu(low#(X, Z)) 
  nu(if!fac6220low#(false, X, add(Y, Z))) = add(Y, Z) |> Z = nu(low#(X, Z)) 

By [Kop12, Thm. 7.35], we may replace a dependency pair problem (P_5, R_0, minimal, f) by (P_15, R_0, minimal, f), where P_15 contains:

  low#(X, add(Y, Z)) =#> if!fac6220low#(le(Y, X), X, add(Y, Z))   

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

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

This graph has no strongly connected components.  By [Kop12, Thm. 7.31], this implies finiteness of the dependency pair problem.

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

We consider the dependency pair problem (P_4, R_0, minimal, formative).

We apply the subterm criterion with the following projection function:

  nu(app#) = 1 

Thus, we can orient the dependency pairs as follows:

  nu(app#(add(X, Y), Z)) = add(X, Y) |> Y = nu(app#(Y, Z)) 

By [Kop12, Thm. 7.35], we may replace a dependency pair problem (P_4, R_0, minimal, f) by ({}, R_0, minimal, f).  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, minimal, formative), (P_2, R_0, minimal, formative) and (P_3, R_0, minimal, formative) is finite.

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

We apply the subterm criterion with the following projection function:

  nu(le#) = 1 

Thus, we can orient the dependency pairs as follows:

  nu(le#(s(X), s(Y))) = s(X) |> X = nu(le#(X, Y)) 

By [Kop12, Thm. 7.35], we may replace a dependency pair problem (P_3, R_0, minimal, f) by ({}, R_0, minimal, f).  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, minimal, formative) and (P_2, R_0, minimal, formative) is finite.

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

The formative rules of (P_2, R_0) are R_1 ::=

  minus(X, 0) => X 
  minus(s(X), s(Y)) => minus(X, Y) 
  quot(0, s(X)) => 0 
  quot(s(X), s(Y)) => s(quot(minus(X, Y), s(Y))) 

By [Kop12, Thm. 7.17], we may replace the dependency pair problem (P_2, R_0, minimal, formative) by (P_2, R_1, minimal, formative).

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

We consider the dependency pair problem (P_2, R_1, minimal, formative).

We will use the reduction pair processor with usable rules [Kop12, Thm. 7.44].  The usable rules of (P_2, R_1) are:

  minus(X, 0) => X 
  minus(s(X), s(Y)) => minus(X, Y) 

It suffices to find a standard reduction pair [Kop12, Def. 6.69].  Thus, we must orient:

  quot#(s(X), s(Y)) >? quot#(minus(X, Y), s(Y)) 
  minus(X, 0) >= X 
  minus(s(X), s(Y)) >= minus(X, Y) 

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

The following interpretation satisfies the requirements:

  0 = 0 
  minus = \y0y1.y0 
  quot# = \y0y1.3y0 
  s = \y0.3 + 3y0 

Using this interpretation, the requirements translate to:

  [[quot#(s(_x0), s(_x1))]] = 9 + 9x0 > 3x0 = [[quot#(minus(_x0, _x1), s(_x1))]] 
  [[minus(_x0, 0)]] = x0 >= x0 = [[_x0]] 
  [[minus(s(_x0), s(_x1))]] = 3 + 3x0 >= x0 = [[minus(_x0, _x1)]] 

By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_2, R_1) by ({}, R_1).  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, minimal, formative) is finite.

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

We apply the subterm criterion with the following projection function:

  nu(minus#) = 1 

Thus, we can orient the dependency pairs as follows:

  nu(minus#(s(X), s(Y))) = s(X) |> X = nu(minus#(X, Y)) 

By [Kop12, Thm. 7.35], we may replace a dependency pair problem (P_1, R_0, minimal, f) by ({}, R_0, minimal, f).  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.