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 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] 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)) =#> map#(F, Y) 19] filter#(F, add(X, Y)) =#> filter2#(F X, F, X, Y) 20] filter2#(true, F, X, Y) =#> filter#(F, Y) 21] 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, 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 * 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 : 18 * 19 : 20, 21 * 20 : 19 * 21 : 19 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)) =#> map#(F, Y) P_9: 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_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), (P_8, R_0, m, f) and (P_9, 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), (P_5, R_0, static, formative), (P_6, R_0, static, formative), (P_7, R_0, static, formative), (P_8, R_0, static, formative) and (P_9, R_0, static, formative) is finite. We consider the dependency pair problem (P_9, R_0, static, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: 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) 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]] = _|_ [[filter2(x_1, x_2, x_3, x_4)]] = filter2(x_2, x_3, x_4) [[filter2#(x_1, x_2, x_3, x_4)]] = filter2#(x_4, x_2, x_1) [[filter#(x_1, x_2)]] = filter#(x_2, x_1) [[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]] = _|_ [[true]] = _|_ We choose Lex = {app, filter2#, filter#} and Mul = {@_{o -> o}, add, false, filter, filter2, if!fac6220low, le, low, map, quicksort, quot, s}, and the following precedence: filter = filter2 > filter2# = filter# > le > false > map > @_{o -> o} > quicksort > app > add = if!fac6220low = low > quot > s Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: filter#(F, add(X, Y)) > filter2#(@_{o -> o}(F, X), F, X, Y) filter2#(_|_, F, X, Y) >= filter#(F, Y) filter2#(false, F, X, Y) >= filter#(F, Y) X >= X s(X) >= X quot(_|_, s(X)) >= _|_ quot(s(X), s(Y)) >= s(quot(X, s(Y))) le(_|_, X) >= _|_ le(s(X), _|_) >= false le(s(X), s(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)) filter(F, _|_) >= _|_ filter(F, add(X, Y)) >= filter2(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] filter#(F, add(X, Y)) > filter2#(@_{o -> o}(F, X), F, X, Y) because [2], by definition 2] filter#*(F, add(X, Y)) >= filter2#(@_{o -> o}(F, X), F, X, Y) because filter# = filter2#, [3], [6], [7] and [13], by (Stat) 3] add(X, Y) > Y because [4], by definition 4] add*(X, Y) >= Y because [5], by (Select) 5] Y >= Y by (Meta) 6] filter#*(F, add(X, Y)) >= @_{o -> o}(F, X) because filter# > @_{o -> o}, [7] and [9], by (Copy) 7] filter#*(F, add(X, Y)) >= F because [8], by (Select) 8] F >= F by (Meta) 9] filter#*(F, add(X, Y)) >= X because [10], by (Select) 10] add(X, Y) >= X because [11], by (Star) 11] add*(X, Y) >= X because [12], by (Select) 12] X >= X by (Meta) 13] filter#*(F, add(X, Y)) >= Y because [14], by (Select) 14] add(X, Y) >= Y because [4], by (Star) 15] filter2#(_|_, F, X, Y) >= filter#(F, Y) because [16], by (Star) 16] filter2#*(_|_, F, X, Y) >= filter#(F, Y) because filter2# = filter#, [17], [18], [19] and [20], by (Stat) 17] F >= F by (Meta) 18] Y >= Y by (Meta) 19] filter2#*(_|_, F, X, Y) >= F because [17], by (Select) 20] filter2#*(_|_, F, X, Y) >= Y because [18], by (Select) 21] filter2#(false, F, X, Y) >= filter#(F, Y) because [22], by (Star) 22] filter2#*(false, F, X, Y) >= filter#(F, Y) because filter2# = filter#, [23], [24], [25] and [26], by (Stat) 23] F >= F by (Meta) 24] Y >= Y by (Meta) 25] filter2#*(false, F, X, Y) >= F because [23], by (Select) 26] filter2#*(false, F, X, Y) >= Y because [24], by (Select) 27] X >= X by (Meta) 28] s(X) >= X because [29], by (Star) 29] s*(X) >= X because [30], by (Select) 30] X >= X by (Meta) 31] quot(_|_, s(X)) >= _|_ by (Bot) 32] quot(s(X), s(Y)) >= s(quot(X, s(Y))) because [33], by (Star) 33] quot*(s(X), s(Y)) >= s(quot(X, s(Y))) because quot > s and [34], by (Copy) 34] quot*(s(X), s(Y)) >= quot(X, s(Y)) because quot in Mul, [35] and [38], by (Stat) 35] s(X) > X because [36], by definition 36] s*(X) >= X because [37], by (Select) 37] X >= X by (Meta) 38] s(Y) >= s(Y) because s in Mul and [39], by (Fun) 39] Y >= Y by (Meta) 40] le(_|_, X) >= _|_ by (Bot) 41] le(s(X), _|_) >= false because [42], by (Star) 42] le*(s(X), _|_) >= false because le > false, by (Copy) 43] le(s(X), s(Y)) >= le(X, Y) because [44], by (Star) 44] le*(s(X), s(Y)) >= le(X, Y) because le in Mul, [45] and [48], by (Stat) 45] s(X) >= X because [46], by (Star) 46] s*(X) >= X because [47], by (Select) 47] X >= X by (Meta) 48] s(Y) > Y because [49], by definition 49] s*(Y) >= Y because [50], by (Select) 50] Y >= Y by (Meta) 51] app(_|_, X) >= X because [52], by (Star) 52] app*(_|_, X) >= X because [53], by (Select) 53] X >= X by (Meta) 54] app(add(X, Y), Z) >= add(X, app(Y, Z)) because [55], by (Star) 55] app*(add(X, Y), Z) >= add(X, app(Y, Z)) because app > add, [56] and [60], by (Copy) 56] app*(add(X, Y), Z) >= X because [57], by (Select) 57] add(X, Y) >= X because [58], by (Star) 58] add*(X, Y) >= X because [59], by (Select) 59] X >= X by (Meta) 60] app*(add(X, Y), Z) >= app(Y, Z) because [61], [64] and [66], by (Stat) 61] add(X, Y) > Y because [62], by definition 62] add*(X, Y) >= Y because [63], by (Select) 63] Y >= Y by (Meta) 64] app*(add(X, Y), Z) >= Y because [65], by (Select) 65] add(X, Y) >= Y because [62], by (Star) 66] app*(add(X, Y), Z) >= Z because [67], by (Select) 67] Z >= Z by (Meta) 68] low(_|_) >= _|_ by (Bot) 69] low(add(X, Y)) >= if!fac6220low(add(X, Y)) because low = if!fac6220low, low in Mul and [70], by (Fun) 70] add(X, Y) >= add(X, Y) because add in Mul, [71] and [72], by (Fun) 71] X >= X by (Meta) 72] Y >= Y by (Meta) 73] if!fac6220low(add(X, Y)) >= add(X, low(Y)) because [74], by (Star) 74] if!fac6220low*(add(X, Y)) >= add(X, low(Y)) because if!fac6220low = add, if!fac6220low in Mul, [75] and [78], by (Stat) 75] add(X, Y) > X because [76], by definition 76] add*(X, Y) >= X because [77], by (Select) 77] X >= X by (Meta) 78] add(X, Y) > low(Y) because [79], by definition 79] add*(X, Y) >= low(Y) because add = low, add in Mul and [80], by (Stat) 80] Y >= Y by (Meta) 81] if!fac6220low(add(X, Y)) >= low(Y) because if!fac6220low = low, if!fac6220low in Mul and [82], by (Fun) 82] add(X, Y) >= Y because [83], by (Star) 83] add*(X, Y) >= Y because [84], by (Select) 84] Y >= Y by (Meta) 85] _|_ >= _|_ by (Bot) 86] add(X, Y) >= add(X, Y) because add in Mul, [87] and [88], by (Fun) 87] X >= X by (Meta) 88] Y >= Y by (Meta) 89] add(X, Y) >= Y because [90], by (Star) 90] add*(X, Y) >= Y because [91], by (Select) 91] Y >= Y by (Meta) 92] add(X, Y) >= add(X, Y) because add in Mul, [93] and [94], by (Fun) 93] X >= X by (Meta) 94] Y >= Y by (Meta) 95] quicksort(_|_) >= _|_ by (Bot) 96] quicksort(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(Y))) because [97], by (Star) 97] quicksort*(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(Y))) because quicksort > app, [98] and [102], by (Copy) 98] quicksort*(add(X, Y)) >= quicksort(low(Y)) because quicksort in Mul and [99], by (Stat) 99] add(X, Y) > low(Y) because [100], by definition 100] add*(X, Y) >= low(Y) because add = low, add in Mul and [101], by (Stat) 101] Y >= Y by (Meta) 102] quicksort*(add(X, Y)) >= add(X, quicksort(Y)) because quicksort > add, [103] and [107], by (Copy) 103] quicksort*(add(X, Y)) >= X because [104], by (Select) 104] add(X, Y) >= X because [105], by (Star) 105] add*(X, Y) >= X because [106], by (Select) 106] X >= X by (Meta) 107] quicksort*(add(X, Y)) >= quicksort(Y) because quicksort in Mul and [108], by (Stat) 108] add(X, Y) > Y because [109], by definition 109] add*(X, Y) >= Y because [101], by (Select) 110] map(F, _|_) >= _|_ by (Bot) 111] map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because [112], by (Star) 112] map*(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because map > add, [113] and [120], by (Copy) 113] map*(F, add(X, Y)) >= @_{o -> o}(F, X) because map > @_{o -> o}, [114] and [116], by (Copy) 114] map*(F, add(X, Y)) >= F because [115], by (Select) 115] F >= F by (Meta) 116] map*(F, add(X, Y)) >= X because [117], by (Select) 117] add(X, Y) >= X because [118], by (Star) 118] add*(X, Y) >= X because [119], by (Select) 119] X >= X by (Meta) 120] map*(F, add(X, Y)) >= map(F, Y) because map in Mul, [121] and [122], by (Stat) 121] F >= F by (Meta) 122] add(X, Y) > Y because [123], by definition 123] add*(X, Y) >= Y because [124], by (Select) 124] Y >= Y by (Meta) 125] filter(F, _|_) >= _|_ by (Bot) 126] filter(F, add(X, Y)) >= filter2(F, X, Y) because [127], by (Star) 127] filter*(F, add(X, Y)) >= filter2(F, X, Y) because filter = filter2, filter in Mul, [128], [129] and [3], by (Stat) 128] F >= F by (Meta) 129] add(X, Y) > X because [130], by definition 130] add*(X, Y) >= X because [12], by (Select) 131] filter2(F, X, Y) >= add(X, filter(F, Y)) because [132], by (Star) 132] filter2*(F, X, Y) >= add(X, filter(F, Y)) because filter2 > add, [133] and [135], by (Copy) 133] filter2*(F, X, Y) >= X because [134], by (Select) 134] X >= X by (Meta) 135] filter2*(F, X, Y) >= filter(F, Y) because filter2 = filter, filter2 in Mul, [17] and [18], by (Stat) 136] filter2(F, X, Y) >= filter(F, Y) because [137], by (Star) 137] filter2*(F, X, Y) >= filter(F, Y) because filter2 = filter, filter2 in Mul, [23] and [24], by (Stat) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_9, R_0, static, formative) by (P_10, R_0, static, formative), where P_10 consists of: 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, static, formative), (P_2, R_0, static, formative), (P_3, R_0, static, formative), (P_4, R_0, static, formative), (P_5, R_0, static, formative), (P_6, R_0, static, formative), (P_7, R_0, static, formative), (P_8, R_0, static, formative) and (P_10, R_0, static, formative) is finite. We consider the dependency pair problem (P_10, 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 : * 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, static, formative), (P_2, R_0, static, formative), (P_3, R_0, static, formative), (P_4, R_0, static, formative), (P_5, R_0, static, formative), (P_6, R_0, static, formative), (P_7, R_0, static, formative) and (P_8, R_0, static, formative) is finite. We consider the dependency pair problem (P_8, R_0, static, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: 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]] = _|_ [[false]] = _|_ [[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)]] = high(x_2) [[if!fac6220high(x_1, x_2, x_3)]] = if!fac6220high(x_3) [[if!fac6220low(x_1, x_2, x_3)]] = x_3 [[low(x_1, x_2)]] = x_2 [[minus(x_1, x_2)]] = minus(x_1) [[nil]] = _|_ [[true]] = _|_ We choose Lex = {} and Mul = {@_{o -> o}, add, app, filter2, high, if!fac6220high, le, map, map#, minus, quicksort, quot, s}, and the following precedence: map > @_{o -> o} > quicksort > app > quot > s > minus > le > add = filter2 = high = if!fac6220high > map# 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)) > map#(F, Y) minus(X) >= X minus(s(X)) >= minus(X) quot(_|_, s(X)) >= _|_ quot(s(X), s(Y)) >= s(quot(minus(X), s(Y))) le(_|_, X) >= _|_ le(s(X), _|_) >= _|_ le(s(X), s(Y)) >= le(X, Y) app(_|_, X) >= X app(add(X, Y), Z) >= add(X, app(Y, Z)) _|_ >= _|_ add(X, Y) >= add(X, Y) add(X, Y) >= add(X, Y) add(X, Y) >= 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(Y), add(X, quicksort(high(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)) > map#(F, Y) because [2], by definition 2] map#*(F, add(X, Y)) >= map#(F, Y) because map# in Mul, [3] and [4], by (Stat) 3] F >= F by (Meta) 4] add(X, Y) > Y because [5], by definition 5] add*(X, Y) >= Y because [6], by (Select) 6] Y >= Y by (Meta) 7] minus(X) >= X because [8], by (Star) 8] minus*(X) >= X because [9], by (Select) 9] X >= X by (Meta) 10] minus(s(X)) >= minus(X) because [11], by (Star) 11] minus*(s(X)) >= minus(X) because minus in Mul and [12], by (Stat) 12] s(X) > X because [13], by definition 13] s*(X) >= X because [14], by (Select) 14] X >= X by (Meta) 15] quot(_|_, s(X)) >= _|_ by (Bot) 16] quot(s(X), s(Y)) >= s(quot(minus(X), s(Y))) because [17], by (Star) 17] quot*(s(X), s(Y)) >= s(quot(minus(X), s(Y))) because quot > s and [18], by (Copy) 18] quot*(s(X), s(Y)) >= quot(minus(X), s(Y)) because quot in Mul, [19] and [23], by (Stat) 19] s(X) > minus(X) because [20], by definition 20] s*(X) >= minus(X) because s > minus and [21], by (Copy) 21] s*(X) >= X because [22], by (Select) 22] X >= X by (Meta) 23] s(Y) >= s(Y) because s in Mul and [24], by (Fun) 24] Y >= Y by (Meta) 25] le(_|_, X) >= _|_ by (Bot) 26] le(s(X), _|_) >= _|_ by (Bot) 27] le(s(X), s(Y)) >= le(X, Y) because [28], by (Star) 28] le*(s(X), s(Y)) >= le(X, Y) because le in Mul, [29] and [32], by (Stat) 29] s(X) >= X because [30], by (Star) 30] s*(X) >= X because [31], by (Select) 31] X >= X by (Meta) 32] s(Y) > Y because [33], by definition 33] s*(Y) >= Y because [34], by (Select) 34] Y >= Y by (Meta) 35] app(_|_, X) >= X because [36], by (Star) 36] app*(_|_, X) >= X because [37], by (Select) 37] X >= X by (Meta) 38] app(add(X, Y), Z) >= add(X, app(Y, Z)) because [39], by (Star) 39] app*(add(X, Y), Z) >= add(X, app(Y, Z)) because app > add, [40] and [44], by (Copy) 40] app*(add(X, Y), Z) >= X because [41], by (Select) 41] add(X, Y) >= X because [42], by (Star) 42] add*(X, Y) >= X because [43], by (Select) 43] X >= X by (Meta) 44] app*(add(X, Y), Z) >= app(Y, Z) because app in Mul, [45] and [48], by (Stat) 45] add(X, Y) > Y because [46], by definition 46] add*(X, Y) >= Y because [47], by (Select) 47] Y >= Y by (Meta) 48] Z >= Z by (Meta) 49] _|_ >= _|_ by (Bot) 50] add(X, Y) >= add(X, Y) because add in Mul, [51] and [52], by (Fun) 51] X >= X by (Meta) 52] Y >= Y by (Meta) 53] add(X, Y) >= add(X, Y) because add in Mul, [54] and [55], by (Fun) 54] X >= X by (Meta) 55] Y >= Y by (Meta) 56] add(X, Y) >= Y because [57], by (Star) 57] add*(X, Y) >= Y because [58], by (Select) 58] Y >= Y by (Meta) 59] high(_|_) >= _|_ by (Bot) 60] high(add(X, Y)) >= if!fac6220high(add(X, Y)) because high = if!fac6220high, high in Mul and [61], by (Fun) 61] add(X, Y) >= add(X, Y) because add in Mul, [62] and [63], by (Fun) 62] X >= X by (Meta) 63] Y >= Y by (Meta) 64] if!fac6220high(add(X, Y)) >= high(Y) because [65], by (Star) 65] if!fac6220high*(add(X, Y)) >= high(Y) because if!fac6220high = high, if!fac6220high in Mul and [66], by (Stat) 66] add(X, Y) > Y because [67], by definition 67] add*(X, Y) >= Y because [68], by (Select) 68] Y >= Y by (Meta) 69] if!fac6220high(add(X, Y)) >= add(X, high(Y)) because [70], by (Star) 70] if!fac6220high*(add(X, Y)) >= add(X, high(Y)) because if!fac6220high = add, if!fac6220high in Mul, [71] and [74], by (Stat) 71] add(X, Y) > X because [72], by definition 72] add*(X, Y) >= X because [73], by (Select) 73] X >= X by (Meta) 74] add(X, Y) > high(Y) because [75], by definition 75] add*(X, Y) >= high(Y) because add = high, add in Mul and [76], by (Stat) 76] Y >= Y by (Meta) 77] quicksort(_|_) >= _|_ by (Bot) 78] quicksort(add(X, Y)) >= app(quicksort(Y), add(X, quicksort(high(Y)))) because [79], by (Star) 79] quicksort*(add(X, Y)) >= app(quicksort(Y), add(X, quicksort(high(Y)))) because quicksort > app, [80] and [84], by (Copy) 80] quicksort*(add(X, Y)) >= quicksort(Y) because quicksort in Mul and [81], by (Stat) 81] add(X, Y) > Y because [82], by definition 82] add*(X, Y) >= Y because [83], by (Select) 83] Y >= Y by (Meta) 84] quicksort*(add(X, Y)) >= add(X, quicksort(high(Y))) because quicksort > add, [85] and [89], by (Copy) 85] quicksort*(add(X, Y)) >= X because [86], by (Select) 86] add(X, Y) >= X because [87], by (Star) 87] add*(X, Y) >= X because [88], by (Select) 88] X >= X by (Meta) 89] quicksort*(add(X, Y)) >= quicksort(high(Y)) because quicksort in Mul and [90], by (Stat) 90] add(X, Y) > high(Y) because [91], by definition 91] add*(X, Y) >= high(Y) because add = high, add in Mul and [92], by (Stat) 92] Y >= Y by (Meta) 93] map(F, _|_) >= _|_ by (Bot) 94] map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because [95], by (Star) 95] map*(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because map > add, [96] and [102], by (Copy) 96] map*(F, add(X, Y)) >= @_{o -> o}(F, X) because map > @_{o -> o}, [97] and [98], by (Copy) 97] map*(F, add(X, Y)) >= F because [3], by (Select) 98] map*(F, add(X, Y)) >= X because [99], by (Select) 99] add(X, Y) >= X because [100], by (Star) 100] add*(X, Y) >= X because [101], by (Select) 101] X >= X by (Meta) 102] map*(F, add(X, Y)) >= map(F, Y) because map in Mul, [3] and [4], by (Stat) 103] _|_ >= _|_ by (Bot) 104] add(X, Y) >= filter2(X, Y) because add = filter2, add in Mul, [105] and [106], by (Fun) 105] X >= X by (Meta) 106] Y >= Y by (Meta) 107] filter2(X, Y) >= add(X, Y) because filter2 = add, filter2 in Mul, [108] and [109], by (Fun) 108] X >= X by (Meta) 109] Y >= Y by (Meta) 110] filter2(X, Y) >= Y because [111], by (Star) 111] filter2*(X, Y) >= Y because [112], by (Select) 112] 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_8, 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), (P_4, R_0, static, formative), (P_5, R_0, static, formative), (P_6, R_0, static, formative) and (P_7, R_0, static, formative) is finite. We consider the dependency pair problem (P_7, R_0, static, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: quicksort#(add(X, Y)) >? quicksort#(low(X, Y)) quicksort#(add(X, Y)) >? quicksort#(high(X, 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]] = _|_ [[@_{o -> o}(x_1, x_2)]] = @_{o -> o}(x_2, x_1) [[false]] = _|_ [[filter(x_1, x_2)]] = filter(x_2, x_1) [[filter2(x_1, x_2, x_3, x_4)]] = filter2(x_4, x_2, x_3, x_1) [[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)]] = x_3 [[low(x_1, x_2)]] = x_2 [[minus(x_1, x_2)]] = minus(x_1) [[nil]] = _|_ [[true]] = _|_ We choose Lex = {@_{o -> o}, filter, filter2} and Mul = {add, app, high, if!fac6220high, le, map, minus, quicksort, quicksort#, quot, s}, and the following precedence: le > map > quicksort > app > quicksort# > quot > s > @_{o -> o} = filter = filter2 > add = high = if!fac6220high > minus Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: quicksort#(add(X, Y)) >= quicksort#(Y) quicksort#(add(X, Y)) > quicksort#(high(Y)) minus(X) >= X minus(s(X)) >= minus(X) quot(_|_, s(X)) >= _|_ quot(s(X), s(Y)) >= s(quot(minus(X), s(Y))) le(_|_, X) >= _|_ le(s(X), _|_) >= _|_ le(s(X), s(Y)) >= le(X, Y) app(_|_, X) >= X app(add(X, Y), Z) >= add(X, app(Y, Z)) _|_ >= _|_ add(X, Y) >= add(X, Y) add(X, Y) >= add(X, Y) add(X, Y) >= 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(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] quicksort#(add(X, Y)) >= quicksort#(Y) because [2], by (Star) 2] quicksort#*(add(X, Y)) >= quicksort#(Y) because quicksort# in Mul and [3], by (Stat) 3] add(X, Y) > Y because [4], by definition 4] add*(X, Y) >= Y because [5], by (Select) 5] Y >= Y by (Meta) 6] quicksort#(add(X, Y)) > quicksort#(high(Y)) because [7], by definition 7] quicksort#*(add(X, Y)) >= quicksort#(high(Y)) because quicksort# in Mul and [8], by (Stat) 8] add(X, Y) > high(Y) because [9], by definition 9] add*(X, Y) >= high(Y) because add = high, add in Mul and [10], by (Stat) 10] Y >= Y by (Meta) 11] minus(X) >= X because [12], by (Star) 12] minus*(X) >= X because [13], by (Select) 13] X >= X by (Meta) 14] minus(s(X)) >= minus(X) because [15], by (Star) 15] minus*(s(X)) >= minus(X) because minus in Mul and [16], by (Stat) 16] s(X) > X because [17], by definition 17] s*(X) >= X because [18], by (Select) 18] X >= X by (Meta) 19] quot(_|_, s(X)) >= _|_ by (Bot) 20] quot(s(X), s(Y)) >= s(quot(minus(X), s(Y))) because [21], by (Star) 21] quot*(s(X), s(Y)) >= s(quot(minus(X), s(Y))) because quot > s and [22], by (Copy) 22] quot*(s(X), s(Y)) >= quot(minus(X), s(Y)) because quot in Mul, [23] and [27], by (Stat) 23] s(X) > minus(X) because [24], by definition 24] s*(X) >= minus(X) because s > minus and [25], by (Copy) 25] s*(X) >= X because [26], by (Select) 26] X >= X by (Meta) 27] s(Y) >= s(Y) because s in Mul and [28], by (Fun) 28] Y >= Y by (Meta) 29] le(_|_, X) >= _|_ by (Bot) 30] le(s(X), _|_) >= _|_ by (Bot) 31] le(s(X), s(Y)) >= le(X, Y) because le in Mul, [32] and [35], by (Fun) 32] s(X) >= X because [33], by (Star) 33] s*(X) >= X because [34], by (Select) 34] X >= X by (Meta) 35] s(Y) >= Y because [36], by (Star) 36] s*(Y) >= Y because [37], by (Select) 37] Y >= Y by (Meta) 38] app(_|_, X) >= X because [39], by (Star) 39] app*(_|_, X) >= X because [40], by (Select) 40] X >= X by (Meta) 41] app(add(X, Y), Z) >= add(X, app(Y, Z)) because [42], by (Star) 42] app*(add(X, Y), Z) >= add(X, app(Y, Z)) because app > add, [43] and [47], by (Copy) 43] app*(add(X, Y), Z) >= X because [44], by (Select) 44] add(X, Y) >= X because [45], by (Star) 45] add*(X, Y) >= X because [46], by (Select) 46] X >= X by (Meta) 47] app*(add(X, Y), Z) >= app(Y, Z) because app in Mul, [48] and [51], by (Stat) 48] add(X, Y) > Y because [49], by definition 49] add*(X, Y) >= Y because [50], by (Select) 50] Y >= Y by (Meta) 51] Z >= Z by (Meta) 52] _|_ >= _|_ by (Bot) 53] add(X, Y) >= add(X, Y) because add in Mul, [54] and [55], by (Fun) 54] X >= X by (Meta) 55] Y >= Y by (Meta) 56] add(X, Y) >= add(X, Y) because add in Mul, [57] and [58], by (Fun) 57] X >= X by (Meta) 58] Y >= Y by (Meta) 59] add(X, Y) >= Y because [60], by (Star) 60] add*(X, Y) >= Y because [61], by (Select) 61] Y >= Y by (Meta) 62] high(_|_) >= _|_ by (Bot) 63] high(add(X, Y)) >= if!fac6220high(add(X, Y)) because high = if!fac6220high, high in Mul and [64], by (Fun) 64] add(X, Y) >= add(X, Y) because add in Mul, [65] and [66], by (Fun) 65] X >= X by (Meta) 66] Y >= Y by (Meta) 67] if!fac6220high(add(X, Y)) >= high(Y) because [68], by (Star) 68] if!fac6220high*(add(X, Y)) >= high(Y) because if!fac6220high = high, if!fac6220high in Mul and [69], by (Stat) 69] add(X, Y) > Y because [70], by definition 70] add*(X, Y) >= Y because [71], by (Select) 71] Y >= Y by (Meta) 72] if!fac6220high(add(X, Y)) >= add(X, high(Y)) because [73], by (Star) 73] if!fac6220high*(add(X, Y)) >= add(X, high(Y)) because if!fac6220high = add, if!fac6220high in Mul, [74] and [77], by (Stat) 74] add(X, Y) > X because [75], by definition 75] add*(X, Y) >= X because [76], by (Select) 76] X >= X by (Meta) 77] add(X, Y) > high(Y) because [78], by definition 78] add*(X, Y) >= high(Y) because add = high, add in Mul and [79], by (Stat) 79] Y >= Y by (Meta) 80] quicksort(_|_) >= _|_ by (Bot) 81] quicksort(add(X, Y)) >= app(quicksort(Y), add(X, quicksort(high(Y)))) because [82], by (Star) 82] quicksort*(add(X, Y)) >= app(quicksort(Y), add(X, quicksort(high(Y)))) because quicksort > app, [83] and [84], by (Copy) 83] quicksort*(add(X, Y)) >= quicksort(Y) because quicksort in Mul and [3], by (Stat) 84] quicksort*(add(X, Y)) >= add(X, quicksort(high(Y))) because quicksort > add, [85] and [89], by (Copy) 85] quicksort*(add(X, Y)) >= X because [86], by (Select) 86] add(X, Y) >= X because [87], by (Star) 87] add*(X, Y) >= X because [88], by (Select) 88] X >= X by (Meta) 89] quicksort*(add(X, Y)) >= quicksort(high(Y)) because quicksort in Mul and [8], by (Stat) 90] map(F, _|_) >= _|_ by (Bot) 91] map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because [92], by (Star) 92] map*(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because map > add, [93] and [100], by (Copy) 93] map*(F, add(X, Y)) >= @_{o -> o}(F, X) because map > @_{o -> o}, [94] and [96], by (Copy) 94] map*(F, add(X, Y)) >= F because [95], by (Select) 95] F >= F by (Meta) 96] map*(F, add(X, Y)) >= X because [97], by (Select) 97] add(X, Y) >= X because [98], by (Star) 98] add*(X, Y) >= X because [99], by (Select) 99] X >= X by (Meta) 100] map*(F, add(X, Y)) >= map(F, Y) because map in Mul, [101] and [102], by (Stat) 101] F >= F by (Meta) 102] add(X, Y) > Y because [103], by definition 103] add*(X, Y) >= Y because [104], by (Select) 104] Y >= Y by (Meta) 105] filter(F, _|_) >= _|_ by (Bot) 106] filter(F, add(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because [107], by (Star) 107] filter*(F, add(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because filter = filter2, [108], [111], [115], [117] and [119], by (Stat) 108] add(X, Y) > Y because [109], by definition 109] add*(X, Y) >= Y because [110], by (Select) 110] Y >= Y by (Meta) 111] filter*(F, add(X, Y)) >= @_{o -> o}(F, X) because filter = @_{o -> o}, [112], [115] and [117], by (Stat) 112] add(X, Y) > X because [113], by definition 113] add*(X, Y) >= X because [114], by (Select) 114] X >= X by (Meta) 115] filter*(F, add(X, Y)) >= F because [116], by (Select) 116] F >= F by (Meta) 117] filter*(F, add(X, Y)) >= X because [118], by (Select) 118] add(X, Y) >= X because [113], by (Star) 119] filter*(F, add(X, Y)) >= Y because [120], by (Select) 120] add(X, Y) >= Y because [109], by (Star) 121] filter2(_|_, F, X, Y) >= add(X, filter(F, Y)) because [122], by (Star) 122] filter2*(_|_, F, X, Y) >= add(X, filter(F, Y)) because filter2 > add, [123] and [125], by (Copy) 123] filter2*(_|_, F, X, Y) >= X because [124], by (Select) 124] X >= X by (Meta) 125] filter2*(_|_, F, X, Y) >= filter(F, Y) because filter2 = filter, [126], [127], [128] and [129], by (Stat) 126] F >= F by (Meta) 127] Y >= Y by (Meta) 128] filter2*(_|_, F, X, Y) >= F because [126], by (Select) 129] filter2*(_|_, F, X, Y) >= Y because [127], by (Select) 130] filter2(_|_, F, X, Y) >= filter(F, Y) because [131], by (Star) 131] filter2*(_|_, F, X, Y) >= filter(F, Y) because filter2 = filter, [132], [133], [134] and [135], by (Stat) 132] F >= F by (Meta) 133] Y >= Y by (Meta) 134] filter2*(_|_, F, X, Y) >= F because [132], by (Select) 135] filter2*(_|_, F, X, Y) >= Y because [133], by (Select) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_7, R_0, static, formative) by (P_11, R_0, static, formative), where P_11 consists of: quicksort#(add(X, Y)) =#> quicksort#(low(X, 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), (P_5, R_0, static, formative), (P_6, R_0, static, formative) and (P_11, R_0, static, formative) is finite. We consider the dependency pair problem (P_11, 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: quicksort#(add(X, Y)) >? quicksort#(low(X, 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]] = _|_ [[filter(x_1, x_2)]] = filter(x_2, x_1) [[filter2(x_1, x_2, x_3, x_4)]] = filter2(x_4, x_2, x_3, x_1) [[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) [[le(x_1, x_2)]] = _|_ [[low(x_1, x_2)]] = low(x_2) [[minus(x_1, x_2)]] = x_1 [[nil]] = _|_ [[quot(x_1, x_2)]] = quot(x_1) [[true]] = _|_ We choose Lex = {filter, filter2} and Mul = {@_{o -> o}, add, app, if!fac6220low, low, map, quicksort, quicksort#, quot, s}, and the following precedence: filter = filter2 > map > @_{o -> o} > quicksort > app > quot = s > add = if!fac6220low = low > quicksort# Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: quicksort#(add(X, Y)) > quicksort#(low(Y)) X >= X s(X) >= X quot(_|_) >= _|_ quot(s(X)) >= s(quot(X)) _|_ >= _|_ _|_ >= _|_ _|_ >= _|_ 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)) 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] quicksort#(add(X, Y)) > quicksort#(low(Y)) because [2], by definition 2] quicksort#*(add(X, Y)) >= quicksort#(low(Y)) because [3], by (Select) 3] add(X, Y) >= quicksort#(low(Y)) because [4], by (Star) 4] add*(X, Y) >= quicksort#(low(Y)) because add > quicksort# and [5], by (Copy) 5] add*(X, Y) >= low(Y) because add = low, add in Mul and [6], by (Stat) 6] Y >= Y by (Meta) 7] X >= X by (Meta) 8] s(X) >= X because [9], by (Star) 9] s*(X) >= X because [10], by (Select) 10] X >= X by (Meta) 11] quot(_|_) >= _|_ by (Bot) 12] quot(s(X)) >= s(quot(X)) because quot = s, quot in Mul and [13], by (Fun) 13] s(X) >= quot(X) because s = quot, s in Mul and [14], by (Fun) 14] X >= X by (Meta) 15] _|_ >= _|_ by (Bot) 16] _|_ >= _|_ by (Bot) 17] _|_ >= _|_ by (Bot) 18] app(_|_, X) >= X because [19], by (Star) 19] app*(_|_, X) >= X because [20], by (Select) 20] X >= X by (Meta) 21] app(add(X, Y), Z) >= add(X, app(Y, Z)) because [22], by (Star) 22] app*(add(X, Y), Z) >= add(X, app(Y, Z)) because app > add, [23] and [27], by (Copy) 23] app*(add(X, Y), Z) >= X because [24], by (Select) 24] add(X, Y) >= X because [25], by (Star) 25] add*(X, Y) >= X because [26], by (Select) 26] X >= X by (Meta) 27] app*(add(X, Y), Z) >= app(Y, Z) because app in Mul, [28] and [31], by (Stat) 28] add(X, Y) > Y because [29], by definition 29] add*(X, Y) >= Y because [30], by (Select) 30] Y >= Y by (Meta) 31] Z >= Z by (Meta) 32] low(_|_) >= _|_ by (Bot) 33] low(add(X, Y)) >= if!fac6220low(add(X, Y)) because low = if!fac6220low, low in Mul and [34], by (Fun) 34] add(X, Y) >= add(X, Y) because add in Mul, [35] and [36], by (Fun) 35] X >= X by (Meta) 36] Y >= Y by (Meta) 37] if!fac6220low(add(X, Y)) >= add(X, low(Y)) because [38], by (Star) 38] if!fac6220low*(add(X, Y)) >= add(X, low(Y)) because if!fac6220low = add, if!fac6220low in Mul, [39] and [42], by (Stat) 39] add(X, Y) > X because [40], by definition 40] add*(X, Y) >= X because [41], by (Select) 41] X >= X by (Meta) 42] add(X, Y) > low(Y) because [43], by definition 43] add*(X, Y) >= low(Y) because add = low, add in Mul and [44], by (Stat) 44] Y >= Y by (Meta) 45] if!fac6220low(add(X, Y)) >= low(Y) because [46], by (Star) 46] if!fac6220low*(add(X, Y)) >= low(Y) because if!fac6220low = low, if!fac6220low in Mul and [47], by (Stat) 47] add(X, Y) > Y because [48], by definition 48] add*(X, Y) >= Y because [49], by (Select) 49] Y >= Y by (Meta) 50] _|_ >= _|_ by (Bot) 51] add(X, Y) >= add(X, Y) because add in Mul, [52] and [53], by (Fun) 52] X >= X by (Meta) 53] Y >= Y by (Meta) 54] add(X, Y) >= Y because [55], by (Star) 55] add*(X, Y) >= Y because [56], by (Select) 56] Y >= Y by (Meta) 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] quicksort(_|_) >= _|_ by (Bot) 61] quicksort(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(Y))) because [62], by (Star) 62] quicksort*(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(Y))) because quicksort > app, [63] and [65], by (Copy) 63] quicksort*(add(X, Y)) >= quicksort(low(Y)) because quicksort in Mul and [64], by (Stat) 64] add(X, Y) > low(Y) because [5], by definition 65] quicksort*(add(X, Y)) >= add(X, quicksort(Y)) because quicksort > add, [66] and [70], by (Copy) 66] quicksort*(add(X, Y)) >= X because [67], by (Select) 67] add(X, Y) >= X because [68], by (Star) 68] add*(X, Y) >= X because [69], by (Select) 69] X >= X by (Meta) 70] quicksort*(add(X, Y)) >= quicksort(Y) because quicksort in Mul and [71], by (Stat) 71] add(X, Y) > Y because [72], by definition 72] add*(X, Y) >= Y because [6], by (Select) 73] map(F, _|_) >= _|_ by (Bot) 74] map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because [75], by (Star) 75] map*(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because map > add, [76] and [83], by (Copy) 76] map*(F, add(X, Y)) >= @_{o -> o}(F, X) because map > @_{o -> o}, [77] and [79], by (Copy) 77] map*(F, add(X, Y)) >= F because [78], by (Select) 78] F >= F by (Meta) 79] map*(F, add(X, Y)) >= X because [80], by (Select) 80] add(X, Y) >= X because [81], by (Star) 81] add*(X, Y) >= X because [82], by (Select) 82] X >= X by (Meta) 83] map*(F, add(X, Y)) >= map(F, Y) because map in Mul, [84] and [85], by (Stat) 84] F >= F by (Meta) 85] add(X, Y) > Y because [86], by definition 86] add*(X, Y) >= Y because [87], by (Select) 87] Y >= Y by (Meta) 88] filter(F, _|_) >= _|_ by (Bot) 89] filter(F, add(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because [90], by (Star) 90] filter*(F, add(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because filter = filter2, [91], [94], [95], [97] and [101], by (Stat) 91] add(X, Y) > Y because [92], by definition 92] add*(X, Y) >= Y because [93], by (Select) 93] Y >= Y by (Meta) 94] filter*(F, add(X, Y)) >= @_{o -> o}(F, X) because filter > @_{o -> o}, [95] and [97], by (Copy) 95] filter*(F, add(X, Y)) >= F because [96], by (Select) 96] F >= F by (Meta) 97] filter*(F, add(X, Y)) >= X because [98], by (Select) 98] add(X, Y) >= X because [99], by (Star) 99] add*(X, Y) >= X because [100], by (Select) 100] X >= X by (Meta) 101] filter*(F, add(X, Y)) >= Y because [102], by (Select) 102] add(X, Y) >= Y because [92], by (Star) 103] filter2(_|_, F, X, Y) >= add(X, filter(F, Y)) because [104], by (Star) 104] filter2*(_|_, F, X, Y) >= add(X, filter(F, Y)) because filter2 > add, [105] and [107], by (Copy) 105] filter2*(_|_, F, X, Y) >= X because [106], by (Select) 106] X >= X by (Meta) 107] filter2*(_|_, F, X, Y) >= filter(F, Y) because filter2 = filter, [108], [109], [110] and [111], by (Stat) 108] F >= F by (Meta) 109] Y >= Y by (Meta) 110] filter2*(_|_, F, X, Y) >= F because [108], by (Select) 111] filter2*(_|_, F, X, Y) >= Y because [109], by (Select) 112] filter2(_|_, F, X, Y) >= filter(F, Y) because [113], by (Star) 113] filter2*(_|_, F, X, Y) >= filter(F, Y) because filter2 = filter, [114], [115], [116] and [117], by (Stat) 114] F >= F by (Meta) 115] Y >= Y by (Meta) 116] filter2*(_|_, F, X, Y) >= F because [114], by (Select) 117] filter2*(_|_, F, X, Y) >= Y because [115], by (Select) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_11, 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), (P_4, R_0, static, formative), (P_5, 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: 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) 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]] = _|_ [[filter(x_1, x_2)]] = filter(x_2) [[filter2(x_1, x_2, x_3, x_4)]] = filter2(x_3, x_4) [[high(x_1, x_2)]] = high(x_2) [[if!fac6220high(x_1, x_2, x_3)]] = if!fac6220high(x_3) [[if!fac6220high#(x_1, x_2, x_3)]] = if!fac6220high#(x_2, x_3) [[if!fac6220low(x_1, x_2, x_3)]] = x_3 [[low(x_1, x_2)]] = x_2 [[minus(x_1, x_2)]] = x_1 [[nil]] = _|_ [[quot(x_1, x_2)]] = quot(x_1) [[true]] = _|_ We choose Lex = {} and Mul = {@_{o -> o}, add, app, filter, filter2, high, high#, if!fac6220high, if!fac6220high#, le, map, quicksort, quot, s}, and the following precedence: filter = filter2 > map > @_{o -> o} > quicksort > app > add = high = if!fac6220high > le > high# = if!fac6220high# > quot = s Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: high#(X, add(Y, Z)) >= if!fac6220high#(X, add(Y, Z)) if!fac6220high#(X, add(Y, Z)) >= high#(X, Z) if!fac6220high#(X, add(Y, Z)) > high#(X, Z) X >= X s(X) >= X quot(_|_) >= _|_ quot(s(X)) >= s(quot(X)) le(_|_, X) >= _|_ le(s(X), _|_) >= _|_ le(s(X), s(Y)) >= le(X, Y) app(_|_, X) >= X app(add(X, Y), Z) >= add(X, app(Y, Z)) _|_ >= _|_ add(X, Y) >= add(X, Y) add(X, Y) >= add(X, Y) add(X, Y) >= 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(Y), add(X, quicksort(high(Y)))) map(F, _|_) >= _|_ map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) filter(_|_) >= _|_ filter(add(X, Y)) >= filter2(X, Y) filter2(X, Y) >= add(X, filter(Y)) filter2(X, Y) >= filter(Y) With these choices, we have: 1] high#(X, add(Y, Z)) >= if!fac6220high#(X, add(Y, Z)) because high# = if!fac6220high#, high# in Mul, [2] and [3], by (Fun) 2] X >= X by (Meta) 3] add(Y, Z) >= add(Y, Z) because add in Mul, [4] and [5], by (Fun) 4] Y >= Y by (Meta) 5] Z >= Z by (Meta) 6] if!fac6220high#(X, add(Y, Z)) >= high#(X, Z) because [7], by (Star) 7] if!fac6220high#*(X, add(Y, Z)) >= high#(X, Z) because if!fac6220high# = high#, if!fac6220high# in Mul, [8] and [9], by (Stat) 8] X >= X by (Meta) 9] add(Y, Z) > Z because [10], by definition 10] add*(Y, Z) >= Z because [11], by (Select) 11] Z >= Z by (Meta) 12] if!fac6220high#(X, add(Y, Z)) > high#(X, Z) because [13], by definition 13] if!fac6220high#*(X, add(Y, Z)) >= high#(X, Z) because if!fac6220high# = high#, if!fac6220high# in Mul, [14] and [15], by (Stat) 14] X >= X by (Meta) 15] add(Y, Z) > Z because [16], by definition 16] add*(Y, Z) >= Z because [17], by (Select) 17] Z >= Z by (Meta) 18] X >= X by (Meta) 19] s(X) >= X because [20], by (Star) 20] s*(X) >= X because [21], by (Select) 21] X >= X by (Meta) 22] quot(_|_) >= _|_ by (Bot) 23] quot(s(X)) >= s(quot(X)) because quot = s, quot in Mul and [24], by (Fun) 24] s(X) >= quot(X) because s = quot, s in Mul and [25], by (Fun) 25] X >= X by (Meta) 26] le(_|_, X) >= _|_ by (Bot) 27] le(s(X), _|_) >= _|_ by (Bot) 28] le(s(X), s(Y)) >= le(X, Y) because le in Mul, [29] and [32], by (Fun) 29] s(X) >= X because [30], by (Star) 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] app(_|_, X) >= X because [36], by (Star) 36] app*(_|_, X) >= X because [37], by (Select) 37] X >= X by (Meta) 38] app(add(X, Y), Z) >= add(X, app(Y, Z)) because [39], by (Star) 39] app*(add(X, Y), Z) >= add(X, app(Y, Z)) because app > add, [40] and [44], by (Copy) 40] app*(add(X, Y), Z) >= X because [41], by (Select) 41] add(X, Y) >= X because [42], by (Star) 42] add*(X, Y) >= X because [43], by (Select) 43] X >= X by (Meta) 44] app*(add(X, Y), Z) >= app(Y, Z) because app in Mul, [45] and [48], by (Stat) 45] add(X, Y) > Y because [46], by definition 46] add*(X, Y) >= Y because [47], by (Select) 47] Y >= Y by (Meta) 48] Z >= Z by (Meta) 49] _|_ >= _|_ by (Bot) 50] add(X, Y) >= add(X, Y) because add in Mul, [51] and [52], by (Fun) 51] X >= X by (Meta) 52] Y >= Y by (Meta) 53] add(X, Y) >= add(X, Y) because add in Mul, [54] and [55], by (Fun) 54] X >= X by (Meta) 55] Y >= Y by (Meta) 56] add(X, Y) >= Y because [57], by (Star) 57] add*(X, Y) >= Y because [58], by (Select) 58] Y >= Y by (Meta) 59] high(_|_) >= _|_ by (Bot) 60] high(add(X, Y)) >= if!fac6220high(add(X, Y)) because high = if!fac6220high, high in Mul and [3], by (Fun) 61] if!fac6220high(add(X, Y)) >= high(Y) because if!fac6220high = high, if!fac6220high in Mul and [62], by (Fun) 62] add(X, Y) >= Y because [10], by (Star) 63] if!fac6220high(add(X, Y)) >= add(X, high(Y)) because [64], by (Star) 64] if!fac6220high*(add(X, Y)) >= add(X, high(Y)) because if!fac6220high = add, if!fac6220high in Mul, [65] and [68], by (Stat) 65] add(X, Y) > X because [66], by definition 66] add*(X, Y) >= X because [67], by (Select) 67] X >= X by (Meta) 68] add(X, Y) > high(Y) because [69], by definition 69] add*(X, Y) >= high(Y) because add = high, add in Mul and [70], by (Stat) 70] Y >= Y by (Meta) 71] quicksort(_|_) >= _|_ by (Bot) 72] quicksort(add(X, Y)) >= app(quicksort(Y), add(X, quicksort(high(Y)))) because [73], by (Star) 73] quicksort*(add(X, Y)) >= app(quicksort(Y), add(X, quicksort(high(Y)))) because quicksort > app, [74] and [78], by (Copy) 74] quicksort*(add(X, Y)) >= quicksort(Y) because quicksort in Mul and [75], by (Stat) 75] add(X, Y) > Y because [76], by definition 76] add*(X, Y) >= Y because [77], by (Select) 77] Y >= Y by (Meta) 78] quicksort*(add(X, Y)) >= add(X, quicksort(high(Y))) because quicksort > add, [79] and [83], by (Copy) 79] quicksort*(add(X, Y)) >= X because [80], by (Select) 80] add(X, Y) >= X because [81], by (Star) 81] add*(X, Y) >= X because [82], by (Select) 82] X >= X by (Meta) 83] quicksort*(add(X, Y)) >= quicksort(high(Y)) because quicksort in Mul and [84], by (Stat) 84] add(X, Y) > high(Y) because [85], by definition 85] add*(X, Y) >= high(Y) because add = high, add in Mul and [86], by (Stat) 86] Y >= Y by (Meta) 87] map(F, _|_) >= _|_ by (Bot) 88] map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because [89], by (Star) 89] map*(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because map > add, [90] and [97], by (Copy) 90] map*(F, add(X, Y)) >= @_{o -> o}(F, X) because map > @_{o -> o}, [91] and [93], by (Copy) 91] map*(F, add(X, Y)) >= F because [92], by (Select) 92] F >= F by (Meta) 93] map*(F, add(X, Y)) >= X because [94], by (Select) 94] add(X, Y) >= X because [95], by (Star) 95] add*(X, Y) >= X because [96], by (Select) 96] X >= X by (Meta) 97] map*(F, add(X, Y)) >= map(F, Y) because map in Mul, [98] and [99], by (Stat) 98] F >= F by (Meta) 99] add(X, Y) > Y because [100], by definition 100] add*(X, Y) >= Y because [101], by (Select) 101] Y >= Y by (Meta) 102] filter(_|_) >= _|_ by (Bot) 103] filter(add(X, Y)) >= filter2(X, Y) because [104], by (Star) 104] filter*(add(X, Y)) >= filter2(X, Y) because filter = filter2, filter in Mul, [105] and [108], by (Stat) 105] add(X, Y) > X because [106], by definition 106] add*(X, Y) >= X because [107], by (Select) 107] X >= X by (Meta) 108] add(X, Y) > Y because [109], by definition 109] add*(X, Y) >= Y because [110], by (Select) 110] Y >= Y by (Meta) 111] filter2(X, Y) >= add(X, filter(Y)) because [112], by (Star) 112] filter2*(X, Y) >= add(X, filter(Y)) because filter2 > add, [113] and [115], by (Copy) 113] filter2*(X, Y) >= X because [114], by (Select) 114] X >= X by (Meta) 115] filter2*(X, Y) >= filter(Y) because filter2 = filter, filter2 in Mul and [116], by (Stat) 116] Y >= Y by (Meta) 117] filter2(X, Y) >= filter(Y) because [118], by (Star) 118] filter2*(X, Y) >= filter(Y) because filter2 = filter, filter2 in Mul and [119], by (Stat) 119] 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_6, R_0, static, formative) by (P_12, R_0, static, formative), where P_12 consists of: high#(X, add(Y, Z)) =#> if!fac6220high#(le(Y, X), X, add(Y, Z)) if!fac6220high#(true, X, add(Y, Z)) =#> high#(X, Z) 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), (P_5, R_0, static, formative) and (P_12, R_0, static, formative) is finite. We consider the dependency pair problem (P_12, 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: high#(X, add(Y, Z)) >? if!fac6220high#(le(Y, X), X, add(Y, Z)) if!fac6220high#(true, X, add(Y, Z)) >? high#(X, Z) 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]] = _|_ [[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)]] = high(x_2) [[high#(x_1, x_2)]] = high#(x_2) [[if!fac6220high(x_1, x_2, x_3)]] = if!fac6220high(x_3) [[if!fac6220high#(x_1, x_2, x_3)]] = if!fac6220high#(x_1, x_3) [[if!fac6220low(x_1, x_2, x_3)]] = if!fac6220low(x_3) [[le(x_1, x_2)]] = le [[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 = {} and Mul = {@_{o -> o}, add, app, filter2, high, high#, if!fac6220high, if!fac6220high#, if!fac6220low, le, low, map, quicksort, quot}, and the following precedence: map > quicksort > app > add = filter2 = high = if!fac6220high = if!fac6220low = low > high# > if!fac6220high# > le > @_{o -> o} > quot Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: high#(add(X, Y)) >= if!fac6220high#(le, add(X, Y)) if!fac6220high#(_|_, add(X, Y)) > high#(Y) X >= X X >= X quot(_|_, X) >= _|_ quot(X, Y) >= quot(X, Y) le >= _|_ le >= _|_ le >= le 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)) _|_ >= _|_ add(X, Y) >= filter2(X, Y) filter2(X, Y) >= add(X, Y) filter2(X, Y) >= Y With these choices, we have: 1] high#(add(X, Y)) >= if!fac6220high#(le, add(X, Y)) because [2], by (Star) 2] high#*(add(X, Y)) >= if!fac6220high#(le, add(X, Y)) because high# > if!fac6220high#, [3] and [4], by (Copy) 3] high#*(add(X, Y)) >= le because high# > le, by (Copy) 4] high#*(add(X, Y)) >= add(X, Y) because [5], by (Select) 5] add(X, Y) >= add(X, Y) because add in Mul, [6] and [7], by (Fun) 6] X >= X by (Meta) 7] Y >= Y by (Meta) 8] if!fac6220high#(_|_, add(X, Y)) > high#(Y) because [9], by definition 9] if!fac6220high#*(_|_, add(X, Y)) >= high#(Y) because [10], by (Select) 10] add(X, Y) >= high#(Y) because [11], by (Star) 11] add*(X, Y) >= high#(Y) because add > high# and [12], by (Copy) 12] add*(X, Y) >= Y because [13], by (Select) 13] Y >= Y by (Meta) 14] X >= X by (Meta) 15] X >= X by (Meta) 16] quot(_|_, X) >= _|_ by (Bot) 17] quot(X, Y) >= quot(X, Y) because quot in Mul, [18] and [19], by (Fun) 18] X >= X by (Meta) 19] Y >= Y by (Meta) 20] le >= _|_ by (Bot) 21] le >= _|_ by (Bot) 22] le >= le because le in Mul, by (Fun) 23] app(_|_, X) >= X because [24], by (Star) 24] app*(_|_, X) >= X because [25], by (Select) 25] X >= X by (Meta) 26] app(add(X, Y), Z) >= add(X, app(Y, Z)) because [27], by (Star) 27] app*(add(X, Y), Z) >= add(X, app(Y, Z)) because app > add, [28] and [32], by (Copy) 28] app*(add(X, Y), Z) >= X because [29], by (Select) 29] add(X, Y) >= X because [30], by (Star) 30] add*(X, Y) >= X because [31], by (Select) 31] X >= X by (Meta) 32] app*(add(X, Y), Z) >= app(Y, Z) because app in Mul, [33] and [36], by (Stat) 33] add(X, Y) > Y because [34], by definition 34] add*(X, Y) >= Y because [35], by (Select) 35] Y >= Y by (Meta) 36] Z >= Z by (Meta) 37] low(_|_) >= _|_ by (Bot) 38] low(add(X, Y)) >= if!fac6220low(add(X, Y)) because low = if!fac6220low, low in Mul and [39], by (Fun) 39] add(X, Y) >= add(X, Y) because add in Mul, [40] and [41], by (Fun) 40] X >= X by (Meta) 41] Y >= Y by (Meta) 42] if!fac6220low(add(X, Y)) >= add(X, low(Y)) because [43], by (Star) 43] if!fac6220low*(add(X, Y)) >= add(X, low(Y)) because if!fac6220low = add, if!fac6220low in Mul, [44] and [47], by (Stat) 44] add(X, Y) > X because [45], by definition 45] add*(X, Y) >= X because [46], by (Select) 46] X >= X by (Meta) 47] add(X, Y) > low(Y) because [48], by definition 48] add*(X, Y) >= low(Y) because add = low, add in Mul and [49], by (Stat) 49] Y >= Y by (Meta) 50] if!fac6220low(add(X, Y)) >= low(Y) because [51], by (Star) 51] if!fac6220low*(add(X, Y)) >= low(Y) because if!fac6220low = low, if!fac6220low in Mul and [52], by (Stat) 52] add(X, Y) > Y because [53], by definition 53] add*(X, Y) >= Y because [54], by (Select) 54] Y >= Y by (Meta) 55] high(_|_) >= _|_ by (Bot) 56] high(add(X, Y)) >= if!fac6220high(add(X, Y)) because high = if!fac6220high, high in Mul and [57], by (Fun) 57] add(X, Y) >= add(X, Y) because add in Mul, [6] and [7], by (Fun) 58] if!fac6220high(add(X, Y)) >= high(Y) because [59], by (Star) 59] if!fac6220high*(add(X, Y)) >= high(Y) because [60], by (Select) 60] add(X, Y) >= high(Y) because [61], by (Star) 61] add*(X, Y) >= high(Y) because add = high, add in Mul and [62], by (Stat) 62] Y >= Y by (Meta) 63] if!fac6220high(add(X, Y)) >= add(X, high(Y)) because [64], by (Star) 64] if!fac6220high*(add(X, Y)) >= add(X, high(Y)) because if!fac6220high = add, if!fac6220high in Mul, [65] and [68], by (Stat) 65] add(X, Y) > X because [66], by definition 66] add*(X, Y) >= X because [67], by (Select) 67] X >= X by (Meta) 68] add(X, Y) > high(Y) because [69], by definition 69] add*(X, Y) >= high(Y) because add = high, add in Mul and [70], by (Stat) 70] Y >= Y by (Meta) 71] quicksort(_|_) >= _|_ by (Bot) 72] quicksort(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(high(Y)))) because [73], by (Star) 73] quicksort*(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(high(Y)))) because quicksort > app, [74] and [78], by (Copy) 74] quicksort*(add(X, Y)) >= quicksort(low(Y)) because quicksort in Mul and [75], by (Stat) 75] add(X, Y) > low(Y) because [76], by definition 76] add*(X, Y) >= low(Y) because add = low, add in Mul and [77], by (Stat) 77] Y >= Y by (Meta) 78] quicksort*(add(X, Y)) >= add(X, quicksort(high(Y))) because quicksort > add, [79] and [83], by (Copy) 79] quicksort*(add(X, Y)) >= X because [80], by (Select) 80] add(X, Y) >= X because [81], by (Star) 81] add*(X, Y) >= X because [82], by (Select) 82] X >= X by (Meta) 83] quicksort*(add(X, Y)) >= quicksort(high(Y)) because quicksort in Mul and [84], by (Stat) 84] add(X, Y) > high(Y) because [85], by definition 85] add*(X, Y) >= high(Y) because add = high, add in Mul and [77], by (Stat) 86] map(F, _|_) >= _|_ by (Bot) 87] map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because [88], by (Star) 88] map*(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because map > add, [89] and [96], by (Copy) 89] map*(F, add(X, Y)) >= @_{o -> o}(F, X) because map > @_{o -> o}, [90] and [92], by (Copy) 90] map*(F, add(X, Y)) >= F because [91], by (Select) 91] F >= F by (Meta) 92] map*(F, add(X, Y)) >= X because [93], by (Select) 93] add(X, Y) >= X because [94], by (Star) 94] add*(X, Y) >= X because [95], by (Select) 95] X >= X by (Meta) 96] map*(F, add(X, Y)) >= map(F, Y) because map in Mul, [97] and [98], by (Stat) 97] F >= F by (Meta) 98] add(X, Y) > Y because [99], by definition 99] add*(X, Y) >= Y because [100], by (Select) 100] Y >= Y by (Meta) 101] _|_ >= _|_ by (Bot) 102] add(X, Y) >= filter2(X, Y) because add = filter2, add in Mul, [103] and [104], by (Fun) 103] X >= X by (Meta) 104] Y >= Y by (Meta) 105] filter2(X, Y) >= add(X, Y) because filter2 = add, filter2 in Mul, [106] and [107], by (Fun) 106] X >= X by (Meta) 107] Y >= Y by (Meta) 108] filter2(X, Y) >= Y because [109], by (Star) 109] filter2*(X, Y) >= Y because [110], by (Select) 110] 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_12, R_0, static, formative) by (P_13, R_0, static, formative), where P_13 consists of: 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, static, formative), (P_2, R_0, static, formative), (P_3, R_0, static, formative), (P_4, R_0, static, formative), (P_5, R_0, static, formative) and (P_13, R_0, static, formative) is finite. We consider the dependency pair problem (P_13, 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 : 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, 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: 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) 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) [[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)]] = x_3 [[if!fac6220low#(x_1, x_2, x_3)]] = if!fac6220low#(x_2, x_3) [[le(x_1, x_2)]] = le(x_1) [[low(x_1, x_2)]] = x_2 [[minus(x_1, x_2)]] = x_1 [[nil]] = _|_ [[quot(x_1, x_2)]] = x_1 [[true]] = _|_ We choose Lex = {@_{o -> o}, filter, filter2} and Mul = {add, app, if!fac6220low#, le, low#, map, quicksort, s}, and the following precedence: if!fac6220low# = low# > map > @_{o -> o} = filter = filter2 > quicksort > app > add > le > s Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: low#(X, add(Y, Z)) >= if!fac6220low#(X, add(Y, Z)) if!fac6220low#(X, add(Y, Z)) >= low#(X, Z) if!fac6220low#(X, add(Y, Z)) > low#(X, Z) X >= X s(X) >= X _|_ >= _|_ s(X) >= s(X) le(_|_) >= _|_ le(s(X)) >= _|_ le(s(X)) >= le(X) app(_|_, X) >= X app(add(X, Y), Z) >= add(X, app(Y, Z)) _|_ >= _|_ add(X, Y) >= add(X, Y) add(X, Y) >= add(X, Y) add(X, Y) >= Y _|_ >= _|_ add(X, Y) >= add(X, Y) add(X, Y) >= Y add(X, Y) >= add(X, Y) quicksort(_|_) >= _|_ quicksort(add(X, Y)) >= app(quicksort(Y), add(X, quicksort(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] low#(X, add(Y, Z)) >= if!fac6220low#(X, add(Y, Z)) because low# = if!fac6220low#, low# in Mul, [2] and [3], by (Fun) 2] X >= X by (Meta) 3] add(Y, Z) >= add(Y, Z) because add in Mul, [4] and [5], by (Fun) 4] Y >= Y by (Meta) 5] Z >= Z by (Meta) 6] if!fac6220low#(X, add(Y, Z)) >= low#(X, Z) because if!fac6220low# = low#, if!fac6220low# in Mul, [7] and [8], by (Fun) 7] X >= X by (Meta) 8] add(Y, Z) >= Z because [9], by (Star) 9] add*(Y, Z) >= Z because [10], by (Select) 10] Z >= Z by (Meta) 11] if!fac6220low#(X, add(Y, Z)) > low#(X, Z) because [12], by definition 12] if!fac6220low#*(X, add(Y, Z)) >= low#(X, Z) because if!fac6220low# = low#, if!fac6220low# in Mul, [13] and [14], by (Stat) 13] X >= X by (Meta) 14] add(Y, Z) > Z because [15], by definition 15] add*(Y, Z) >= Z because [16], by (Select) 16] Z >= Z by (Meta) 17] X >= X by (Meta) 18] s(X) >= X because [19], by (Star) 19] s*(X) >= X because [20], by (Select) 20] X >= X by (Meta) 21] _|_ >= _|_ by (Bot) 22] s(X) >= s(X) because s in Mul and [23], by (Fun) 23] X >= X by (Meta) 24] le(_|_) >= _|_ by (Bot) 25] le(s(X)) >= _|_ by (Bot) 26] le(s(X)) >= le(X) because [27], by (Star) 27] le*(s(X)) >= le(X) because le in Mul and [28], by (Stat) 28] s(X) > X because [29], by definition 29] s*(X) >= X because [30], by (Select) 30] X >= X by (Meta) 31] app(_|_, X) >= X because [32], by (Star) 32] app*(_|_, X) >= X because [33], by (Select) 33] X >= X by (Meta) 34] app(add(X, Y), Z) >= add(X, app(Y, Z)) because [35], by (Star) 35] app*(add(X, Y), Z) >= add(X, app(Y, Z)) because app > add, [36] and [40], by (Copy) 36] app*(add(X, Y), Z) >= X because [37], by (Select) 37] add(X, Y) >= X because [38], by (Star) 38] add*(X, Y) >= X because [39], by (Select) 39] X >= X by (Meta) 40] app*(add(X, Y), Z) >= app(Y, Z) because app in Mul, [41] and [44], by (Stat) 41] add(X, Y) > Y because [42], by definition 42] add*(X, Y) >= Y because [43], by (Select) 43] Y >= Y by (Meta) 44] Z >= Z by (Meta) 45] _|_ >= _|_ by (Bot) 46] add(X, Y) >= add(X, Y) because add in Mul, [4] and [5], by (Fun) 47] add(X, Y) >= add(X, Y) because add in Mul, [48] and [49], by (Fun) 48] X >= X by (Meta) 49] Y >= Y by (Meta) 50] add(X, Y) >= Y because [15], by (Star) 51] _|_ >= _|_ by (Bot) 52] add(X, Y) >= add(X, Y) because add in Mul, [53] and [54], by (Fun) 53] X >= X by (Meta) 54] Y >= Y by (Meta) 55] add(X, Y) >= Y because [56], by (Star) 56] add*(X, Y) >= Y because [57], by (Select) 57] Y >= Y by (Meta) 58] add(X, Y) >= add(X, Y) because add in Mul, [59] and [60], by (Fun) 59] X >= X by (Meta) 60] Y >= Y by (Meta) 61] quicksort(_|_) >= _|_ by (Bot) 62] quicksort(add(X, Y)) >= app(quicksort(Y), add(X, quicksort(Y))) because [63], by (Star) 63] quicksort*(add(X, Y)) >= app(quicksort(Y), add(X, quicksort(Y))) because quicksort > app, [64] and [68], by (Copy) 64] quicksort*(add(X, Y)) >= quicksort(Y) because quicksort in Mul and [65], by (Stat) 65] add(X, Y) > Y because [66], by definition 66] add*(X, Y) >= Y because [67], by (Select) 67] Y >= Y by (Meta) 68] quicksort*(add(X, Y)) >= add(X, quicksort(Y)) because quicksort > add, [69] and [73], by (Copy) 69] quicksort*(add(X, Y)) >= X because [70], by (Select) 70] add(X, Y) >= X because [71], by (Star) 71] add*(X, Y) >= X because [72], by (Select) 72] X >= X by (Meta) 73] quicksort*(add(X, Y)) >= quicksort(Y) because quicksort in Mul and [74], by (Stat) 74] add(X, Y) > Y because [75], by definition 75] add*(X, Y) >= Y because [67], by (Select) 76] map(F, _|_) >= _|_ by (Bot) 77] map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because [78], by (Star) 78] map*(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because map > add, [79] and [86], by (Copy) 79] map*(F, add(X, Y)) >= @_{o -> o}(F, X) because map > @_{o -> o}, [80] and [82], by (Copy) 80] map*(F, add(X, Y)) >= F because [81], by (Select) 81] F >= F by (Meta) 82] map*(F, add(X, Y)) >= X because [83], by (Select) 83] add(X, Y) >= X because [84], by (Star) 84] add*(X, Y) >= X because [85], by (Select) 85] X >= X by (Meta) 86] map*(F, add(X, Y)) >= map(F, Y) because map in Mul, [87] and [88], by (Stat) 87] F >= F by (Meta) 88] add(X, Y) > Y because [89], by definition 89] add*(X, Y) >= Y because [90], by (Select) 90] Y >= Y by (Meta) 91] filter(F, _|_) >= _|_ by (Bot) 92] filter(F, add(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because [93], by (Star) 93] filter*(F, add(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because filter = filter2, [94], [95], [98], [102], [103] and [105], by (Stat) 94] F >= F by (Meta) 95] add(X, Y) > Y because [96], by definition 96] add*(X, Y) >= Y because [97], by (Select) 97] Y >= Y by (Meta) 98] filter*(F, add(X, Y)) >= @_{o -> o}(F, X) because filter = @_{o -> o}, [94], [99], [102] and [103], by (Stat) 99] add(X, Y) > X because [100], by definition 100] add*(X, Y) >= X because [101], by (Select) 101] X >= X by (Meta) 102] filter*(F, add(X, Y)) >= F because [94], by (Select) 103] filter*(F, add(X, Y)) >= X because [104], by (Select) 104] add(X, Y) >= X because [100], by (Star) 105] filter*(F, add(X, Y)) >= Y because [106], by (Select) 106] add(X, Y) >= Y because [96], by (Star) 107] filter2(_|_, F, X, Y) >= add(X, filter(F, Y)) because [108], by (Star) 108] filter2*(_|_, F, X, Y) >= add(X, filter(F, Y)) because filter2 > add, [109] and [111], by (Copy) 109] filter2*(_|_, F, X, Y) >= X because [110], by (Select) 110] X >= X by (Meta) 111] filter2*(_|_, F, X, Y) >= filter(F, Y) because filter2 = filter, [112], [113], [114] and [115], by (Stat) 112] F >= F by (Meta) 113] Y >= Y by (Meta) 114] filter2*(_|_, F, X, Y) >= F because [112], by (Select) 115] filter2*(_|_, F, X, Y) >= Y because [113], by (Select) 116] filter2(_|_, F, X, Y) >= filter(F, Y) because [117], by (Star) 117] filter2*(_|_, F, X, Y) >= filter(F, Y) because filter2 = filter, [118], [119], [120] and [121], by (Stat) 118] F >= F by (Meta) 119] Y >= Y by (Meta) 120] filter2*(_|_, F, X, Y) >= F because [118], by (Select) 121] filter2*(_|_, F, X, Y) >= Y because [119], by (Select) 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_14, R_0, static, formative), where P_14 consists of: low#(X, add(Y, Z)) =#> if!fac6220low#(le(Y, X), X, add(Y, Z)) if!fac6220low#(true, X, add(Y, Z)) =#> low#(X, Z) 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_14, R_0, static, formative) is finite. We consider the dependency pair problem (P_14, 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: low#(X, add(Y, Z)) >? if!fac6220low#(le(Y, X), X, add(Y, Z)) if!fac6220low#(true, X, add(Y, Z)) >? low#(X, Z) 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_3, 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) [[if!fac6220low#(x_1, x_2, x_3)]] = if!fac6220low#(x_2, x_3) [[low(x_1, x_2)]] = low(x_2) [[minus(x_1, x_2)]] = x_1 [[nil]] = _|_ [[quot(x_1, x_2)]] = quot(x_1) We choose Lex = {} and Mul = {@_{o -> o}, add, app, filter, filter2, high, if!fac6220high, if!fac6220low, if!fac6220low#, le, low, low#, map, quicksort, quot, s, true}, and the following precedence: filter = filter2 > map > quicksort > @_{o -> o} > app > add = high = if!fac6220high = if!fac6220low = if!fac6220low# = low = low# > le > quot = s > true Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: low#(X, add(Y, Z)) >= if!fac6220low#(X, add(Y, Z)) if!fac6220low#(X, add(Y, Z)) > low#(X, Z) X >= X s(X) >= X quot(_|_) >= _|_ quot(s(X)) >= s(quot(X)) le(_|_, X) >= true le(s(X), _|_) >= _|_ le(s(X), s(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(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] low#(X, add(Y, Z)) >= if!fac6220low#(X, add(Y, Z)) because low# = if!fac6220low#, low# in Mul, [2] and [3], by (Fun) 2] X >= X by (Meta) 3] add(Y, Z) >= add(Y, Z) because add in Mul, [4] and [5], by (Fun) 4] Y >= Y by (Meta) 5] Z >= Z by (Meta) 6] if!fac6220low#(X, add(Y, Z)) > low#(X, Z) because [7], by definition 7] if!fac6220low#*(X, add(Y, Z)) >= low#(X, Z) because if!fac6220low# = low#, if!fac6220low# in Mul, [8] and [9], by (Stat) 8] X >= X by (Meta) 9] add(Y, Z) > Z because [10], by definition 10] add*(Y, Z) >= Z because [11], by (Select) 11] Z >= Z by (Meta) 12] X >= X by (Meta) 13] s(X) >= X because [14], by (Star) 14] s*(X) >= X because [15], by (Select) 15] X >= X by (Meta) 16] quot(_|_) >= _|_ by (Bot) 17] quot(s(X)) >= s(quot(X)) because quot = s, quot in Mul and [18], by (Fun) 18] s(X) >= quot(X) because s = quot, s in Mul and [19], by (Fun) 19] X >= X by (Meta) 20] le(_|_, X) >= true because [21], by (Star) 21] le*(_|_, X) >= true because le > true, by (Copy) 22] le(s(X), _|_) >= _|_ by (Bot) 23] le(s(X), s(Y)) >= le(X, Y) because [24], by (Star) 24] le*(s(X), s(Y)) >= le(X, Y) because le in Mul, [25] and [28], by (Stat) 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 definition 29] s*(Y) >= Y because [30], by (Select) 30] Y >= Y by (Meta) 31] app(_|_, X) >= X because [32], by (Star) 32] app*(_|_, X) >= X because [33], by (Select) 33] X >= X by (Meta) 34] app(add(X, Y), Z) >= add(X, app(Y, Z)) because [35], by (Star) 35] app*(add(X, Y), Z) >= add(X, app(Y, Z)) because app > add, [36] and [40], by (Copy) 36] app*(add(X, Y), Z) >= X because [37], by (Select) 37] add(X, Y) >= X because [38], by (Star) 38] add*(X, Y) >= X because [39], by (Select) 39] X >= X by (Meta) 40] app*(add(X, Y), Z) >= app(Y, Z) because app in Mul, [41] and [44], by (Stat) 41] add(X, Y) > Y because [42], by definition 42] add*(X, Y) >= Y because [43], by (Select) 43] Y >= Y by (Meta) 44] Z >= Z by (Meta) 45] low(_|_) >= _|_ by (Bot) 46] low(add(X, Y)) >= if!fac6220low(add(X, Y)) because low = if!fac6220low, low in Mul and [3], by (Fun) 47] if!fac6220low(add(X, Y)) >= add(X, low(Y)) because [48], by (Star) 48] if!fac6220low*(add(X, Y)) >= add(X, low(Y)) because if!fac6220low = add, if!fac6220low in Mul, [49] and [52], by (Stat) 49] add(X, Y) > X because [50], by definition 50] add*(X, Y) >= X because [51], by (Select) 51] X >= X by (Meta) 52] add(X, Y) > low(Y) because [53], by definition 53] add*(X, Y) >= low(Y) because add = low, add in Mul and [54], by (Stat) 54] Y >= Y by (Meta) 55] if!fac6220low(add(X, Y)) >= low(Y) because [56], by (Star) 56] if!fac6220low*(add(X, Y)) >= low(Y) because if!fac6220low = low, if!fac6220low in Mul and [57], by (Stat) 57] add(X, Y) > Y because [58], by definition 58] add*(X, Y) >= Y because [59], by (Select) 59] Y >= Y by (Meta) 60] high(_|_) >= _|_ by (Bot) 61] high(add(X, Y)) >= if!fac6220high(add(X, Y)) because high = if!fac6220high, high in Mul and [62], by (Fun) 62] add(X, Y) >= add(X, Y) because add in Mul, [63] and [64], by (Fun) 63] X >= X by (Meta) 64] Y >= Y by (Meta) 65] if!fac6220high(add(X, Y)) >= high(Y) because [66], by (Star) 66] if!fac6220high*(add(X, Y)) >= high(Y) because if!fac6220high = high, if!fac6220high in Mul and [67], by (Stat) 67] add(X, Y) > Y because [68], by definition 68] add*(X, Y) >= Y because [69], by (Select) 69] Y >= Y by (Meta) 70] if!fac6220high(add(X, Y)) >= add(X, high(Y)) because [71], by (Star) 71] if!fac6220high*(add(X, Y)) >= add(X, high(Y)) because if!fac6220high = add, if!fac6220high in Mul, [72] and [75], by (Stat) 72] add(X, Y) > X because [73], by definition 73] add*(X, Y) >= X because [74], by (Select) 74] X >= X by (Meta) 75] add(X, Y) > high(Y) because [76], by definition 76] add*(X, Y) >= high(Y) because add = high, add in Mul and [77], by (Stat) 77] Y >= Y by (Meta) 78] quicksort(_|_) >= _|_ by (Bot) 79] quicksort(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(high(Y)))) because [80], by (Star) 80] quicksort*(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(high(Y)))) because quicksort > app, [81] and [85], by (Copy) 81] quicksort*(add(X, Y)) >= quicksort(low(Y)) because quicksort in Mul and [82], by (Stat) 82] add(X, Y) > low(Y) because [83], by definition 83] add*(X, Y) >= low(Y) because add = low, add in Mul and [84], by (Stat) 84] Y >= Y by (Meta) 85] quicksort*(add(X, Y)) >= add(X, quicksort(high(Y))) because quicksort > add, [86] and [90], by (Copy) 86] quicksort*(add(X, Y)) >= X because [87], by (Select) 87] add(X, Y) >= X because [88], by (Star) 88] add*(X, Y) >= X because [89], by (Select) 89] X >= X by (Meta) 90] quicksort*(add(X, Y)) >= quicksort(high(Y)) because quicksort in Mul and [91], by (Stat) 91] add(X, Y) > high(Y) because [92], by definition 92] add*(X, Y) >= high(Y) because add = high, add in Mul and [84], by (Stat) 93] map(F, _|_) >= _|_ by (Bot) 94] map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because [95], by (Star) 95] map*(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because map > add, [96] and [103], by (Copy) 96] map*(F, add(X, Y)) >= @_{o -> o}(F, X) because map > @_{o -> o}, [97] and [99], by (Copy) 97] map*(F, add(X, Y)) >= F because [98], by (Select) 98] F >= F by (Meta) 99] map*(F, 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] map*(F, add(X, Y)) >= map(F, Y) because map in Mul, [104] and [105], by (Stat) 104] F >= F by (Meta) 105] add(X, Y) > Y because [106], by definition 106] add*(X, Y) >= Y because [107], by (Select) 107] Y >= Y by (Meta) 108] filter(F, _|_) >= _|_ by (Bot) 109] filter(F, add(X, Y)) >= filter2(F, X, Y) because [110], by (Star) 110] filter*(F, add(X, Y)) >= filter2(F, X, Y) because filter = filter2, filter in Mul, [111], [112] and [115], by (Stat) 111] F >= F by (Meta) 112] add(X, Y) > X because [113], by definition 113] add*(X, Y) >= X because [114], by (Select) 114] X >= X by (Meta) 115] add(X, Y) > Y because [116], by definition 116] add*(X, Y) >= Y because [117], by (Select) 117] Y >= Y by (Meta) 118] filter2(F, X, Y) >= add(X, filter(F, Y)) because [119], by (Star) 119] filter2*(F, X, Y) >= add(X, filter(F, Y)) because filter2 > add, [120] and [122], by (Copy) 120] filter2*(F, X, Y) >= X because [121], by (Select) 121] X >= X by (Meta) 122] filter2*(F, X, Y) >= filter(F, Y) because filter2 = filter, filter2 in Mul, [123] and [124], by (Stat) 123] F >= F by (Meta) 124] Y >= Y by (Meta) 125] filter2(F, X, Y) >= filter(F, Y) because [126], by (Star) 126] filter2*(F, X, Y) >= filter(F, Y) because filter2 = filter, filter2 in Mul, [127] and [128], by (Stat) 127] F >= F by (Meta) 128] 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_14, R_0, static, formative) by (P_15, R_0, static, formative), where P_15 consists of: 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, static, formative), (P_2, R_0, static, formative), (P_3, R_0, static, formative), (P_4, R_0, static, formative) and (P_15, R_0, static, formative) is finite. We consider the dependency pair problem (P_15, 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 : 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, 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: app#(add(X, Y), Z) >? app#(Y, Z) 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_1, x_3) [[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]] = _|_ [[quot(x_1, x_2)]] = quot(x_1) [[true]] = _|_ We choose Lex = {filter, filter2} and Mul = {@_{o -> o}, add, app, app#, if!fac6220low, le, low, map, quicksort, quot, s}, and the following precedence: app# > filter = filter2 > map > @_{o -> o} > quicksort > app > quot = s > le > add = if!fac6220low = low Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: app#(add(X, Y), Z) > app#(Y, Z) X >= X s(X) >= X quot(_|_) >= _|_ quot(s(X)) >= s(quot(X)) le(_|_, X) >= _|_ le(s(X), _|_) >= _|_ le(s(X), s(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)) 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] app#(add(X, Y), Z) > app#(Y, Z) because [2], by definition 2] app#*(add(X, Y), Z) >= app#(Y, Z) because app# in Mul, [3] and [6], by (Stat) 3] add(X, Y) > Y because [4], by definition 4] add*(X, Y) >= Y because [5], by (Select) 5] Y >= Y by (Meta) 6] Z >= Z by (Meta) 7] X >= X by (Meta) 8] s(X) >= X because [9], by (Star) 9] s*(X) >= X because [10], by (Select) 10] X >= X by (Meta) 11] quot(_|_) >= _|_ by (Bot) 12] quot(s(X)) >= s(quot(X)) because quot = s, quot in Mul and [13], by (Fun) 13] s(X) >= quot(X) because s = quot, s in Mul and [14], by (Fun) 14] X >= X by (Meta) 15] le(_|_, X) >= _|_ by (Bot) 16] le(s(X), _|_) >= _|_ by (Bot) 17] le(s(X), s(Y)) >= le(X, Y) because [18], by (Star) 18] le*(s(X), s(Y)) >= le(X, Y) because le in Mul, [19] and [22], by (Stat) 19] s(X) >= X because [20], by (Star) 20] s*(X) >= X because [21], by (Select) 21] X >= X by (Meta) 22] s(Y) > Y because [23], by definition 23] s*(Y) >= Y because [24], by (Select) 24] Y >= Y by (Meta) 25] app(_|_, X) >= X because [26], by (Star) 26] app*(_|_, X) >= X because [27], by (Select) 27] X >= X by (Meta) 28] app(add(X, Y), Z) >= add(X, app(Y, Z)) because [29], by (Star) 29] app*(add(X, Y), Z) >= add(X, app(Y, Z)) because app > add, [30] and [34], by (Copy) 30] app*(add(X, Y), Z) >= X because [31], by (Select) 31] add(X, Y) >= X because [32], by (Star) 32] add*(X, Y) >= X because [33], by (Select) 33] X >= X by (Meta) 34] app*(add(X, Y), Z) >= app(Y, Z) because app in Mul, [3] and [6], by (Stat) 35] low(_|_) >= _|_ by (Bot) 36] low(add(X, Y)) >= if!fac6220low(add(X, Y)) because low = if!fac6220low, low in Mul and [37], by (Fun) 37] add(X, Y) >= add(X, Y) because add in Mul, [38] and [39], by (Fun) 38] X >= X by (Meta) 39] Y >= Y by (Meta) 40] if!fac6220low(add(X, Y)) >= add(X, low(Y)) because [41], by (Star) 41] if!fac6220low*(add(X, Y)) >= add(X, low(Y)) because if!fac6220low = add, if!fac6220low in Mul, [42] and [45], by (Stat) 42] add(X, Y) > X because [43], by definition 43] add*(X, Y) >= X because [44], by (Select) 44] X >= X by (Meta) 45] add(X, Y) > low(Y) because [46], by definition 46] add*(X, Y) >= low(Y) because add = low, add in Mul and [47], by (Stat) 47] Y >= Y by (Meta) 48] if!fac6220low(add(X, Y)) >= low(Y) because if!fac6220low = low, if!fac6220low in Mul and [49], by (Fun) 49] add(X, Y) >= Y because [50], by (Star) 50] add*(X, Y) >= Y because [51], by (Select) 51] Y >= Y by (Meta) 52] _|_ >= _|_ by (Bot) 53] add(X, Y) >= add(X, Y) because add in Mul, [54] and [55], by (Fun) 54] X >= X by (Meta) 55] Y >= Y by (Meta) 56] add(X, Y) >= Y because [57], by (Star) 57] add*(X, Y) >= Y because [58], by (Select) 58] Y >= Y by (Meta) 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] quicksort(_|_) >= _|_ by (Bot) 63] quicksort(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(Y))) because [64], by (Star) 64] quicksort*(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(Y))) because quicksort > app, [65] and [69], by (Copy) 65] quicksort*(add(X, Y)) >= quicksort(low(Y)) because quicksort in Mul and [66], by (Stat) 66] add(X, Y) > low(Y) because [67], by definition 67] add*(X, Y) >= low(Y) because add = low, add in Mul and [68], by (Stat) 68] Y >= Y by (Meta) 69] quicksort*(add(X, Y)) >= add(X, quicksort(Y)) because quicksort > add, [70] and [74], by (Copy) 70] quicksort*(add(X, Y)) >= X because [71], by (Select) 71] add(X, Y) >= X because [72], by (Star) 72] add*(X, Y) >= X because [73], by (Select) 73] X >= X by (Meta) 74] quicksort*(add(X, Y)) >= quicksort(Y) because quicksort in Mul and [75], by (Stat) 75] add(X, Y) > Y because [76], by definition 76] add*(X, Y) >= Y because [68], by (Select) 77] map(F, _|_) >= _|_ by (Bot) 78] map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because [79], by (Star) 79] map*(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because map > add, [80] and [87], by (Copy) 80] map*(F, add(X, Y)) >= @_{o -> o}(F, X) because map > @_{o -> o}, [81] and [83], by (Copy) 81] map*(F, add(X, Y)) >= F because [82], by (Select) 82] F >= F by (Meta) 83] map*(F, add(X, Y)) >= X because [84], by (Select) 84] add(X, Y) >= X because [85], by (Star) 85] add*(X, Y) >= X because [86], by (Select) 86] X >= X by (Meta) 87] map*(F, add(X, Y)) >= map(F, Y) because map in Mul, [88] and [89], by (Stat) 88] F >= F by (Meta) 89] add(X, Y) > Y because [90], by definition 90] add*(X, Y) >= Y because [91], by (Select) 91] Y >= Y by (Meta) 92] filter(F, _|_) >= _|_ by (Bot) 93] filter(F, add(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because [94], by (Star) 94] filter*(F, add(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because filter = filter2, [95], [96], [99], [100], [101] and [105], by (Stat) 95] F >= F by (Meta) 96] add(X, Y) > Y because [97], by definition 97] add*(X, Y) >= Y because [98], by (Select) 98] Y >= Y by (Meta) 99] filter*(F, add(X, Y)) >= @_{o -> o}(F, X) because filter > @_{o -> o}, [100] and [101], by (Copy) 100] filter*(F, add(X, Y)) >= F because [95], by (Select) 101] filter*(F, add(X, Y)) >= X because [102], by (Select) 102] add(X, Y) >= X because [103], by (Star) 103] add*(X, Y) >= X because [104], by (Select) 104] X >= X by (Meta) 105] filter*(F, add(X, Y)) >= Y because [106], by (Select) 106] add(X, Y) >= Y because [97], by (Star) 107] filter2(_|_, F, X, Y) >= add(X, filter(F, Y)) because [108], by (Star) 108] filter2*(_|_, F, X, Y) >= add(X, filter(F, Y)) because filter2 > add, [109] and [111], by (Copy) 109] filter2*(_|_, F, X, Y) >= X because [110], by (Select) 110] X >= X by (Meta) 111] filter2*(_|_, F, X, Y) >= filter(F, Y) because filter2 = filter, [112], [113], [114] and [115], by (Stat) 112] F >= F by (Meta) 113] Y >= Y by (Meta) 114] filter2*(_|_, F, X, Y) >= F because [112], by (Select) 115] filter2*(_|_, F, X, Y) >= Y because [113], by (Select) 116] filter2(_|_, F, X, Y) >= filter(F, Y) because [117], by (Star) 117] filter2*(_|_, F, X, Y) >= filter(F, Y) because filter2 = filter, [118], [119], [120] and [121], by (Stat) 118] F >= F by (Meta) 119] Y >= Y by (Meta) 120] filter2*(_|_, F, X, Y) >= F because [118], by (Select) 121] filter2*(_|_, F, X, Y) >= Y because [119], by (Select) 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: le#(s(X), s(Y)) >? le#(X, 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) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 0 add = \y0y1.0 app = \y0y1.y1 false = 0 filter = \G0y1.0 filter2 = \y0G1y2y3.0 high = \y0y1.0 if!fac6220high = \y0y1y2.0 if!fac6220low = \y0y1y2.0 le = \y0y1.0 le# = \y0y1.y0 low = \y0y1.0 map = \G0y1.0 minus = \y0y1.y0 nil = 0 quicksort = \y0.0 quot = \y0y1.y0 s = \y0.2 + 2y0 true = 0 Using this interpretation, the requirements translate to: [[le#(s(_x0), s(_x1))]] = 2 + 2x0 > x0 = [[le#(_x0, _x1)]] [[minus(_x0, 0)]] = x0 >= x0 = [[_x0]] [[minus(s(_x0), s(_x1))]] = 2 + 2x0 >= x0 = [[minus(_x0, _x1)]] [[quot(0, s(_x0))]] = 0 >= 0 = [[0]] [[quot(s(_x0), s(_x1))]] = 2 + 2x0 >= 2 + 2x0 = [[s(quot(minus(_x0, _x1), s(_x1)))]] [[le(0, _x0)]] = 0 >= 0 = [[true]] [[le(s(_x0), 0)]] = 0 >= 0 = [[false]] [[le(s(_x0), s(_x1))]] = 0 >= 0 = [[le(_x0, _x1)]] [[app(nil, _x0)]] = x0 >= x0 = [[_x0]] [[app(add(_x0, _x1), _x2)]] = x2 >= 0 = [[add(_x0, app(_x1, _x2))]] [[low(_x0, nil)]] = 0 >= 0 = [[nil]] [[low(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220low(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220low(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[add(_x1, low(_x0, _x2))]] [[if!fac6220low(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[low(_x0, _x2)]] [[high(_x0, nil)]] = 0 >= 0 = [[nil]] [[high(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220high(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220high(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[high(_x0, _x2)]] [[if!fac6220high(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[add(_x1, high(_x0, _x2))]] [[quicksort(nil)]] = 0 >= 0 = [[nil]] [[quicksort(add(_x0, _x1))]] = 0 >= 0 = [[app(quicksort(low(_x0, _x1)), add(_x0, quicksort(high(_x0, _x1))))]] [[map(_F0, nil)]] = 0 >= 0 = [[nil]] [[map(_F0, add(_x1, _x2))]] = 0 >= 0 = [[add(_F0 _x1, map(_F0, _x2))]] [[filter(_F0, nil)]] = 0 >= 0 = [[nil]] [[filter(_F0, add(_x1, _x2))]] = 0 >= 0 = [[filter2(_F0 _x1, _F0, _x1, _x2)]] [[filter2(true, _F0, _x1, _x2)]] = 0 >= 0 = [[add(_x1, filter(_F0, _x2))]] [[filter2(false, _F0, _x1, _x2)]] = 0 >= 0 = [[filter(_F0, _x2)]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_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: quot#(s(X), s(Y)) >? quot#(minus(X, Y), s(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) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 0 add = \y0y1.0 app = \y0y1.2y1 false = 0 filter = \G0y1.2G0(0) filter2 = \y0G1y2y3.2G1(0) high = \y0y1.0 if!fac6220high = \y0y1y2.0 if!fac6220low = \y0y1y2.0 le = \y0y1.0 low = \y0y1.0 map = \G0y1.0 minus = \y0y1.y0 nil = 0 quicksort = \y0.0 quot = \y0y1.y0 quot# = \y0y1.y0 s = \y0.1 + y0 true = 0 Using this interpretation, the requirements translate to: [[quot#(s(_x0), s(_x1))]] = 1 + x0 > x0 = [[quot#(minus(_x0, _x1), s(_x1))]] [[minus(_x0, 0)]] = x0 >= x0 = [[_x0]] [[minus(s(_x0), s(_x1))]] = 1 + x0 >= x0 = [[minus(_x0, _x1)]] [[quot(0, s(_x0))]] = 0 >= 0 = [[0]] [[quot(s(_x0), s(_x1))]] = 1 + x0 >= 1 + x0 = [[s(quot(minus(_x0, _x1), s(_x1)))]] [[le(0, _x0)]] = 0 >= 0 = [[true]] [[le(s(_x0), 0)]] = 0 >= 0 = [[false]] [[le(s(_x0), s(_x1))]] = 0 >= 0 = [[le(_x0, _x1)]] [[app(nil, _x0)]] = 2x0 >= x0 = [[_x0]] [[app(add(_x0, _x1), _x2)]] = 2x2 >= 0 = [[add(_x0, app(_x1, _x2))]] [[low(_x0, nil)]] = 0 >= 0 = [[nil]] [[low(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220low(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220low(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[add(_x1, low(_x0, _x2))]] [[if!fac6220low(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[low(_x0, _x2)]] [[high(_x0, nil)]] = 0 >= 0 = [[nil]] [[high(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220high(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220high(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[high(_x0, _x2)]] [[if!fac6220high(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[add(_x1, high(_x0, _x2))]] [[quicksort(nil)]] = 0 >= 0 = [[nil]] [[quicksort(add(_x0, _x1))]] = 0 >= 0 = [[app(quicksort(low(_x0, _x1)), add(_x0, quicksort(high(_x0, _x1))))]] [[map(_F0, nil)]] = 0 >= 0 = [[nil]] [[map(_F0, add(_x1, _x2))]] = 0 >= 0 = [[add(_F0 _x1, map(_F0, _x2))]] [[filter(_F0, nil)]] = 2F0(0) >= 0 = [[nil]] [[filter(_F0, add(_x1, _x2))]] = 2F0(0) >= 2F0(0) = [[filter2(_F0 _x1, _F0, _x1, _x2)]] [[filter2(true, _F0, _x1, _x2)]] = 2F0(0) >= 0 = [[add(_x1, filter(_F0, _x2))]] [[filter2(false, _F0, _x1, _x2)]] = 2F0(0) >= 2F0(0) = [[filter(_F0, _x2)]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace 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: minus#(s(X), s(Y)) >? minus#(X, 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) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 0 add = \y0y1.0 app = \y0y1.y1 false = 0 filter = \G0y1.0 filter2 = \y0G1y2y3.0 high = \y0y1.0 if!fac6220high = \y0y1y2.0 if!fac6220low = \y0y1y2.0 le = \y0y1.0 low = \y0y1.0 map = \G0y1.0 minus = \y0y1.y0 minus# = \y0y1.y1 nil = 0 quicksort = \y0.0 quot = \y0y1.1 + 2y1 + 3y0 s = \y0.3 + y0 true = 0 Using this interpretation, the requirements translate to: [[minus#(s(_x0), s(_x1))]] = 3 + x1 > x1 = [[minus#(_x0, _x1)]] [[minus(_x0, 0)]] = x0 >= x0 = [[_x0]] [[minus(s(_x0), s(_x1))]] = 3 + x0 >= x0 = [[minus(_x0, _x1)]] [[quot(0, s(_x0))]] = 7 + 2x0 >= 0 = [[0]] [[quot(s(_x0), s(_x1))]] = 16 + 2x1 + 3x0 >= 10 + 2x1 + 3x0 = [[s(quot(minus(_x0, _x1), s(_x1)))]] [[le(0, _x0)]] = 0 >= 0 = [[true]] [[le(s(_x0), 0)]] = 0 >= 0 = [[false]] [[le(s(_x0), s(_x1))]] = 0 >= 0 = [[le(_x0, _x1)]] [[app(nil, _x0)]] = x0 >= x0 = [[_x0]] [[app(add(_x0, _x1), _x2)]] = x2 >= 0 = [[add(_x0, app(_x1, _x2))]] [[low(_x0, nil)]] = 0 >= 0 = [[nil]] [[low(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220low(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220low(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[add(_x1, low(_x0, _x2))]] [[if!fac6220low(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[low(_x0, _x2)]] [[high(_x0, nil)]] = 0 >= 0 = [[nil]] [[high(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220high(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220high(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[high(_x0, _x2)]] [[if!fac6220high(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[add(_x1, high(_x0, _x2))]] [[quicksort(nil)]] = 0 >= 0 = [[nil]] [[quicksort(add(_x0, _x1))]] = 0 >= 0 = [[app(quicksort(low(_x0, _x1)), add(_x0, quicksort(high(_x0, _x1))))]] [[map(_F0, nil)]] = 0 >= 0 = [[nil]] [[map(_F0, add(_x1, _x2))]] = 0 >= 0 = [[add(_F0 _x1, map(_F0, _x2))]] [[filter(_F0, nil)]] = 0 >= 0 = [[nil]] [[filter(_F0, add(_x1, _x2))]] = 0 >= 0 = [[filter2(_F0 _x1, _F0, _x1, _x2)]] [[filter2(true, _F0, _x1, _x2)]] = 0 >= 0 = [[add(_x1, filter(_F0, _x2))]] [[filter2(false, _F0, _x1, _x2)]] = 0 >= 0 = [[filter(_F0, _x2)]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_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.