We consider the system Applicative_first_order_05__11. Alphabet: !facminus : [a * a] --> a !facplus : [a * a] --> a !factimes : [a * a] --> a 0 : [] --> a 1 : [] --> a 2 : [] --> a D : [a] --> a cons : [c * d] --> d constant : [] --> a div : [a * a] --> a false : [] --> b filter : [c -> b * d] --> d filter2 : [b * c -> b * c * d] --> d ln : [a] --> a map : [c -> c * d] --> d minus : [a] --> a nil : [] --> d pow : [a * a] --> a t : [] --> a true : [] --> b Rules: D(t) => 1 D(constant) => 0 D(!facplus(x, y)) => !facplus(D(x), D(y)) D(!factimes(x, y)) => !facplus(!factimes(y, D(x)), !factimes(x, D(y))) D(!facminus(x, y)) => !facminus(D(x), D(y)) D(minus(x)) => minus(D(x)) D(div(x, y)) => !facminus(div(D(x), y), div(!factimes(x, D(y)), pow(y, 2))) D(ln(x)) => div(D(x), x) D(pow(x, y)) => !facplus(!factimes(!factimes(y, pow(x, !facminus(y, 1))), D(x)), !factimes(!factimes(pow(x, y), ln(x)), D(y))) map(f, nil) => nil map(f, cons(x, y)) => cons(f x, map(f, y)) filter(f, nil) => nil filter(f, cons(x, y)) => filter2(f x, f, x, y) filter2(true, f, x, y) => cons(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 rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): D(t) >? 1 D(constant) >? 0 D(!facplus(X, Y)) >? !facplus(D(X), D(Y)) D(!factimes(X, Y)) >? !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X, Y)) >? !facminus(D(X), D(Y)) D(minus(X)) >? minus(D(X)) D(div(X, Y)) >? !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) D(ln(X)) >? div(D(X), X) D(pow(X, Y)) >? !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) map(F, nil) >? nil map(F, cons(X, Y)) >? cons(F X, map(F, Y)) filter(F, nil) >? nil filter(F, cons(X, Y)) >? filter2(F X, F, X, Y) filter2(true, F, X, Y) >? cons(X, filter(F, Y)) filter2(false, F, X, Y) >? filter(F, Y) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[!facminus(x_1, x_2)]] = !facminus(x_2, x_1) [[!facplus(x_1, x_2)]] = !facplus(x_2, x_1) [[0]] = _|_ [[1]] = _|_ [[2]] = _|_ [[cons(x_1, x_2)]] = cons(x_2, x_1) [[div(x_1, x_2)]] = div(x_2, x_1) [[filter2(x_1, x_2, x_3, x_4)]] = filter2(x_2, x_4, x_3, x_1) [[pow(x_1, x_2)]] = pow(x_2, x_1) We choose Lex = {!facminus, !facplus, D, cons, div, filter, filter2, pow} and Mul = {!factimes, @_{o -> o}, constant, false, ln, map, minus, nil, t, true}, and the following precedence: filter = filter2 > map > @_{o -> o} > cons > D = div > false > !facminus > ln > minus > !factimes > nil > !facplus = pow > t > true > constant Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: D(t) > _|_ D(constant) >= _|_ D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) D(minus(X)) >= minus(D(X)) D(div(X, Y)) >= !facminus(div D(X) Y, div) D(ln(X)) >= div(D(X), X) D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow X !facminus(Y, _|_)), D(X)), !factimes(!factimes(pow, ln(X)), D(Y))) map(F, nil) > nil map(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) filter(F, nil) > nil filter(F, cons(X, Y)) > filter2(@_{o -> o}(F, X), F, X, Y) filter2(true, F, X, Y) > cons(X, filter(F, Y)) filter2(false, F, X, Y) > filter(F, Y) With these choices, we have: 1] D(t) > _|_ because [2], by definition 2] D*(t) >= _|_ by (Bot) 3] D(constant) >= _|_ by (Bot) 4] D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) because [5], by (Star) 5] D*(!facplus(X, Y)) >= !facplus(D(X), D(Y)) because D > !facplus, [6] and [12], by (Copy) 6] D*(!facplus(X, Y)) >= D(X) because [7], [10] and [7], by (Stat) 7] !facplus(X, Y) > X because [8], by definition 8] !facplus*(X, Y) >= X because [9], by (Select) 9] X >= X by (Meta) 10] D*(!facplus(X, Y)) >= X because [11], by (Select) 11] !facplus(X, Y) >= X because [8], by (Star) 12] D*(!facplus(X, Y)) >= D(Y) because [13], [16] and [13], by (Stat) 13] !facplus(X, Y) > Y because [14], by definition 14] !facplus*(X, Y) >= Y because [15], by (Select) 15] Y >= Y by (Meta) 16] D*(!facplus(X, Y)) >= Y because [17], by (Select) 17] !facplus(X, Y) >= Y because [14], by (Star) 18] D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) because [19], by (Star) 19] D*(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) because D > !facplus, [20] and [31], by (Copy) 20] D*(!factimes(X, Y)) >= !factimes(Y, D(X)) because D > !factimes, [21] and [25], by (Copy) 21] D*(!factimes(X, Y)) >= Y because [22], by (Select) 22] !factimes(X, Y) >= Y because [23], by (Star) 23] !factimes*(X, Y) >= Y because [24], by (Select) 24] Y >= Y by (Meta) 25] D*(!factimes(X, Y)) >= D(X) because [26], [29] and [26], by (Stat) 26] !factimes(X, Y) > X because [27], by definition 27] !factimes*(X, Y) >= X because [28], by (Select) 28] X >= X by (Meta) 29] D*(!factimes(X, Y)) >= X because [30], by (Select) 30] !factimes(X, Y) >= X because [27], by (Star) 31] D*(!factimes(X, Y)) >= !factimes(X, D(Y)) because D > !factimes, [29] and [32], by (Copy) 32] D*(!factimes(X, Y)) >= D(Y) because [33], [21] and [33], by (Stat) 33] !factimes(X, Y) > Y because [34], by definition 34] !factimes*(X, Y) >= Y because [24], by (Select) 35] D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) because [36], by (Star) 36] D*(!facminus(X, Y)) >= !facminus(D(X), D(Y)) because D > !facminus, [37] and [43], by (Copy) 37] D*(!facminus(X, Y)) >= D(X) because [38], [41] and [38], by (Stat) 38] !facminus(X, Y) > X because [39], by definition 39] !facminus*(X, Y) >= X because [40], by (Select) 40] X >= X by (Meta) 41] D*(!facminus(X, Y)) >= X because [42], by (Select) 42] !facminus(X, Y) >= X because [39], by (Star) 43] D*(!facminus(X, Y)) >= D(Y) because [44], [47] and [44], by (Stat) 44] !facminus(X, Y) > Y because [45], by definition 45] !facminus*(X, Y) >= Y because [46], by (Select) 46] Y >= Y by (Meta) 47] D*(!facminus(X, Y)) >= Y because [48], by (Select) 48] !facminus(X, Y) >= Y because [45], by (Star) 49] D(minus(X)) >= minus(D(X)) because [50], by (Star) 50] D*(minus(X)) >= minus(D(X)) because D > minus and [51], by (Copy) 51] D*(minus(X)) >= D(X) because [52] and [55], by (Stat) 52] minus(X) > X because [53], by definition 53] minus*(X) >= X because [54], by (Select) 54] X >= X by (Meta) 55] D*(minus(X)) >= X because [56], by (Select) 56] minus(X) >= X because [53], by (Star) 57] D(div(X, Y)) >= !facminus(div D(X) Y, div) because [58], by (Star) 58] D*(div(X, Y)) >= !facminus(div D(X) Y, div) because D > !facminus, [59] and [71], by (Copy) 59] D*(div(X, Y)) >= div(D(X), Y) because D = div, [60], [63] and [69], by (Stat) 60] div(X, Y) > Y because [61], by definition 61] div*(X, Y) >= Y because [62], by (Select) 62] Y >= Y by (Meta) 63] D*(div(X, Y)) >= D(X) because [64], [67] and [64], by (Stat) 64] div(X, Y) > X because [65], by definition 65] div*(X, Y) >= X because [66], by (Select) 66] X >= X by (Meta) 67] D*(div(X, Y)) >= X because [68], by (Select) 68] div(X, Y) >= X because [65], by (Star) 69] D*(div(X, Y)) >= Y because [70], by (Select) 70] div(X, Y) >= Y because [61], by (Star) 71] D*(div(X, Y)) >= div(!factimes(X, D(Y)), pow(Y, _|_)) because D = div, [72], [75] and [77], by (Stat) 72] div(X, Y) > pow(Y, _|_) because [73], by definition 73] div*(X, Y) >= pow(Y, _|_) because div > pow, [61] and [74], by (Copy) 74] div*(X, Y) >= _|_ by (Bot) 75] D*(div(X, Y)) >= !factimes(X, D(Y)) because D > !factimes, [67] and [76], by (Copy) 76] D*(div(X, Y)) >= D(Y) because [60], [69] and [60], by (Stat) 77] D*(div(X, Y)) >= pow(Y, _|_) because [78], by (Select) 78] div(X, Y) >= pow(Y, _|_) because [73], by (Star) 79] D(ln(X)) >= div(D(X), X) because [80], by (Star) 80] D*(ln(X)) >= div(D(X), X) because D = div, [81], [84] and [85], by (Stat) 81] ln(X) > X because [82], by definition 82] ln*(X) >= X because [83], by (Select) 83] X >= X by (Meta) 84] D*(ln(X)) >= D(X) because [81] and [85], by (Stat) 85] D*(ln(X)) >= X because [86], by (Select) 86] ln(X) >= X because [82], by (Star) 87] D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow X !facminus(Y, _|_)), D(X)), !factimes(!factimes(pow, ln(X)), D(Y))) because [88], by (Star) 88] D*(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow X !facminus(Y, _|_)), D(X)), !factimes(!factimes(pow, ln(X)), D(Y))) because D > !facplus, [89] and [105], by (Copy) 89] D*(pow(X, Y)) >= !factimes(!factimes(Y, pow(X, !facminus(Y, _|_))), D(X)) because D > !factimes, [90] and [102], by (Copy) 90] D*(pow(X, Y)) >= !factimes(Y, pow(X, !facminus(Y, _|_))) because D > !factimes, [91] and [95], by (Copy) 91] D*(pow(X, Y)) >= Y because [92], by (Select) 92] pow(X, Y) >= Y because [93], by (Star) 93] pow*(X, Y) >= Y because [94], by (Select) 94] Y >= Y by (Meta) 95] D*(pow(X, Y)) >= pow(X, !facminus(Y, _|_)) because D > pow, [96] and [100], by (Copy) 96] D*(pow(X, Y)) >= X because [97], by (Select) 97] pow(X, Y) >= X because [98], by (Star) 98] pow*(X, Y) >= X because [99], by (Select) 99] X >= X by (Meta) 100] D*(pow(X, Y)) >= !facminus(Y, _|_) because D > !facminus, [91] and [101], by (Copy) 101] D*(pow(X, Y)) >= _|_ by (Bot) 102] D*(pow(X, Y)) >= D(X) because [103], [96] and [103], by (Stat) 103] pow(X, Y) > X because [104], by definition 104] pow*(X, Y) >= X because [99], by (Select) 105] D*(pow(X, Y)) >= !factimes(!factimes(pow(X, Y), ln(X)), D(Y)) because D > !factimes, [106] and [112], by (Copy) 106] D*(pow(X, Y)) >= !factimes(pow(X, Y), ln(X)) because D > !factimes, [107] and [111], by (Copy) 107] D*(pow(X, Y)) >= pow(X, Y) because [108], by (Select) 108] pow(X, Y) >= pow(X, Y) because [109] and [110], by (Fun) 109] X >= X by (Meta) 110] Y >= Y by (Meta) 111] D*(pow(X, Y)) >= ln(X) because D > ln and [96], by (Copy) 112] D*(pow(X, Y)) >= D(Y) because [113], [91] and [113], by (Stat) 113] pow(X, Y) > Y because [114], by definition 114] pow*(X, Y) >= Y because [110], by (Select) 115] map(F, nil) > nil because [116], by definition 116] map*(F, nil) >= nil because [117], by (Select) 117] nil >= nil by (Fun) 118] map(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) because [119], by (Star) 119] map*(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) because map > cons, [120] and [127], by (Copy) 120] map*(F, cons(X, Y)) >= @_{o -> o}(F, X) because map > @_{o -> o}, [121] and [123], by (Copy) 121] map*(F, cons(X, Y)) >= F because [122], by (Select) 122] F >= F by (Meta) 123] map*(F, cons(X, Y)) >= X because [124], by (Select) 124] cons(X, Y) >= X because [125], by (Star) 125] cons*(X, Y) >= X because [126], by (Select) 126] X >= X by (Meta) 127] map*(F, cons(X, Y)) >= map(F, Y) because map in Mul, [128] and [129], by (Stat) 128] F >= F by (Meta) 129] cons(X, Y) > Y because [130], by definition 130] cons*(X, Y) >= Y because [131], by (Select) 131] Y >= Y by (Meta) 132] filter(F, nil) > nil because [133], by definition 133] filter*(F, nil) >= nil because [117], by (Select) 134] filter(F, cons(X, Y)) > filter2(@_{o -> o}(F, X), F, X, Y) because [135], by definition 135] filter*(F, cons(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because filter = filter2, [136], [137], [140], [141], [142] and [146], by (Stat) 136] F >= F by (Meta) 137] cons(X, Y) > Y because [138], by definition 138] cons*(X, Y) >= Y because [139], by (Select) 139] Y >= Y by (Meta) 140] filter*(F, cons(X, Y)) >= @_{o -> o}(F, X) because filter > @_{o -> o}, [141] and [142], by (Copy) 141] filter*(F, cons(X, Y)) >= F because [136], by (Select) 142] filter*(F, cons(X, Y)) >= X because [143], by (Select) 143] cons(X, Y) >= X because [144], by (Star) 144] cons*(X, Y) >= X because [145], by (Select) 145] X >= X by (Meta) 146] filter*(F, cons(X, Y)) >= Y because [147], by (Select) 147] cons(X, Y) >= Y because [138], by (Star) 148] filter2(true, F, X, Y) > cons(X, filter(F, Y)) because [149], by definition 149] filter2*(true, F, X, Y) >= cons(X, filter(F, Y)) because filter2 > cons, [150] and [152], by (Copy) 150] filter2*(true, F, X, Y) >= X because [151], by (Select) 151] X >= X by (Meta) 152] filter2*(true, F, X, Y) >= filter(F, Y) because filter2 = filter, [153], [154], [155], [156], [153] and [154], by (Stat) 153] F >= F by (Meta) 154] Y >= Y by (Meta) 155] filter2*(true, F, X, Y) >= F because [153], by (Select) 156] filter2*(true, F, X, Y) >= Y because [154], by (Select) 157] filter2(false, F, X, Y) > filter(F, Y) because [158], by definition 158] filter2*(false, F, X, Y) >= filter(F, Y) because filter2 = filter, [159], [160], [161], [162], [159] and [160], by (Stat) 159] F >= F by (Meta) 160] Y >= Y by (Meta) 161] filter2*(false, F, X, Y) >= F because [159], by (Select) 162] filter2*(false, F, X, Y) >= Y because [160], by (Select) We can thus remove the following rules: D(t) => 1 map(F, nil) => nil filter(F, nil) => nil filter(F, cons(X, Y)) => filter2(F X, F, X, Y) filter2(true, F, X, Y) => cons(X, filter(F, Y)) filter2(false, F, X, Y) => filter(F, Y) We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): D(constant) >? 0 D(!facplus(X, Y)) >? !facplus(D(X), D(Y)) D(!factimes(X, Y)) >? !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X, Y)) >? !facminus(D(X), D(Y)) D(minus(X)) >? minus(D(X)) D(div(X, Y)) >? !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) D(ln(X)) >? div(D(X), X) D(pow(X, Y)) >? !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) map(F, cons(X, Y)) >? cons(F X, map(F, Y)) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[!facminus(x_1, x_2)]] = !facminus(x_2, x_1) [[!facplus(x_1, x_2)]] = !facplus(x_2, x_1) [[0]] = _|_ [[1]] = _|_ [[2]] = _|_ [[div(x_1, x_2)]] = div(x_2, x_1) [[minus(x_1)]] = x_1 [[pow(x_1, x_2)]] = pow(x_2, x_1) We choose Lex = {!facminus, !facplus, D, div, pow} and Mul = {!factimes, @_{o -> o}, cons, constant, ln, map}, and the following precedence: map > @_{o -> o} > cons > D > div > ln > pow > !facminus > !facplus > !factimes > constant Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: D(constant) > _|_ D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) D(X) >= D(X) D(div(X, Y)) >= !facminus(div D(X) Y, div) D(ln(X)) >= div(D(X), X) D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow X !facminus(Y, _|_)), D(X)), !factimes(!factimes(pow, ln(X)), D(Y))) map(F, cons(X, Y)) > cons(@_{o -> o}(F, X), map(F, Y)) With these choices, we have: 1] D(constant) > _|_ because [2], by definition 2] D*(constant) >= _|_ by (Bot) 3] D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) because [4], by (Star) 4] D*(!facplus(X, Y)) >= !facplus(D(X), D(Y)) because D > !facplus, [5] and [11], by (Copy) 5] D*(!facplus(X, Y)) >= D(X) because [6], [9] and [6], by (Stat) 6] !facplus(X, Y) > X because [7], by definition 7] !facplus*(X, Y) >= X because [8], by (Select) 8] X >= X by (Meta) 9] D*(!facplus(X, Y)) >= X because [10], by (Select) 10] !facplus(X, Y) >= X because [7], by (Star) 11] D*(!facplus(X, Y)) >= D(Y) because [12], [15] and [12], by (Stat) 12] !facplus(X, Y) > Y because [13], by definition 13] !facplus*(X, Y) >= Y because [14], by (Select) 14] Y >= Y by (Meta) 15] D*(!facplus(X, Y)) >= Y because [16], by (Select) 16] !facplus(X, Y) >= Y because [13], by (Star) 17] D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) because [18], by (Star) 18] D*(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) because D > !facplus, [19] and [30], by (Copy) 19] D*(!factimes(X, Y)) >= !factimes(Y, D(X)) because D > !factimes, [20] and [24], by (Copy) 20] D*(!factimes(X, Y)) >= Y because [21], by (Select) 21] !factimes(X, Y) >= Y because [22], by (Star) 22] !factimes*(X, Y) >= Y because [23], by (Select) 23] Y >= Y by (Meta) 24] D*(!factimes(X, Y)) >= D(X) because [25], [28] and [25], by (Stat) 25] !factimes(X, Y) > X because [26], by definition 26] !factimes*(X, Y) >= X because [27], by (Select) 27] X >= X by (Meta) 28] D*(!factimes(X, Y)) >= X because [29], by (Select) 29] !factimes(X, Y) >= X because [26], by (Star) 30] D*(!factimes(X, Y)) >= !factimes(X, D(Y)) because D > !factimes, [28] and [31], by (Copy) 31] D*(!factimes(X, Y)) >= D(Y) because [32], [20] and [32], by (Stat) 32] !factimes(X, Y) > Y because [33], by definition 33] !factimes*(X, Y) >= Y because [23], by (Select) 34] D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) because [35], by (Star) 35] D*(!facminus(X, Y)) >= !facminus(D(X), D(Y)) because D > !facminus, [36] and [42], by (Copy) 36] D*(!facminus(X, Y)) >= D(X) because [37], [40] and [37], by (Stat) 37] !facminus(X, Y) > X because [38], by definition 38] !facminus*(X, Y) >= X because [39], by (Select) 39] X >= X by (Meta) 40] D*(!facminus(X, Y)) >= X because [41], by (Select) 41] !facminus(X, Y) >= X because [38], by (Star) 42] D*(!facminus(X, Y)) >= D(Y) because [43], [46] and [43], by (Stat) 43] !facminus(X, Y) > Y because [44], by definition 44] !facminus*(X, Y) >= Y because [45], by (Select) 45] Y >= Y by (Meta) 46] D*(!facminus(X, Y)) >= Y because [47], by (Select) 47] !facminus(X, Y) >= Y because [44], by (Star) 48] D(X) >= D(X) because [49], by (Fun) 49] X >= X by (Meta) 50] D(div(X, Y)) >= !facminus(div D(X) Y, div) because [51], by (Star) 51] D*(div(X, Y)) >= !facminus(div D(X) Y, div) because D > !facminus, [52] and [63], by (Copy) 52] D*(div(X, Y)) >= div(D(X), Y) because D > div, [53] and [59], by (Copy) 53] D*(div(X, Y)) >= D(X) because [54], [57] and [54], by (Stat) 54] div(X, Y) > X because [55], by definition 55] div*(X, Y) >= X because [56], by (Select) 56] X >= X by (Meta) 57] D*(div(X, Y)) >= X because [58], by (Select) 58] div(X, Y) >= X because [55], by (Star) 59] D*(div(X, Y)) >= Y because [60], by (Select) 60] div(X, Y) >= Y because [61], by (Star) 61] div*(X, Y) >= Y because [62], by (Select) 62] Y >= Y by (Meta) 63] D*(div(X, Y)) >= div(!factimes(X, D(Y)), pow(Y, _|_)) because D > div, [64] and [68], by (Copy) 64] D*(div(X, Y)) >= !factimes(X, D(Y)) because D > !factimes, [57] and [65], by (Copy) 65] D*(div(X, Y)) >= D(Y) because [66], [59] and [66], by (Stat) 66] div(X, Y) > Y because [67], by definition 67] div*(X, Y) >= Y because [62], by (Select) 68] D*(div(X, Y)) >= pow(Y, _|_) because [69], by (Select) 69] div(X, Y) >= pow(Y, _|_) because [70], by (Star) 70] div*(X, Y) >= pow(Y, _|_) because div > pow, [67] and [71], by (Copy) 71] div*(X, Y) >= _|_ by (Bot) 72] D(ln(X)) >= div(D(X), X) because [73], by (Star) 73] D*(ln(X)) >= div(D(X), X) because D > div, [74] and [78], by (Copy) 74] D*(ln(X)) >= D(X) because [75] and [78], by (Stat) 75] ln(X) > X because [76], by definition 76] ln*(X) >= X because [77], by (Select) 77] X >= X by (Meta) 78] D*(ln(X)) >= X because [79], by (Select) 79] ln(X) >= X because [76], by (Star) 80] D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow X !facminus(Y, _|_)), D(X)), !factimes(!factimes(pow, ln(X)), D(Y))) because [81], by (Star) 81] D*(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow X !facminus(Y, _|_)), D(X)), !factimes(!factimes(pow, ln(X)), D(Y))) because D > !facplus, [82] and [98], by (Copy) 82] D*(pow(X, Y)) >= !factimes(!factimes(Y, pow(X, !facminus(Y, _|_))), D(X)) because D > !factimes, [83] and [95], by (Copy) 83] D*(pow(X, Y)) >= !factimes(Y, pow(X, !facminus(Y, _|_))) because D > !factimes, [84] and [88], by (Copy) 84] D*(pow(X, Y)) >= Y because [85], by (Select) 85] pow(X, Y) >= Y because [86], by (Star) 86] pow*(X, Y) >= Y because [87], by (Select) 87] Y >= Y by (Meta) 88] D*(pow(X, Y)) >= pow(X, !facminus(Y, _|_)) because D > pow, [89] and [93], by (Copy) 89] D*(pow(X, Y)) >= X because [90], by (Select) 90] pow(X, Y) >= X because [91], by (Star) 91] pow*(X, Y) >= X because [92], by (Select) 92] X >= X by (Meta) 93] D*(pow(X, Y)) >= !facminus(Y, _|_) because D > !facminus, [84] and [94], by (Copy) 94] D*(pow(X, Y)) >= _|_ by (Bot) 95] D*(pow(X, Y)) >= D(X) because [96], [89] and [96], by (Stat) 96] pow(X, Y) > X because [97], by definition 97] pow*(X, Y) >= X because [92], by (Select) 98] D*(pow(X, Y)) >= !factimes(!factimes(pow(X, Y), ln(X)), D(Y)) because D > !factimes, [99] and [105], by (Copy) 99] D*(pow(X, Y)) >= !factimes(pow(X, Y), ln(X)) because D > !factimes, [100] and [104], by (Copy) 100] D*(pow(X, Y)) >= pow(X, Y) because [101], by (Select) 101] pow(X, Y) >= pow(X, Y) because [102] and [103], by (Fun) 102] X >= X by (Meta) 103] Y >= Y by (Meta) 104] D*(pow(X, Y)) >= ln(X) because D > ln and [89], by (Copy) 105] D*(pow(X, Y)) >= D(Y) because [106], [84] and [106], by (Stat) 106] pow(X, Y) > Y because [107], by definition 107] pow*(X, Y) >= Y because [103], by (Select) 108] map(F, cons(X, Y)) > cons(@_{o -> o}(F, X), map(F, Y)) because [109], by definition 109] map*(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) because map > cons, [110] and [117], by (Copy) 110] map*(F, cons(X, Y)) >= @_{o -> o}(F, X) because map > @_{o -> o}, [111] and [113], by (Copy) 111] map*(F, cons(X, Y)) >= F because [112], by (Select) 112] F >= F by (Meta) 113] map*(F, cons(X, Y)) >= X because [114], by (Select) 114] cons(X, Y) >= X because [115], by (Star) 115] cons*(X, Y) >= X because [116], by (Select) 116] X >= X by (Meta) 117] map*(F, cons(X, Y)) >= map(F, Y) because map in Mul, [118] and [119], by (Stat) 118] F >= F by (Meta) 119] cons(X, Y) > Y because [120], by definition 120] cons*(X, Y) >= Y because [121], by (Select) 121] Y >= Y by (Meta) We can thus remove the following rules: D(constant) => 0 map(F, cons(X, Y)) => cons(F X, map(F, Y)) We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): D(!facplus(X, Y)) >? !facplus(D(X), D(Y)) D(!factimes(X, Y)) >? !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X, Y)) >? !facminus(D(X), D(Y)) D(minus(X)) >? minus(D(X)) D(div(X, Y)) >? !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) D(ln(X)) >? div(D(X), X) D(pow(X, Y)) >? !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[!facminus(x_1, x_2)]] = !facminus(x_2, x_1) [[!factimes(x_1, x_2)]] = !factimes(x_2, x_1) [[1]] = _|_ [[2]] = _|_ [[div(x_1, x_2)]] = div(x_2, x_1) [[minus(x_1)]] = x_1 We choose Lex = {!facminus, !facplus, !factimes, D, div, ln, pow} and Mul = {}, and the following precedence: D = ln = pow > !facplus > div > !facminus > !factimes Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) D(!factimes(X, Y)) > !facplus(!factimes, !factimes X D(Y)) D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) D(X) >= D(X) D(div(X, Y)) >= !facminus(div D(X) Y, div) D(ln(X)) >= div(D(X), X) D(pow(X, Y)) >= !facplus(!factimes, !factimes (!factimes pow(X, Y) ln(X)) D(Y)) With these choices, we have: 1] D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) because [2], by (Star) 2] D*(!facplus(X, Y)) >= !facplus(D(X), D(Y)) because D > !facplus, [3] and [9], by (Copy) 3] D*(!facplus(X, Y)) >= D(X) because [4], [7] and [4], by (Stat) 4] !facplus(X, Y) > X because [5], by definition 5] !facplus*(X, Y) >= X because [6], by (Select) 6] X >= X by (Meta) 7] D*(!facplus(X, Y)) >= X because [8], by (Select) 8] !facplus(X, Y) >= X because [5], by (Star) 9] D*(!facplus(X, Y)) >= D(Y) because [10], [13] and [10], by (Stat) 10] !facplus(X, Y) > Y because [11], by definition 11] !facplus*(X, Y) >= Y because [12], by (Select) 12] Y >= Y by (Meta) 13] D*(!facplus(X, Y)) >= Y because [14], by (Select) 14] !facplus(X, Y) >= Y because [11], by (Star) 15] D(!factimes(X, Y)) > !facplus(!factimes, !factimes X D(Y)) because [16], by definition 16] D*(!factimes(X, Y)) >= !facplus(!factimes, !factimes X D(Y)) because D > !facplus, [17] and [28], by (Copy) 17] D*(!factimes(X, Y)) >= !factimes(Y, D(X)) because D > !factimes, [18] and [22], by (Copy) 18] D*(!factimes(X, Y)) >= Y because [19], by (Select) 19] !factimes(X, Y) >= Y because [20], by (Star) 20] !factimes*(X, Y) >= Y because [21], by (Select) 21] Y >= Y by (Meta) 22] D*(!factimes(X, Y)) >= D(X) because [23], [26] and [23], by (Stat) 23] !factimes(X, Y) > X because [24], by definition 24] !factimes*(X, Y) >= X because [25], by (Select) 25] X >= X by (Meta) 26] D*(!factimes(X, Y)) >= X because [27], by (Select) 27] !factimes(X, Y) >= X because [24], by (Star) 28] D*(!factimes(X, Y)) >= !factimes(X, D(Y)) because D > !factimes, [26] and [29], by (Copy) 29] D*(!factimes(X, Y)) >= D(Y) because [30], [18] and [30], by (Stat) 30] !factimes(X, Y) > Y because [31], by definition 31] !factimes*(X, Y) >= Y because [21], by (Select) 32] D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) because [33], by (Star) 33] D*(!facminus(X, Y)) >= !facminus(D(X), D(Y)) because D > !facminus, [34] and [40], by (Copy) 34] D*(!facminus(X, Y)) >= D(X) because [35], [38] and [35], by (Stat) 35] !facminus(X, Y) > X because [36], by definition 36] !facminus*(X, Y) >= X because [37], by (Select) 37] X >= X by (Meta) 38] D*(!facminus(X, Y)) >= X because [39], by (Select) 39] !facminus(X, Y) >= X because [36], by (Star) 40] D*(!facminus(X, Y)) >= D(Y) because [41], [44] and [41], by (Stat) 41] !facminus(X, Y) > Y because [42], by definition 42] !facminus*(X, Y) >= Y because [43], by (Select) 43] Y >= Y by (Meta) 44] D*(!facminus(X, Y)) >= Y because [45], by (Select) 45] !facminus(X, Y) >= Y because [42], by (Star) 46] D(X) >= D(X) because [47], by (Fun) 47] X >= X by (Meta) 48] D(div(X, Y)) >= !facminus(div D(X) Y, div) because [49], by (Star) 49] D*(div(X, Y)) >= !facminus(div D(X) Y, div) because D > !facminus, [50] and [61], by (Copy) 50] D*(div(X, Y)) >= div(D(X), Y) because D > div, [51] and [57], by (Copy) 51] D*(div(X, Y)) >= D(X) because [52], [55] and [52], by (Stat) 52] div(X, Y) > X because [53], by definition 53] div*(X, Y) >= X because [54], by (Select) 54] X >= X by (Meta) 55] D*(div(X, Y)) >= X because [56], by (Select) 56] div(X, Y) >= X because [53], by (Star) 57] D*(div(X, Y)) >= Y because [58], by (Select) 58] div(X, Y) >= Y because [59], by (Star) 59] div*(X, Y) >= Y because [60], by (Select) 60] Y >= Y by (Meta) 61] D*(div(X, Y)) >= div(!factimes(X, D(Y)), pow(Y, _|_)) because D > div, [62] and [66], by (Copy) 62] D*(div(X, Y)) >= !factimes(X, D(Y)) because D > !factimes, [55] and [63], by (Copy) 63] D*(div(X, Y)) >= D(Y) because [64], [57] and [64], by (Stat) 64] div(X, Y) > Y because [65], by definition 65] div*(X, Y) >= Y because [60], by (Select) 66] D*(div(X, Y)) >= pow(Y, _|_) because D = pow, [64], [57], [67], [64] and [68], by (Stat) 67] D*(div(X, Y)) >= _|_ by (Bot) 68] div(X, Y) > _|_ because [69], by definition 69] div*(X, Y) >= _|_ by (Bot) 70] D(ln(X)) >= div(D(X), X) because [71], by (Star) 71] D*(ln(X)) >= div(D(X), X) because D > div, [72] and [75], by (Copy) 72] D*(ln(X)) >= D(X) because [73], by (Select) 73] ln(X) >= D(X) because ln = D and [74], by (Fun) 74] X >= X by (Meta) 75] D*(ln(X)) >= X because [76], by (Select) 76] ln(X) >= X because [77], by (Star) 77] ln*(X) >= X because [74], by (Select) 78] D(pow(X, Y)) >= !facplus(!factimes, !factimes (!factimes pow(X, Y) ln(X)) D(Y)) because [79], by (Star) 79] D*(pow(X, Y)) >= !facplus(!factimes, !factimes (!factimes pow(X, Y) ln(X)) D(Y)) because D > !facplus, [80] and [98], by (Copy) 80] D*(pow(X, Y)) >= !factimes(!factimes(Y, pow(X, !facminus(Y, _|_))), D(X)) because D > !factimes, [81] and [94], by (Copy) 81] D*(pow(X, Y)) >= !factimes(Y, pow(X, !facminus(Y, _|_))) because D > !factimes, [82] and [86], by (Copy) 82] D*(pow(X, Y)) >= Y because [83], by (Select) 83] pow(X, Y) >= Y because [84], by (Star) 84] pow*(X, Y) >= Y because [85], by (Select) 85] Y >= Y by (Meta) 86] D*(pow(X, Y)) >= pow(X, !facminus(Y, _|_)) because D = pow, [87], [90] and [92], by (Stat) 87] pow(X, Y) > X because [88], by definition 88] pow*(X, Y) >= X because [89], by (Select) 89] X >= X by (Meta) 90] D*(pow(X, Y)) >= X because [91], by (Select) 91] pow(X, Y) >= X because [88], by (Star) 92] D*(pow(X, Y)) >= !facminus(Y, _|_) because D > !facminus, [82] and [93], by (Copy) 93] D*(pow(X, Y)) >= _|_ by (Bot) 94] D*(pow(X, Y)) >= D(X) because [95], by (Select) 95] pow(X, Y) >= D(X) because [96], by (Star) 96] pow*(X, Y) >= D(X) because pow = D, [97], [88] and [97], by (Stat) 97] X >= X by (Meta) 98] D*(pow(X, Y)) >= !factimes(!factimes(pow(X, Y), ln(X)), D(Y)) because D > !factimes, [99] and [106], by (Copy) 99] D*(pow(X, Y)) >= !factimes(pow(X, Y), ln(X)) because D > !factimes, [100] and [103], by (Copy) 100] D*(pow(X, Y)) >= pow(X, Y) because [101], by (Select) 101] pow(X, Y) >= pow(X, Y) because [97] and [102], by (Fun) 102] Y >= Y by (Meta) 103] D*(pow(X, Y)) >= ln(X) because [104], by (Select) 104] pow(X, Y) >= ln(X) because [105], by (Star) 105] pow*(X, Y) >= ln(X) because pow = ln, [97], [88] and [97], by (Stat) 106] D*(pow(X, Y)) >= D(Y) because [107], [82] and [107], by (Stat) 107] pow(X, Y) > Y because [108], by definition 108] pow*(X, Y) >= Y because [102], by (Select) We can thus remove the following rules: D(!factimes(X, Y)) => !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): D(!facplus(X, Y)) >? !facplus(D(X), D(Y)) D(!facminus(X, Y)) >? !facminus(D(X), D(Y)) D(minus(X)) >? minus(D(X)) D(div(X, Y)) >? !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) D(ln(X)) >? div(D(X), X) D(pow(X, Y)) >? !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[!facminus(x_1, x_2)]] = !facminus(x_2, x_1) [[!factimes(x_1, x_2)]] = !factimes(x_2, x_1) [[1]] = _|_ [[2]] = _|_ [[div(x_1, x_2)]] = div(x_2, x_1) [[minus(x_1)]] = x_1 We choose Lex = {!facminus, !facplus, !factimes, D, div, pow} and Mul = {ln}, and the following precedence: D = div > ln > !facminus > !factimes = pow > !facplus Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) D(X) >= D(X) D(div(X, Y)) >= !facminus(div D(X) Y, div) D(ln(X)) > div(D(X), X) D(pow(X, Y)) >= !facplus(!factimes, !factimes (!factimes pow(X, Y) ln(X)) D(Y)) With these choices, we have: 1] D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) because [2], by (Star) 2] D*(!facplus(X, Y)) >= !facplus(D(X), D(Y)) because D > !facplus, [3] and [9], by (Copy) 3] D*(!facplus(X, Y)) >= D(X) because [4], [7] and [4], by (Stat) 4] !facplus(X, Y) > X because [5], by definition 5] !facplus*(X, Y) >= X because [6], by (Select) 6] X >= X by (Meta) 7] D*(!facplus(X, Y)) >= X because [8], by (Select) 8] !facplus(X, Y) >= X because [5], by (Star) 9] D*(!facplus(X, Y)) >= D(Y) because [10], [13] and [10], by (Stat) 10] !facplus(X, Y) > Y because [11], by definition 11] !facplus*(X, Y) >= Y because [12], by (Select) 12] Y >= Y by (Meta) 13] D*(!facplus(X, Y)) >= Y because [14], by (Select) 14] !facplus(X, Y) >= Y because [11], by (Star) 15] D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) because [16], by (Star) 16] D*(!facminus(X, Y)) >= !facminus(D(X), D(Y)) because D > !facminus, [17] and [23], by (Copy) 17] D*(!facminus(X, Y)) >= D(X) because [18], [21] and [18], by (Stat) 18] !facminus(X, Y) > X because [19], by definition 19] !facminus*(X, Y) >= X because [20], by (Select) 20] X >= X by (Meta) 21] D*(!facminus(X, Y)) >= X because [22], by (Select) 22] !facminus(X, Y) >= X because [19], by (Star) 23] D*(!facminus(X, Y)) >= D(Y) because [24], [27] and [24], by (Stat) 24] !facminus(X, Y) > Y because [25], by definition 25] !facminus*(X, Y) >= Y because [26], by (Select) 26] Y >= Y by (Meta) 27] D*(!facminus(X, Y)) >= Y because [28], by (Select) 28] !facminus(X, Y) >= Y because [25], by (Star) 29] D(X) >= D(X) because [30], by (Fun) 30] X >= X by (Meta) 31] D(div(X, Y)) >= !facminus(div D(X) Y, div) because [32], by (Star) 32] D*(div(X, Y)) >= !facminus(div D(X) Y, div) because D > !facminus, [33] and [45], by (Copy) 33] D*(div(X, Y)) >= div(D(X), Y) because D = div, [34], [37] and [43], by (Stat) 34] div(X, Y) > Y because [35], by definition 35] div*(X, Y) >= Y because [36], by (Select) 36] Y >= Y by (Meta) 37] D*(div(X, Y)) >= D(X) because [38], [41] and [38], by (Stat) 38] div(X, Y) > X because [39], by definition 39] div*(X, Y) >= X because [40], by (Select) 40] X >= X by (Meta) 41] D*(div(X, Y)) >= X because [42], by (Select) 42] div(X, Y) >= X because [39], by (Star) 43] D*(div(X, Y)) >= Y because [44], by (Select) 44] div(X, Y) >= Y because [35], by (Star) 45] D*(div(X, Y)) >= div(!factimes(X, D(Y)), pow(Y, _|_)) because D = div, [46], [49] and [51], by (Stat) 46] div(X, Y) > pow(Y, _|_) because [47], by definition 47] div*(X, Y) >= pow(Y, _|_) because div > pow, [35] and [48], by (Copy) 48] div*(X, Y) >= _|_ by (Bot) 49] D*(div(X, Y)) >= !factimes(X, D(Y)) because D > !factimes, [41] and [50], by (Copy) 50] D*(div(X, Y)) >= D(Y) because [34], [43] and [34], by (Stat) 51] D*(div(X, Y)) >= pow(Y, _|_) because D > pow, [43] and [52], by (Copy) 52] D*(div(X, Y)) >= _|_ by (Bot) 53] D(ln(X)) > div(D(X), X) because [54], by definition 54] D*(ln(X)) >= div(D(X), X) because D = div, [55], [58] and [59], by (Stat) 55] ln(X) > X because [56], by definition 56] ln*(X) >= X because [57], by (Select) 57] X >= X by (Meta) 58] D*(ln(X)) >= D(X) because [55] and [59], by (Stat) 59] D*(ln(X)) >= X because [60], by (Select) 60] ln(X) >= X because [56], by (Star) 61] D(pow(X, Y)) >= !facplus(!factimes, !factimes (!factimes pow(X, Y) ln(X)) D(Y)) because [62], by (Star) 62] D*(pow(X, Y)) >= !facplus(!factimes, !factimes (!factimes pow(X, Y) ln(X)) D(Y)) because D > !facplus, [63] and [79], by (Copy) 63] D*(pow(X, Y)) >= !factimes(!factimes(Y, pow(X, !facminus(Y, _|_))), D(X)) because D > !factimes, [64] and [76], by (Copy) 64] D*(pow(X, Y)) >= !factimes(Y, pow(X, !facminus(Y, _|_))) because D > !factimes, [65] and [69], by (Copy) 65] D*(pow(X, Y)) >= Y because [66], by (Select) 66] pow(X, Y) >= Y because [67], by (Star) 67] pow*(X, Y) >= Y because [68], by (Select) 68] Y >= Y by (Meta) 69] D*(pow(X, Y)) >= pow(X, !facminus(Y, _|_)) because D > pow, [70] and [74], by (Copy) 70] D*(pow(X, Y)) >= X because [71], by (Select) 71] pow(X, Y) >= X because [72], by (Star) 72] pow*(X, Y) >= X because [73], by (Select) 73] X >= X by (Meta) 74] D*(pow(X, Y)) >= !facminus(Y, _|_) because D > !facminus, [65] and [75], by (Copy) 75] D*(pow(X, Y)) >= _|_ by (Bot) 76] D*(pow(X, Y)) >= D(X) because [77], [70] and [77], by (Stat) 77] pow(X, Y) > X because [78], by definition 78] pow*(X, Y) >= X because [73], by (Select) 79] D*(pow(X, Y)) >= !factimes(!factimes(pow(X, Y), ln(X)), D(Y)) because D > !factimes, [80] and [86], by (Copy) 80] D*(pow(X, Y)) >= !factimes(pow(X, Y), ln(X)) because D > !factimes, [81] and [85], by (Copy) 81] D*(pow(X, Y)) >= pow(X, Y) because [82], by (Select) 82] pow(X, Y) >= pow(X, Y) because [83] and [84], by (Fun) 83] X >= X by (Meta) 84] Y >= Y by (Meta) 85] D*(pow(X, Y)) >= ln(X) because D > ln and [70], by (Copy) 86] D*(pow(X, Y)) >= D(Y) because [87], [65] and [87], by (Stat) 87] pow(X, Y) > Y because [88], by definition 88] pow*(X, Y) >= Y because [84], by (Select) We can thus remove the following rules: D(ln(X)) => div(D(X), X) We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): D(!facplus(X, Y)) >? !facplus(D(X), D(Y)) D(!facminus(X, Y)) >? !facminus(D(X), D(Y)) D(minus(X)) >? minus(D(X)) D(div(X, Y)) >? !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) D(pow(X, Y)) >? !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[!facminus(x_1, x_2)]] = !facminus(x_2, x_1) [[1]] = _|_ [[2]] = _|_ [[div(x_1, x_2)]] = div(x_2, x_1) [[ln(x_1)]] = x_1 [[minus(x_1)]] = x_1 [[pow(x_1, x_2)]] = pow(x_2, x_1) We choose Lex = {!facminus, !facplus, !factimes, D, div, pow} and Mul = {}, and the following precedence: D > !facminus = div > !facplus = !factimes = pow Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: D(!facplus(X, Y)) > !facplus(D(X), D(Y)) D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) D(X) >= D(X) D(div(X, Y)) >= !facminus(div D(X) Y, div) D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow), D(X)), !factimes(!factimes(pow X Y, X), D(Y))) With these choices, we have: 1] D(!facplus(X, Y)) > !facplus(D(X), D(Y)) because [2], by definition 2] D*(!facplus(X, Y)) >= !facplus(D(X), D(Y)) because D > !facplus, [3] and [9], by (Copy) 3] D*(!facplus(X, Y)) >= D(X) because [4], [7] and [4], by (Stat) 4] !facplus(X, Y) > X because [5], by definition 5] !facplus*(X, Y) >= X because [6], by (Select) 6] X >= X by (Meta) 7] D*(!facplus(X, Y)) >= X because [8], by (Select) 8] !facplus(X, Y) >= X because [5], by (Star) 9] D*(!facplus(X, Y)) >= D(Y) because [10], [13] and [10], by (Stat) 10] !facplus(X, Y) > Y because [11], by definition 11] !facplus*(X, Y) >= Y because [12], by (Select) 12] Y >= Y by (Meta) 13] D*(!facplus(X, Y)) >= Y because [14], by (Select) 14] !facplus(X, Y) >= Y because [11], by (Star) 15] D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) because [16], by (Star) 16] D*(!facminus(X, Y)) >= !facminus(D(X), D(Y)) because D > !facminus, [17] and [23], by (Copy) 17] D*(!facminus(X, Y)) >= D(X) because [18], [21] and [18], by (Stat) 18] !facminus(X, Y) > X because [19], by definition 19] !facminus*(X, Y) >= X because [20], by (Select) 20] X >= X by (Meta) 21] D*(!facminus(X, Y)) >= X because [22], by (Select) 22] !facminus(X, Y) >= X because [19], by (Star) 23] D*(!facminus(X, Y)) >= D(Y) because [24], [27] and [24], by (Stat) 24] !facminus(X, Y) > Y because [25], by definition 25] !facminus*(X, Y) >= Y because [26], by (Select) 26] Y >= Y by (Meta) 27] D*(!facminus(X, Y)) >= Y because [28], by (Select) 28] !facminus(X, Y) >= Y because [25], by (Star) 29] D(X) >= D(X) because [30], by (Fun) 30] X >= X by (Meta) 31] D(div(X, Y)) >= !facminus(div D(X) Y, div) because [32], by (Star) 32] D*(div(X, Y)) >= !facminus(div D(X) Y, div) because D > !facminus, [33] and [44], by (Copy) 33] D*(div(X, Y)) >= div(D(X), Y) because D > div, [34] and [40], by (Copy) 34] D*(div(X, Y)) >= D(X) because [35], [38] and [35], by (Stat) 35] div(X, Y) > X because [36], by definition 36] div*(X, Y) >= X because [37], by (Select) 37] X >= X by (Meta) 38] D*(div(X, Y)) >= X because [39], by (Select) 39] div(X, Y) >= X because [36], by (Star) 40] D*(div(X, Y)) >= Y because [41], by (Select) 41] div(X, Y) >= Y because [42], by (Star) 42] div*(X, Y) >= Y because [43], by (Select) 43] Y >= Y by (Meta) 44] D*(div(X, Y)) >= div(!factimes(X, D(Y)), pow(Y, _|_)) because D > div, [45] and [49], by (Copy) 45] D*(div(X, Y)) >= !factimes(X, D(Y)) because D > !factimes, [38] and [46], by (Copy) 46] D*(div(X, Y)) >= D(Y) because [47], [40] and [47], by (Stat) 47] div(X, Y) > Y because [48], by definition 48] div*(X, Y) >= Y because [43], by (Select) 49] D*(div(X, Y)) >= pow(Y, _|_) because D > pow, [40] and [50], by (Copy) 50] D*(div(X, Y)) >= _|_ by (Bot) 51] D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow), D(X)), !factimes(!factimes(pow X Y, X), D(Y))) because [52], by (Star) 52] D*(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow), D(X)), !factimes(!factimes(pow X Y, X), D(Y))) because D > !facplus, [53] and [69], by (Copy) 53] D*(pow(X, Y)) >= !factimes(!factimes(Y, pow(X, !facminus(Y, _|_))), D(X)) because D > !factimes, [54] and [66], by (Copy) 54] D*(pow(X, Y)) >= !factimes(Y, pow(X, !facminus(Y, _|_))) because D > !factimes, [55] and [59], by (Copy) 55] D*(pow(X, Y)) >= Y because [56], by (Select) 56] pow(X, Y) >= Y because [57], by (Star) 57] pow*(X, Y) >= Y because [58], by (Select) 58] Y >= Y by (Meta) 59] D*(pow(X, Y)) >= pow(X, !facminus(Y, _|_)) because D > pow, [60] and [64], by (Copy) 60] D*(pow(X, Y)) >= X because [61], by (Select) 61] pow(X, Y) >= X because [62], by (Star) 62] pow*(X, Y) >= X because [63], by (Select) 63] X >= X by (Meta) 64] D*(pow(X, Y)) >= !facminus(Y, _|_) because D > !facminus, [55] and [65], by (Copy) 65] D*(pow(X, Y)) >= _|_ by (Bot) 66] D*(pow(X, Y)) >= D(X) because [67], [60] and [67], by (Stat) 67] pow(X, Y) > X because [68], by definition 68] pow*(X, Y) >= X because [63], by (Select) 69] D*(pow(X, Y)) >= !factimes(!factimes(pow(X, Y), X), D(Y)) because D > !factimes, [70] and [76], by (Copy) 70] D*(pow(X, Y)) >= !factimes(pow(X, Y), X) because D > !factimes, [71] and [75], by (Copy) 71] D*(pow(X, Y)) >= pow(X, Y) because [72], by (Select) 72] pow(X, Y) >= pow(X, Y) because [73] and [74], by (Fun) 73] X >= X by (Meta) 74] Y >= Y by (Meta) 75] D*(pow(X, Y)) >= X because [61], by (Select) 76] D*(pow(X, Y)) >= D(Y) because [77], [55] and [77], by (Stat) 77] pow(X, Y) > Y because [78], by definition 78] pow*(X, Y) >= Y because [74], by (Select) We can thus remove the following rules: D(!facplus(X, Y)) => !facplus(D(X), D(Y)) We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): D(!facminus(X, Y)) >? !facminus(D(X), D(Y)) D(minus(X)) >? minus(D(X)) D(div(X, Y)) >? !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) D(pow(X, Y)) >? !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[1]] = _|_ [[2]] = _|_ [[div(x_1, x_2)]] = div(x_2, x_1) [[ln(x_1)]] = x_1 [[minus(x_1)]] = x_1 We choose Lex = {!facminus, !facplus, !factimes, D, div, pow} and Mul = {}, and the following precedence: D > !facminus = div > !facplus = !factimes = pow Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) D(X) >= D(X) D(div(X, Y)) >= !facminus(div, div !factimes(X, D(Y)) pow(Y, _|_)) D(pow(X, Y)) > !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, _|_))), D(X)), !factimes(!factimes(pow(X, Y), X), D(Y))) With these choices, we have: 1] D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) because [2], by (Star) 2] D*(!facminus(X, Y)) >= !facminus(D(X), D(Y)) because D > !facminus, [3] and [9], by (Copy) 3] D*(!facminus(X, Y)) >= D(X) because [4], [7] and [4], by (Stat) 4] !facminus(X, Y) > X because [5], by definition 5] !facminus*(X, Y) >= X because [6], by (Select) 6] X >= X by (Meta) 7] D*(!facminus(X, Y)) >= X because [8], by (Select) 8] !facminus(X, Y) >= X because [5], by (Star) 9] D*(!facminus(X, Y)) >= D(Y) because [10], [13] and [10], by (Stat) 10] !facminus(X, Y) > Y because [11], by definition 11] !facminus*(X, Y) >= Y because [12], by (Select) 12] Y >= Y by (Meta) 13] D*(!facminus(X, Y)) >= Y because [14], by (Select) 14] !facminus(X, Y) >= Y because [11], by (Star) 15] D(X) >= D(X) because [16], by (Fun) 16] X >= X by (Meta) 17] D(div(X, Y)) >= !facminus(div, div !factimes(X, D(Y)) pow(Y, _|_)) because [18], by (Star) 18] D*(div(X, Y)) >= !facminus(div, div !factimes(X, D(Y)) pow(Y, _|_)) because D > !facminus, [19] and [30], by (Copy) 19] D*(div(X, Y)) >= div(D(X), Y) because D > div, [20] and [26], by (Copy) 20] D*(div(X, Y)) >= D(X) because [21], [24] and [21], by (Stat) 21] div(X, Y) > X because [22], by definition 22] div*(X, Y) >= X because [23], by (Select) 23] X >= X by (Meta) 24] D*(div(X, Y)) >= X because [25], by (Select) 25] div(X, Y) >= X because [22], by (Star) 26] D*(div(X, Y)) >= Y because [27], by (Select) 27] div(X, Y) >= Y because [28], by (Star) 28] div*(X, Y) >= Y because [29], by (Select) 29] Y >= Y by (Meta) 30] D*(div(X, Y)) >= div(!factimes(X, D(Y)), pow(Y, _|_)) because D > div, [31] and [35], by (Copy) 31] D*(div(X, Y)) >= !factimes(X, D(Y)) because D > !factimes, [24] and [32], by (Copy) 32] D*(div(X, Y)) >= D(Y) because [33], [26] and [33], by (Stat) 33] div(X, Y) > Y because [34], by definition 34] div*(X, Y) >= Y because [29], by (Select) 35] D*(div(X, Y)) >= pow(Y, _|_) because D > pow, [26] and [36], by (Copy) 36] D*(div(X, Y)) >= _|_ by (Bot) 37] D(pow(X, Y)) > !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, _|_))), D(X)), !factimes(!factimes(pow(X, Y), X), D(Y))) because [38], by definition 38] D*(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, _|_))), D(X)), !factimes(!factimes(pow(X, Y), X), D(Y))) because D > !facplus, [39] and [55], by (Copy) 39] D*(pow(X, Y)) >= !factimes(!factimes(Y, pow(X, !facminus(Y, _|_))), D(X)) because D > !factimes, [40] and [52], by (Copy) 40] D*(pow(X, Y)) >= !factimes(Y, pow(X, !facminus(Y, _|_))) because D > !factimes, [41] and [45], by (Copy) 41] D*(pow(X, Y)) >= Y because [42], by (Select) 42] pow(X, Y) >= Y because [43], by (Star) 43] pow*(X, Y) >= Y because [44], by (Select) 44] Y >= Y by (Meta) 45] D*(pow(X, Y)) >= pow(X, !facminus(Y, _|_)) because D > pow, [46] and [50], by (Copy) 46] D*(pow(X, Y)) >= X because [47], by (Select) 47] pow(X, Y) >= X because [48], by (Star) 48] pow*(X, Y) >= X because [49], by (Select) 49] X >= X by (Meta) 50] D*(pow(X, Y)) >= !facminus(Y, _|_) because D > !facminus, [41] and [51], by (Copy) 51] D*(pow(X, Y)) >= _|_ by (Bot) 52] D*(pow(X, Y)) >= D(X) because [53], [46] and [53], by (Stat) 53] pow(X, Y) > X because [54], by definition 54] pow*(X, Y) >= X because [49], by (Select) 55] D*(pow(X, Y)) >= !factimes(!factimes(pow(X, Y), X), D(Y)) because D > !factimes, [56] and [62], by (Copy) 56] D*(pow(X, Y)) >= !factimes(pow(X, Y), X) because D > !factimes, [57] and [61], by (Copy) 57] D*(pow(X, Y)) >= pow(X, Y) because [58], by (Select) 58] pow(X, Y) >= pow(X, Y) because [59] and [60], by (Fun) 59] X >= X by (Meta) 60] Y >= Y by (Meta) 61] D*(pow(X, Y)) >= X because [47], by (Select) 62] D*(pow(X, Y)) >= D(Y) because [63], [41] and [63], by (Stat) 63] pow(X, Y) > Y because [64], by definition 64] pow*(X, Y) >= Y because [60], by (Select) We can thus remove the following rules: D(pow(X, Y)) => !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): D(!facminus(X, Y)) >? !facminus(D(X), D(Y)) D(minus(X)) >? minus(D(X)) D(div(X, Y)) >? !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[2]] = _|_ [[div(x_1, x_2)]] = div(x_2, x_1) [[minus(x_1)]] = x_1 We choose Lex = {!facminus, D, div} and Mul = {!factimes, pow}, and the following precedence: D > !factimes > pow > div > !facminus Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: D(!facminus(X, Y)) > !facminus(D(X), D(Y)) D(X) >= D(X) D(div(X, Y)) > !facminus(div, div !factimes(X, D(Y)) pow(Y, _|_)) With these choices, we have: 1] D(!facminus(X, Y)) > !facminus(D(X), D(Y)) because [2], by definition 2] D*(!facminus(X, Y)) >= !facminus(D(X), D(Y)) because D > !facminus, [3] and [9], by (Copy) 3] D*(!facminus(X, Y)) >= D(X) because [4], [7] and [4], by (Stat) 4] !facminus(X, Y) > X because [5], by definition 5] !facminus*(X, Y) >= X because [6], by (Select) 6] X >= X by (Meta) 7] D*(!facminus(X, Y)) >= X because [8], by (Select) 8] !facminus(X, Y) >= X because [5], by (Star) 9] D*(!facminus(X, Y)) >= D(Y) because [10], [13] and [10], by (Stat) 10] !facminus(X, Y) > Y because [11], by definition 11] !facminus*(X, Y) >= Y because [12], by (Select) 12] Y >= Y by (Meta) 13] D*(!facminus(X, Y)) >= Y because [14], by (Select) 14] !facminus(X, Y) >= Y because [11], by (Star) 15] D(X) >= D(X) because [16], by (Fun) 16] X >= X by (Meta) 17] D(div(X, Y)) > !facminus(div, div !factimes(X, D(Y)) pow(Y, _|_)) because [18], by definition 18] D*(div(X, Y)) >= !facminus(div, div !factimes(X, D(Y)) pow(Y, _|_)) because D > !facminus, [19] and [30], by (Copy) 19] D*(div(X, Y)) >= div(D(X), Y) because D > div, [20] and [26], by (Copy) 20] D*(div(X, Y)) >= D(X) because [21], [24] and [21], by (Stat) 21] div(X, Y) > X because [22], by definition 22] div*(X, Y) >= X because [23], by (Select) 23] X >= X by (Meta) 24] D*(div(X, Y)) >= X because [25], by (Select) 25] div(X, Y) >= X because [22], by (Star) 26] D*(div(X, Y)) >= Y because [27], by (Select) 27] div(X, Y) >= Y because [28], by (Star) 28] div*(X, Y) >= Y because [29], by (Select) 29] Y >= Y by (Meta) 30] D*(div(X, Y)) >= div(!factimes(X, D(Y)), pow(Y, _|_)) because D > div, [31] and [35], by (Copy) 31] D*(div(X, Y)) >= !factimes(X, D(Y)) because D > !factimes, [24] and [32], by (Copy) 32] D*(div(X, Y)) >= D(Y) because [33], [26] and [33], by (Stat) 33] div(X, Y) > Y because [34], by definition 34] div*(X, Y) >= Y because [29], by (Select) 35] D*(div(X, Y)) >= pow(Y, _|_) because D > pow, [26] and [36], by (Copy) 36] D*(div(X, Y)) >= _|_ by (Bot) We can thus remove the following rules: D(!facminus(X, Y)) => !facminus(D(X), D(Y)) D(div(X, Y)) => !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): D(minus(X)) >? minus(D(X)) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: D = Lam[y0].3*y0 minus = Lam[y0].2 + y0 Using this interpretation, the requirements translate to: [[D(minus(_x0))]] = 6 + 3*x0 > 2 + 3*x0 = [[minus(D(_x0))]] We can thus remove the following rules: D(minus(X)) => minus(D(X)) All rules were succesfully removed. Thus, termination of the original system has been reduced to termination of the beta-rule, which is well-known to hold. +++ Citations +++ [Kop12] C. Kop. Higher Order Termination. PhD Thesis, 2012.