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 with usable rules [Kop12, Thm. 7.44]. (P_8, R_0) has no usable rules. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: map#(F, add(X, Y)) >? map#(F, Y) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: add = \y0y1.3 + 2y1 map# = \G0y1.y1 Using this interpretation, the requirements translate to: [[map#(_F0, add(_x1, _x2))]] = 3 + 2x2 > x2 = [[map#(_F0, _x2)]] 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 with usable rules [Kop12, Thm. 7.44]. The usable rules of (P_7, R_0) are: le(0, X) => true le(s(X), 0) => false le(s(X), s(Y)) => le(X, Y) low(X, nil) => nil low(X, add(Y, Z)) => if!fac6220low(le(Y, X), X, add(Y, Z)) if!fac6220low(true, X, add(Y, Z)) => add(Y, low(X, Z)) if!fac6220low(false, X, add(Y, Z)) => low(X, Z) high(X, nil) => nil high(X, add(Y, Z)) => if!fac6220high(le(Y, X), X, add(Y, Z)) if!fac6220high(true, X, add(Y, Z)) => high(X, Z) if!fac6220high(false, X, add(Y, Z)) => add(Y, high(X, Z)) It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: quicksort#(add(X, Y)) >? quicksort#(low(X, Y)) quicksort#(add(X, Y)) >? quicksort#(high(X, Y)) le(0, X) >= true le(s(X), 0) >= false le(s(X), s(Y)) >= le(X, Y) low(X, nil) >= nil low(X, add(Y, Z)) >= if!fac6220low(le(Y, X), X, add(Y, Z)) if!fac6220low(true, X, add(Y, Z)) >= add(Y, low(X, Z)) if!fac6220low(false, X, add(Y, Z)) >= low(X, Z) high(X, nil) >= nil high(X, add(Y, Z)) >= if!fac6220high(le(Y, X), X, add(Y, Z)) if!fac6220high(true, X, add(Y, Z)) >= high(X, Z) if!fac6220high(false, X, add(Y, Z)) >= add(Y, high(X, Z)) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 3 add = \y0y1.2 + 3y1 false = 0 high = \y0y1.y1 if!fac6220high = \y0y1y2.y2 if!fac6220low = \y0y1y2.2 + 3y2 le = \y0y1.0 low = \y0y1.2 + 3y1 nil = 0 quicksort# = \y0.2y0 s = \y0.3 true = 0 Using this interpretation, the requirements translate to: [[quicksort#(add(_x0, _x1))]] = 4 + 6x1 >= 4 + 6x1 = [[quicksort#(low(_x0, _x1))]] [[quicksort#(add(_x0, _x1))]] = 4 + 6x1 > 2x1 = [[quicksort#(high(_x0, _x1))]] [[le(0, _x0)]] = 0 >= 0 = [[true]] [[le(s(_x0), 0)]] = 0 >= 0 = [[false]] [[le(s(_x0), s(_x1))]] = 0 >= 0 = [[le(_x0, _x1)]] [[low(_x0, nil)]] = 2 >= 0 = [[nil]] [[low(_x0, add(_x1, _x2))]] = 8 + 9x2 >= 8 + 9x2 = [[if!fac6220low(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220low(true, _x0, add(_x1, _x2))]] = 8 + 9x2 >= 8 + 9x2 = [[add(_x1, low(_x0, _x2))]] [[if!fac6220low(false, _x0, add(_x1, _x2))]] = 8 + 9x2 >= 2 + 3x2 = [[low(_x0, _x2)]] [[high(_x0, nil)]] = 0 >= 0 = [[nil]] [[high(_x0, add(_x1, _x2))]] = 2 + 3x2 >= 2 + 3x2 = [[if!fac6220high(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220high(true, _x0, add(_x1, _x2))]] = 2 + 3x2 >= x2 = [[high(_x0, _x2)]] [[if!fac6220high(false, _x0, add(_x1, _x2))]] = 2 + 3x2 >= 2 + 3x2 = [[add(_x1, high(_x0, _x2))]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_7, R_0, static, formative) by (P_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 with usable rules [Kop12, Thm. 7.44]. The usable rules of (P_11, R_0) are: le(0, X) => true le(s(X), 0) => false le(s(X), s(Y)) => le(X, Y) low(X, nil) => nil low(X, add(Y, Z)) => if!fac6220low(le(Y, X), X, add(Y, Z)) if!fac6220low(true, X, add(Y, Z)) => add(Y, low(X, Z)) if!fac6220low(false, X, add(Y, Z)) => low(X, Z) It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: quicksort#(add(X, Y)) >? quicksort#(low(X, Y)) le(0, X) >= true le(s(X), 0) >= false le(s(X), s(Y)) >= le(X, Y) low(X, nil) >= nil low(X, add(Y, Z)) >= if!fac6220low(le(Y, X), X, add(Y, Z)) if!fac6220low(true, X, add(Y, Z)) >= add(Y, low(X, Z)) if!fac6220low(false, X, add(Y, Z)) >= low(X, Z) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 3 add = \y0y1.2 + 2y0 + 2y1 false = 0 if!fac6220low = \y0y1y2.2y2 le = \y0y1.0 low = \y0y1.2y1 nil = 0 quicksort# = \y0.2y0 s = \y0.3 true = 0 Using this interpretation, the requirements translate to: [[quicksort#(add(_x0, _x1))]] = 4 + 4x0 + 4x1 > 4x1 = [[quicksort#(low(_x0, _x1))]] [[le(0, _x0)]] = 0 >= 0 = [[true]] [[le(s(_x0), 0)]] = 0 >= 0 = [[false]] [[le(s(_x0), s(_x1))]] = 0 >= 0 = [[le(_x0, _x1)]] [[low(_x0, nil)]] = 0 >= 0 = [[nil]] [[low(_x0, add(_x1, _x2))]] = 4 + 4x1 + 4x2 >= 4 + 4x1 + 4x2 = [[if!fac6220low(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220low(true, _x0, add(_x1, _x2))]] = 4 + 4x1 + 4x2 >= 2 + 2x1 + 4x2 = [[add(_x1, low(_x0, _x2))]] [[if!fac6220low(false, _x0, add(_x1, _x2))]] = 4 + 4x1 + 4x2 >= 2x2 = [[low(_x0, _x2)]] 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 with usable rules [Kop12, Thm. 7.44]. The usable rules of (P_6, R_0) are: le(0, X) => true le(s(X), 0) => false le(s(X), s(Y)) => le(X, Y) 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) le(0, X) >= true le(s(X), 0) >= false le(s(X), s(Y)) >= le(X, Y) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 3 add = \y0y1.3 + 3y0 + 3y1 false = 0 high# = \y0y1.3y1 if!fac6220high# = \y0y1y2.2y2 le = \y0y1.2y1 + 3y0 s = \y0.3 + 3y0 true = 0 Using this interpretation, the requirements translate to: [[high#(_x0, add(_x1, _x2))]] = 9 + 9x1 + 9x2 > 6 + 6x1 + 6x2 = [[if!fac6220high#(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220high#(true, _x0, add(_x1, _x2))]] = 6 + 6x1 + 6x2 > 3x2 = [[high#(_x0, _x2)]] [[if!fac6220high#(false, _x0, add(_x1, _x2))]] = 6 + 6x1 + 6x2 > 3x2 = [[high#(_x0, _x2)]] [[le(0, _x0)]] = 9 + 2x0 >= 0 = [[true]] [[le(s(_x0), 0)]] = 15 + 9x0 >= 0 = [[false]] [[le(s(_x0), s(_x1))]] = 15 + 6x1 + 9x0 >= 2x1 + 3x0 = [[le(_x0, _x1)]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_6, R_0) by ({}, R_0). By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed. Thus, the original system is terminating if each of (P_1, R_0, static, formative), (P_2, R_0, static, formative), (P_3, R_0, static, formative), (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 with usable rules [Kop12, Thm. 7.44]. The usable rules of (P_5, R_0) are: le(0, X) => true le(s(X), 0) => false le(s(X), s(Y)) => le(X, Y) 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) le(0, X) >= true le(s(X), 0) >= false le(s(X), s(Y)) >= le(X, Y) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 3 add = \y0y1.3 + 3y0 + 3y1 false = 0 if!fac6220low# = \y0y1y2.2y2 le = \y0y1.2y1 + 3y0 low# = \y0y1.3y1 s = \y0.3 + 3y0 true = 0 Using this interpretation, the requirements translate to: [[low#(_x0, add(_x1, _x2))]] = 9 + 9x1 + 9x2 > 6 + 6x1 + 6x2 = [[if!fac6220low#(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220low#(true, _x0, add(_x1, _x2))]] = 6 + 6x1 + 6x2 > 3x2 = [[low#(_x0, _x2)]] [[if!fac6220low#(false, _x0, add(_x1, _x2))]] = 6 + 6x1 + 6x2 > 3x2 = [[low#(_x0, _x2)]] [[le(0, _x0)]] = 9 + 2x0 >= 0 = [[true]] [[le(s(_x0), 0)]] = 15 + 9x0 >= 0 = [[false]] [[le(s(_x0), s(_x1))]] = 15 + 6x1 + 9x0 >= 2x1 + 3x0 = [[le(_x0, _x1)]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_5, R_0) by ({}, R_0). By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed. Thus, the original system is terminating if each of (P_1, R_0, static, formative), (P_2, R_0, static, formative), (P_3, R_0, static, formative) and (P_4, R_0, static, formative) is finite. We consider the dependency pair problem (P_4, R_0, static, formative). We will use the reduction pair processor with usable rules [Kop12, Thm. 7.44]. (P_4, R_0) has no usable rules. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: app#(add(X, Y), Z) >? app#(Y, Z) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: add = \y0y1.1 + 2y1 app# = \y0y1.y0 Using this interpretation, the requirements translate to: [[app#(add(_x0, _x1), _x2)]] = 1 + 2x1 > x1 = [[app#(_x1, _x2)]] 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 with usable rules [Kop12, Thm. 7.44]. (P_3, R_0) has no usable rules. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: le#(s(X), s(Y)) >? le#(X, Y) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: le# = \y0y1.y0 + y1 s = \y0.3 + 2y0 Using this interpretation, the requirements translate to: [[le#(s(_x0), s(_x1))]] = 6 + 2x0 + 2x1 > x0 + x1 = [[le#(_x0, _x1)]] 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 with usable rules [Kop12, Thm. 7.44]. The usable rules of (P_2, R_0) are: minus(X, 0) => X minus(s(X), s(Y)) => minus(X, Y) It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: quot#(s(X), s(Y)) >? quot#(minus(X, Y), s(Y)) minus(X, 0) >= X minus(s(X), s(Y)) >= minus(X, Y) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 0 minus = \y0y1.y0 quot# = \y0y1.3y0 s = \y0.3 + 3y0 Using this interpretation, the requirements translate to: [[quot#(s(_x0), s(_x1))]] = 9 + 9x0 > 3x0 = [[quot#(minus(_x0, _x1), s(_x1))]] [[minus(_x0, 0)]] = x0 >= x0 = [[_x0]] [[minus(s(_x0), s(_x1))]] = 3 + 3x0 >= x0 = [[minus(_x0, _x1)]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_2, R_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 with usable rules [Kop12, Thm. 7.44]. (P_1, R_0) has no usable rules. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: minus#(s(X), s(Y)) >? minus#(X, Y) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: minus# = \y0y1.y0 + y1 s = \y0.3 + 2y0 Using this interpretation, the requirements translate to: [[minus#(s(_x0), s(_x1))]] = 6 + 2x0 + 2x1 > x0 + x1 = [[minus#(_x0, _x1)]] 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.