We consider the system 433. Alphabet: 0 : [] --> R 1 : [] --> R D : [R -> R * R] --> R add : [R * R] --> R cos : [R] --> R min : [R] --> R mul : [R * R] --> R sin : [R] --> R Rules: D(/\x.X, Y) => 0 D(/\x.x, X) => 1 D(/\x.min(X(x)), Y) => min(D(/\y.X(y), Y)) D(/\x.add(X(x), Y(x)), Z) => add(D(/\y.X(y), Z), D(/\z.Y(z), Z)) D(/\x.mul(X(x), Y(x)), Z) => add(mul(D(/\y.X(y), Z), Y(Z)), mul(X(Z), D(/\z.Y(z), Z))) D(/\x.sin(X(x)), Y) => mul(cos(Y), D(/\y.X(y), Y)) D(/\x.cos(X(x)), Y) => mul(min(sin(Y)), D(/\y.X(y), Y)) We use the dependency pair framework as described in [Kop12, Ch. 6/7], with dynamic dependency pairs. We thus obtain the following dependency pair problem (P_0, R_0, minimal, all): Dependency Pairs P_0: 0] D#(/\x.min(X(x)), Y) =#> D#(/\y.X(y), Y) 1] D#(/\x.min(X(x)), Y) =#> X(y) 2] D#(/\x.add(X(x), Y(x)), Z) =#> D#(/\y.X(y), Z) 3] D#(/\x.add(X(x), Y(x)), Z) =#> X(y) 4] D#(/\x.add(X(x), Y(x)), Z) =#> D#(/\y.Y(y), Z) 5] D#(/\x.add(X(x), Y(x)), Z) =#> Y(y) 6] D#(/\x.mul(X(x), Y(x)), Z) =#> D#(/\y.X(y), Z) 7] D#(/\x.mul(X(x), Y(x)), Z) =#> X(y) 8] D#(/\x.mul(X(x), Y(x)), Z) =#> Y(Z) 9] D#(/\x.mul(X(x), Y(x)), Z) =#> X(Z) 10] D#(/\x.mul(X(x), Y(x)), Z) =#> D#(/\y.Y(y), Z) 11] D#(/\x.mul(X(x), Y(x)), Z) =#> Y(y) 12] D#(/\x.sin(X(x)), Y) =#> D#(/\y.X(y), Y) 13] D#(/\x.sin(X(x)), Y) =#> X(y) 14] D#(/\x.cos(X(x)), Y) =#> D#(/\y.X(y), Y) 15] D#(/\x.cos(X(x)), Y) =#> X(y) Rules R_0: D(/\x.X, Y) => 0 D(/\x.x, X) => 1 D(/\x.min(X(x)), Y) => min(D(/\y.X(y), Y)) D(/\x.add(X(x), Y(x)), Z) => add(D(/\y.X(y), Z), D(/\z.Y(z), Z)) D(/\x.mul(X(x), Y(x)), Z) => add(mul(D(/\y.X(y), Z), Y(Z)), mul(X(Z), D(/\z.Y(z), Z))) D(/\x.sin(X(x)), Y) => mul(cos(Y), D(/\y.X(y), Y)) D(/\x.cos(X(x)), Y) => mul(min(sin(Y)), D(/\y.X(y), Y)) Thus, the original system is terminating if (P_0, R_0, minimal, all) is finite. We consider the dependency pair problem (P_0, R_0, minimal, all). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: D#(/\x.min(X(x)), Y) >? D#(/\y.X(y), Y) D#(/\x.min(X(x)), Y) >? X(~c0) D#(/\x.add(X(x), Y(x)), Z) >? D#(/\y.X(y), Z) D#(/\x.add(X(x), Y(x)), Z) >? X(~c1) D#(/\x.add(X(x), Y(x)), Z) >? D#(/\y.Y(y), Z) D#(/\x.add(X(x), Y(x)), Z) >? Y(~c2) D#(/\x.mul(X(x), Y(x)), Z) >? D#(/\y.X(y), Z) D#(/\x.mul(X(x), Y(x)), Z) >? X(~c3) D#(/\x.mul(X(x), Y(x)), Z) >? Y(Z) D#(/\x.mul(X(x), Y(x)), Z) >? X(Z) D#(/\x.mul(X(x), Y(x)), Z) >? D#(/\y.Y(y), Z) D#(/\x.mul(X(x), Y(x)), Z) >? Y(~c4) D#(/\x.sin(X(x)), Y) >? D#(/\y.X(y), Y) D#(/\x.sin(X(x)), Y) >? X(~c5) D#(/\x.cos(X(x)), Y) >? D#(/\y.X(y), Y) D#(/\x.cos(X(x)), Y) >? X(~c6) D(/\x.X, Y) >= 0 D(/\x.x, X) >= 1 D(/\x.min(X(x)), Y) >= min(D(/\y.X(y), Y)) D(/\x.add(X(x), Y(x)), Z) >= add(D(/\y.X(y), Z), D(/\z.Y(z), Z)) D(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\y.X(y), Z), Y(Z)), mul(X(Z), D(/\z.Y(z), Z))) D(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\y.X(y), Y)) D(/\x.cos(X(x)), Y) >= mul(min(sin(Y)), D(/\y.X(y), Y)) D(F, X) >= D#(F, X) 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]] = _|_ [[1]] = _|_ [[min(x_1)]] = x_1 [[~c0]] = _|_ [[~c1]] = _|_ [[~c2]] = _|_ [[~c3]] = _|_ [[~c4]] = _|_ [[~c5]] = _|_ [[~c6]] = _|_ We choose Lex = {} and Mul = {D, D#, add, cos, mul, sin}, and the following precedence: D > D# > add > cos > mul > sin Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: D#(/\x.X(x), Y) >= D#(/\x.X(x), Y) D#(/\x.X(x), Y) >= X(_|_) D#(/\x.add(X(x), Y(x)), Z) >= D#(/\x.X(x), Z) D#(/\x.add(X(x), Y(x)), Z) > X(_|_) D#(/\x.add(X(x), Y(x)), Z) >= D#(/\x.Y(x), Z) D#(/\x.add(X(x), Y(x)), Z) >= Y(_|_) D#(/\x.mul(X(x), Y(x)), Z) > D#(/\x.X(x), Z) D#(/\x.mul(X(x), Y(x)), Z) > X(_|_) D#(/\x.mul(X(x), Y(x)), Z) >= Y(Z) D#(/\x.mul(X(x), Y(x)), Z) >= X(Z) D#(/\x.mul(X(x), Y(x)), Z) >= D#(/\x.Y(x), Z) D#(/\x.mul(X(x), Y(x)), Z) >= Y(_|_) D#(/\x.sin(X(x)), Y) >= D#(/\x.X(x), Y) D#(/\x.sin(X(x)), Y) > X(_|_) D#(/\x.cos(X(x)), Y) >= D#(/\x.X(x), Y) D#(/\x.cos(X(x)), Y) >= X(_|_) D(/\x.X, Y) >= _|_ D(/\x.x, X) >= _|_ D(/\x.X(x), Y) >= D(/\x.X(x), Y) D(/\x.add(X(x), Y(x)), Z) >= add(D(/\x.X(x), Z), D(/\y.Y(y), Z)) D(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\x.X(x), Z), Y(Z)), mul(X(Z), D(/\y.Y(y), Z))) D(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) D(/\x.cos(X(x)), Y) >= mul(sin(Y), D(/\x.X(x), Y)) D(F, X) >= D#(F, X) With these choices, we have: 1] D#(/\x.X(x), Y) >= D#(/\x.X(x), Y) because D# in Mul, [2] and [5], by (Fun) 2] /\y.X(y) >= /\y.X(y) because [3], by (Abs) 3] X(x) >= X(x) because [4], by (Meta) 4] x >= x by (Var) 5] Y >= Y by (Meta) 6] D#(/\x.X(x), Y) >= X(_|_) because [7], by (Star) 7] D#*(/\x.X(x), Y) >= X(_|_) because [8], by (Select) 8] X(D#*(/\x.X(x), Y)) >= X(_|_) because [9], by (Meta) 9] D#*(/\x.X(x), Y) >= _|_ by (Bot) 10] D#(/\x.add(X(x), Y(x)), Z) >= D#(/\x.X(x), Z) because D# in Mul, [11] and [16], by (Fun) 11] /\y.add(X(y), Y(y)) >= /\y.X(y) because [12], by (Abs) 12] add(X(x), Y(x)) >= X(x) because [13], by (Star) 13] add*(X(x), Y(x)) >= X(x) because [14], by (Select) 14] X(x) >= X(x) because [15], by (Meta) 15] x >= x by (Var) 16] Z >= Z by (Meta) 17] D#(/\x.add(X(x), Y(x)), Z) > X(_|_) because [18], by definition 18] D#*(/\x.add(X(x), Y(x)), Z) >= X(_|_) because [19], by (Select) 19] add(X(D#*(/\x.add(X(x), Y(x)), Z)), Y(D#*(/\y.add(X(y), Y(y)), Z))) >= X(_|_) because [20], by (Star) 20] add*(X(D#*(/\x.add(X(x), Y(x)), Z)), Y(D#*(/\y.add(X(y), Y(y)), Z))) >= X(_|_) because [21], by (Select) 21] X(D#*(/\x.add(X(x), Y(x)), Z)) >= X(_|_) because [22], by (Meta) 22] D#*(/\x.add(X(x), Y(x)), Z) >= _|_ by (Bot) 23] D#(/\x.add(X(x), Y(x)), Z) >= D#(/\x.Y(x), Z) because D# in Mul, [24] and [16], by (Fun) 24] /\y.add(X(y), Y(y)) >= /\y.Y(y) because [25], by (Abs) 25] add(X(x), Y(x)) >= Y(x) because [26], by (Star) 26] add*(X(x), Y(x)) >= Y(x) because [27], by (Select) 27] Y(x) >= Y(x) because [28], by (Meta) 28] x >= x by (Var) 29] D#(/\x.add(X(x), Y(x)), Z) >= Y(_|_) because [30], by (Star) 30] D#*(/\x.add(X(x), Y(x)), Z) >= Y(_|_) because [31], by (Select) 31] add(X(D#*(/\x.add(X(x), Y(x)), Z)), Y(D#*(/\y.add(X(y), Y(y)), Z))) >= Y(_|_) because [32], by (Star) 32] add*(X(D#*(/\x.add(X(x), Y(x)), Z)), Y(D#*(/\y.add(X(y), Y(y)), Z))) >= Y(_|_) because [33], by (Select) 33] Y(D#*(/\x.add(X(x), Y(x)), Z)) >= Y(_|_) because [34], by (Meta) 34] D#*(/\x.add(X(x), Y(x)), Z) >= _|_ by (Bot) 35] D#(/\x.mul(X(x), Y(x)), Z) > D#(/\x.X(x), Z) because [36], by definition 36] D#*(/\x.mul(X(x), Y(x)), Z) >= D#(/\x.X(x), Z) because D# in Mul, [37] and [42], by (Stat) 37] /\x.mul(X(x), Y(x)) > /\x.X(x) because [38], by definition 38] /\y.mul*(X(y), Y(y)) >= /\y.X(y) because [39], by (Abs) 39] mul*(X(x), Y(x)) >= X(x) because [40], by (Select) 40] X(x) >= X(x) because [41], by (Meta) 41] x >= x by (Var) 42] Z >= Z by (Meta) 43] D#(/\x.mul(X(x), Y(x)), Z) > X(_|_) because [44], by definition 44] D#*(/\x.mul(X(x), Y(x)), Z) >= X(_|_) because [45], by (Select) 45] mul(X(D#*(/\x.mul(X(x), Y(x)), Z)), Y(D#*(/\y.mul(X(y), Y(y)), Z))) >= X(_|_) because [46], by (Star) 46] mul*(X(D#*(/\x.mul(X(x), Y(x)), Z)), Y(D#*(/\y.mul(X(y), Y(y)), Z))) >= X(_|_) because [47], by (Select) 47] X(D#*(/\x.mul(X(x), Y(x)), Z)) >= X(_|_) because [48], by (Meta) 48] D#*(/\x.mul(X(x), Y(x)), Z) >= _|_ by (Bot) 49] D#(/\x.mul(X(x), Y(x)), Z) >= Y(Z) because [50], by (Star) 50] D#*(/\x.mul(X(x), Y(x)), Z) >= Y(Z) because [51], by (Select) 51] mul(X(D#*(/\x.mul(X(x), Y(x)), Z)), Y(D#*(/\y.mul(X(y), Y(y)), Z))) >= Y(Z) because [52], by (Star) 52] mul*(X(D#*(/\x.mul(X(x), Y(x)), Z)), Y(D#*(/\y.mul(X(y), Y(y)), Z))) >= Y(Z) because [53], by (Select) 53] Y(D#*(/\x.mul(X(x), Y(x)), Z)) >= Y(Z) because [54], by (Meta) 54] D#*(/\x.mul(X(x), Y(x)), Z) >= Z because [42], by (Select) 55] D#(/\x.mul(X(x), Y(x)), Z) >= X(Z) because [56], by (Star) 56] D#*(/\x.mul(X(x), Y(x)), Z) >= X(Z) because [57], by (Select) 57] mul(X(D#*(/\x.mul(X(x), Y(x)), Z)), Y(D#*(/\y.mul(X(y), Y(y)), Z))) >= X(Z) because [58], by (Star) 58] mul*(X(D#*(/\x.mul(X(x), Y(x)), Z)), Y(D#*(/\y.mul(X(y), Y(y)), Z))) >= X(Z) because [59], by (Select) 59] X(D#*(/\x.mul(X(x), Y(x)), Z)) >= X(Z) because [54], by (Meta) 60] D#(/\x.mul(X(x), Y(x)), Z) >= D#(/\x.Y(x), Z) because D# in Mul, [61] and [42], by (Fun) 61] /\y.mul(X(y), Y(y)) >= /\y.Y(y) because [62], by (Abs) 62] mul(X(x), Y(x)) >= Y(x) because [63], by (Star) 63] mul*(X(x), Y(x)) >= Y(x) because [64], by (Select) 64] Y(x) >= Y(x) because [65], by (Meta) 65] x >= x by (Var) 66] D#(/\x.mul(X(x), Y(x)), Z) >= Y(_|_) because [67], by (Star) 67] D#*(/\x.mul(X(x), Y(x)), Z) >= Y(_|_) because [68], by (Select) 68] mul(X(D#*(/\x.mul(X(x), Y(x)), Z)), Y(D#*(/\y.mul(X(y), Y(y)), Z))) >= Y(_|_) because [69], by (Star) 69] mul*(X(D#*(/\x.mul(X(x), Y(x)), Z)), Y(D#*(/\y.mul(X(y), Y(y)), Z))) >= Y(_|_) because [70], by (Select) 70] Y(D#*(/\x.mul(X(x), Y(x)), Z)) >= Y(_|_) because [71], by (Meta) 71] D#*(/\x.mul(X(x), Y(x)), Z) >= _|_ by (Bot) 72] D#(/\x.sin(X(x)), Y) >= D#(/\x.X(x), Y) because D# in Mul, [73] and [78], by (Fun) 73] /\y.sin(X(y)) >= /\y.X(y) because [74], by (Abs) 74] sin(X(x)) >= X(x) because [75], by (Star) 75] sin*(X(x)) >= X(x) because [76], by (Select) 76] X(x) >= X(x) because [77], by (Meta) 77] x >= x by (Var) 78] Y >= Y by (Meta) 79] D#(/\x.sin(X(x)), Y) > X(_|_) because [80], by definition 80] D#*(/\x.sin(X(x)), Y) >= X(_|_) because [81], by (Select) 81] sin(X(D#*(/\x.sin(X(x)), Y))) >= X(_|_) because [82], by (Star) 82] sin*(X(D#*(/\x.sin(X(x)), Y))) >= X(_|_) because [83], by (Select) 83] X(D#*(/\x.sin(X(x)), Y)) >= X(_|_) because [84], by (Meta) 84] D#*(/\x.sin(X(x)), Y) >= _|_ by (Bot) 85] D#(/\x.cos(X(x)), Y) >= D#(/\x.X(x), Y) because D# in Mul, [86] and [91], by (Fun) 86] /\y.cos(X(y)) >= /\y.X(y) because [87], by (Abs) 87] cos(X(x)) >= X(x) because [88], by (Star) 88] cos*(X(x)) >= X(x) because [89], by (Select) 89] X(x) >= X(x) because [90], by (Meta) 90] x >= x by (Var) 91] Y >= Y by (Meta) 92] D#(/\x.cos(X(x)), Y) >= X(_|_) because [93], by (Star) 93] D#*(/\x.cos(X(x)), Y) >= X(_|_) because [94], by (Select) 94] cos(X(D#*(/\x.cos(X(x)), Y))) >= X(_|_) because [95], by (Star) 95] cos*(X(D#*(/\x.cos(X(x)), Y))) >= X(_|_) because [96], by (Select) 96] X(D#*(/\x.cos(X(x)), Y)) >= X(_|_) because [97], by (Meta) 97] D#*(/\x.cos(X(x)), Y) >= _|_ by (Bot) 98] D(/\x.X, Y) >= _|_ by (Bot) 99] D(/\x.x, X) >= _|_ by (Bot) 100] D(/\x.X(x), Y) >= D(/\x.X(x), Y) because D in Mul, [2] and [5], by (Fun) 101] D(/\x.add(X(x), Y(x)), Z) >= add(D(/\x.X(x), Z), D(/\y.Y(y), Z)) because [102], by (Star) 102] D*(/\x.add(X(x), Y(x)), Z) >= add(D(/\x.X(x), Z), D(/\y.Y(y), Z)) because D > add, [103] and [109], by (Copy) 103] D*(/\x.add(X(x), Y(x)), Z) >= D(/\x.X(x), Z) because D in Mul, [104] and [16], by (Stat) 104] /\x.add(X(x), Y(x)) > /\x.X(x) because [105], by definition 105] /\y.add*(X(y), Y(y)) >= /\y.X(y) because [106], by (Abs) 106] add*(X(x), Y(x)) >= X(x) because [107], by (Select) 107] X(x) >= X(x) because [108], by (Meta) 108] x >= x by (Var) 109] D*(/\y.add(X(y), Y(y)), Z) >= D(/\y.Y(y), Z) because D in Mul, [110] and [16], by (Stat) 110] /\y.add(X(y), Y(y)) > /\y.Y(y) because [111], by definition 111] /\z.add*(X(z), Y(z)) >= /\z.Y(z) because [112], by (Abs) 112] add*(X(y), Y(y)) >= Y(y) because [113], by (Select) 113] Y(y) >= Y(y) because [114], by (Meta) 114] y >= y by (Var) 115] D(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\x.X(x), Z), Y(Z)), mul(X(Z), D(/\y.Y(y), Z))) because [116], by (Star) 116] D*(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\x.X(x), Z), Y(Z)), mul(X(Z), D(/\y.Y(y), Z))) because D > add, [117] and [124], by (Copy) 117] D*(/\x.mul(X(x), Y(x)), Z) >= mul(D(/\x.X(x), Z), Y(Z)) because D > mul, [118] and [119], by (Copy) 118] D*(/\x.mul(X(x), Y(x)), Z) >= D(/\x.X(x), Z) because D in Mul, [37] and [42], by (Stat) 119] D*(/\x.mul(X(x), Y(x)), Z) >= Y(Z) because [120], by (Select) 120] mul(X(D*(/\x.mul(X(x), Y(x)), Z)), Y(D*(/\y.mul(X(y), Y(y)), Z))) >= Y(Z) because [121], by (Star) 121] mul*(X(D*(/\x.mul(X(x), Y(x)), Z)), Y(D*(/\y.mul(X(y), Y(y)), Z))) >= Y(Z) because [122], by (Select) 122] Y(D*(/\x.mul(X(x), Y(x)), Z)) >= Y(Z) because [123], by (Meta) 123] D*(/\x.mul(X(x), Y(x)), Z) >= Z because [42], by (Select) 124] D*(/\x.mul(X(x), Y(x)), Z) >= mul(X(Z), D(/\x.Y(x), Z)) because D > mul, [125] and [129], by (Copy) 125] D*(/\x.mul(X(x), Y(x)), Z) >= X(Z) because [126], by (Select) 126] mul(X(D*(/\x.mul(X(x), Y(x)), Z)), Y(D*(/\y.mul(X(y), Y(y)), Z))) >= X(Z) because [127], by (Star) 127] mul*(X(D*(/\x.mul(X(x), Y(x)), Z)), Y(D*(/\y.mul(X(y), Y(y)), Z))) >= X(Z) because [128], by (Select) 128] X(D*(/\x.mul(X(x), Y(x)), Z)) >= X(Z) because [123], by (Meta) 129] D*(/\x.mul(X(x), Y(x)), Z) >= D(/\x.Y(x), Z) because D in Mul, [130] and [42], by (Stat) 130] /\x.mul(X(x), Y(x)) > /\x.Y(x) because [131], by definition 131] /\y.mul*(X(y), Y(y)) >= /\y.Y(y) because [132], by (Abs) 132] mul*(X(x), Y(x)) >= Y(x) because [133], by (Select) 133] Y(x) >= Y(x) because [134], by (Meta) 134] x >= x by (Var) 135] D(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) because [136], by (Star) 136] D*(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) because D > mul, [137] and [139], by (Copy) 137] D*(/\x.sin(X(x)), Y) >= cos(Y) because D > cos and [138], by (Copy) 138] D*(/\x.sin(X(x)), Y) >= Y because [78], by (Select) 139] D*(/\x.sin(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [140] and [78], by (Stat) 140] /\x.sin(X(x)) > /\x.X(x) because [141], by definition 141] /\y.sin*(X(y)) >= /\y.X(y) because [142], by (Abs) 142] sin*(X(x)) >= X(x) because [143], by (Select) 143] X(x) >= X(x) because [144], by (Meta) 144] x >= x by (Var) 145] D(/\x.cos(X(x)), Y) >= mul(sin(Y), D(/\x.X(x), Y)) because [146], by (Star) 146] D*(/\x.cos(X(x)), Y) >= mul(sin(Y), D(/\x.X(x), Y)) because D > mul, [147] and [149], by (Copy) 147] D*(/\x.cos(X(x)), Y) >= sin(Y) because D > sin and [148], by (Copy) 148] D*(/\x.cos(X(x)), Y) >= Y because [91], by (Select) 149] D*(/\x.cos(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [150] and [91], by (Stat) 150] /\x.cos(X(x)) > /\x.X(x) because [151], by definition 151] /\y.cos*(X(y)) >= /\y.X(y) because [152], by (Abs) 152] cos*(X(x)) >= X(x) because [153], by (Select) 153] X(x) >= X(x) because [154], by (Meta) 154] x >= x by (Var) 155] D(F, X) >= D#(F, X) because [156], by (Star) 156] D*(F, X) >= D#(F, X) because D > D#, [157] and [159], by (Copy) 157] D*(F, X) >= F because [158], by (Select) 158] F >= F by (Meta) 159] D*(F, X) >= X because [160], by (Select) 160] X >= X by (Meta) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_0, R_0, minimal, all) by (P_1, R_0, minimal, all), where P_1 consists of: D#(/\x.min(X(x)), Y) =#> D#(/\y.X(y), Y) D#(/\x.min(X(x)), Y) =#> X(y) D#(/\x.add(X(x), Y(x)), Z) =#> D#(/\y.X(y), Z) D#(/\x.add(X(x), Y(x)), Z) =#> D#(/\y.Y(y), Z) D#(/\x.add(X(x), Y(x)), Z) =#> Y(y) D#(/\x.mul(X(x), Y(x)), Z) =#> Y(Z) D#(/\x.mul(X(x), Y(x)), Z) =#> X(Z) D#(/\x.mul(X(x), Y(x)), Z) =#> D#(/\y.Y(y), Z) D#(/\x.mul(X(x), Y(x)), Z) =#> Y(y) D#(/\x.sin(X(x)), Y) =#> D#(/\y.X(y), Y) D#(/\x.cos(X(x)), Y) =#> D#(/\y.X(y), Y) D#(/\x.cos(X(x)), Y) =#> X(y) Thus, the original system is terminating if (P_1, R_0, minimal, all) is finite. We consider the dependency pair problem (P_1, R_0, minimal, all). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: D#(/\x.min(X(x)), Y) >? D#(/\y.X(y), Y) D#(/\x.min(X(x)), Y) >? X(~c0) D#(/\x.add(X(x), Y(x)), Z) >? D#(/\y.X(y), Z) D#(/\x.add(X(x), Y(x)), Z) >? D#(/\y.Y(y), Z) D#(/\x.add(X(x), Y(x)), Z) >? Y(~c1) D#(/\x.mul(X(x), Y(x)), Z) >? Y(Z) D#(/\x.mul(X(x), Y(x)), Z) >? X(Z) D#(/\x.mul(X(x), Y(x)), Z) >? D#(/\y.Y(y), Z) D#(/\x.mul(X(x), Y(x)), Z) >? Y(~c2) D#(/\x.sin(X(x)), Y) >? D#(/\y.X(y), Y) D#(/\x.cos(X(x)), Y) >? D#(/\y.X(y), Y) D#(/\x.cos(X(x)), Y) >? X(~c3) D(/\x.X, Y) >= 0 D(/\x.x, X) >= 1 D(/\x.min(X(x)), Y) >= min(D(/\y.X(y), Y)) D(/\x.add(X(x), Y(x)), Z) >= add(D(/\y.X(y), Z), D(/\z.Y(z), Z)) D(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\y.X(y), Z), Y(Z)), mul(X(Z), D(/\z.Y(z), Z))) D(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\y.X(y), Y)) D(/\x.cos(X(x)), Y) >= mul(min(sin(Y)), D(/\y.X(y), Y)) D(F, X) >= D#(F, X) 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]] = _|_ [[1]] = _|_ [[min(x_1)]] = x_1 [[~c0]] = _|_ [[~c1]] = _|_ [[~c2]] = _|_ [[~c3]] = _|_ We choose Lex = {} and Mul = {D, D#, add, cos, mul, sin}, and the following precedence: D > D# > add > cos > mul > sin Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: D#(/\x.X(x), Y) >= D#(/\x.X(x), Y) D#(/\x.X(x), Y) >= X(_|_) D#(/\x.add(X(x), Y(x)), Z) >= D#(/\x.X(x), Z) D#(/\x.add(X(x), Y(x)), Z) >= D#(/\x.Y(x), Z) D#(/\x.add(X(x), Y(x)), Z) >= Y(_|_) D#(/\x.mul(X(x), Y(x)), Z) >= Y(Z) D#(/\x.mul(X(x), Y(x)), Z) >= X(Z) D#(/\x.mul(X(x), Y(x)), Z) > D#(/\x.Y(x), Z) D#(/\x.mul(X(x), Y(x)), Z) > Y(_|_) D#(/\x.sin(X(x)), Y) >= D#(/\x.X(x), Y) D#(/\x.cos(X(x)), Y) > D#(/\x.X(x), Y) D#(/\x.cos(X(x)), Y) > X(_|_) D(/\x.X, Y) >= _|_ D(/\x.x, X) >= _|_ D(/\x.X(x), Y) >= D(/\x.X(x), Y) D(/\x.add(X(x), Y(x)), Z) >= add(D(/\x.X(x), Z), D(/\y.Y(y), Z)) D(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\x.X(x), Z), Y(Z)), mul(X(Z), D(/\y.Y(y), Z))) D(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) D(/\x.cos(X(x)), Y) >= mul(sin(Y), D(/\x.X(x), Y)) D(F, X) >= D#(F, X) With these choices, we have: 1] D#(/\x.X(x), Y) >= D#(/\x.X(x), Y) because D# in Mul, [2] and [5], by (Fun) 2] /\y.X(y) >= /\y.X(y) because [3], by (Abs) 3] X(x) >= X(x) because [4], by (Meta) 4] x >= x by (Var) 5] Y >= Y by (Meta) 6] D#(/\x.X(x), Y) >= X(_|_) because [7], by (Star) 7] D#*(/\x.X(x), Y) >= X(_|_) because [8], by (Select) 8] X(D#*(/\x.X(x), Y)) >= X(_|_) because [9], by (Meta) 9] D#*(/\x.X(x), Y) >= _|_ by (Bot) 10] D#(/\x.add(X(x), Y(x)), Z) >= D#(/\x.X(x), Z) because D# in Mul, [11] and [16], by (Fun) 11] /\y.add(X(y), Y(y)) >= /\y.X(y) because [12], by (Abs) 12] add(X(x), Y(x)) >= X(x) because [13], by (Star) 13] add*(X(x), Y(x)) >= X(x) because [14], by (Select) 14] X(x) >= X(x) because [15], by (Meta) 15] x >= x by (Var) 16] Z >= Z by (Meta) 17] D#(/\x.add(X(x), Y(x)), Z) >= D#(/\x.Y(x), Z) because D# in Mul, [18] and [16], by (Fun) 18] /\y.add(X(y), Y(y)) >= /\y.Y(y) because [19], by (Abs) 19] add(X(x), Y(x)) >= Y(x) because [20], by (Star) 20] add*(X(x), Y(x)) >= Y(x) because [21], by (Select) 21] Y(x) >= Y(x) because [22], by (Meta) 22] x >= x by (Var) 23] D#(/\x.add(X(x), Y(x)), Z) >= Y(_|_) because [24], by (Star) 24] D#*(/\x.add(X(x), Y(x)), Z) >= Y(_|_) because [25], by (Select) 25] add(X(D#*(/\x.add(X(x), Y(x)), Z)), Y(D#*(/\y.add(X(y), Y(y)), Z))) >= Y(_|_) because [26], by (Star) 26] add*(X(D#*(/\x.add(X(x), Y(x)), Z)), Y(D#*(/\y.add(X(y), Y(y)), Z))) >= Y(_|_) because [27], by (Select) 27] Y(D#*(/\x.add(X(x), Y(x)), Z)) >= Y(_|_) because [28], by (Meta) 28] D#*(/\x.add(X(x), Y(x)), Z) >= _|_ by (Bot) 29] D#(/\x.mul(X(x), Y(x)), Z) >= Y(Z) because [30], by (Star) 30] D#*(/\x.mul(X(x), Y(x)), Z) >= Y(Z) because [31], by (Select) 31] mul(X(D#*(/\x.mul(X(x), Y(x)), Z)), Y(D#*(/\y.mul(X(y), Y(y)), Z))) >= Y(Z) because [32], by (Star) 32] mul*(X(D#*(/\x.mul(X(x), Y(x)), Z)), Y(D#*(/\y.mul(X(y), Y(y)), Z))) >= Y(Z) because [33], by (Select) 33] Y(D#*(/\x.mul(X(x), Y(x)), Z)) >= Y(Z) because [34], by (Meta) 34] D#*(/\x.mul(X(x), Y(x)), Z) >= Z because [35], by (Select) 35] Z >= Z by (Meta) 36] D#(/\x.mul(X(x), Y(x)), Z) >= X(Z) because [37], by (Star) 37] D#*(/\x.mul(X(x), Y(x)), Z) >= X(Z) because [38], by (Select) 38] mul(X(D#*(/\x.mul(X(x), Y(x)), Z)), Y(D#*(/\y.mul(X(y), Y(y)), Z))) >= X(Z) because [39], by (Star) 39] mul*(X(D#*(/\x.mul(X(x), Y(x)), Z)), Y(D#*(/\y.mul(X(y), Y(y)), Z))) >= X(Z) because [40], by (Select) 40] X(D#*(/\x.mul(X(x), Y(x)), Z)) >= X(Z) because [34], by (Meta) 41] D#(/\x.mul(X(x), Y(x)), Z) > D#(/\x.Y(x), Z) because [42], by definition 42] D#*(/\x.mul(X(x), Y(x)), Z) >= D#(/\x.Y(x), Z) because D# in Mul, [43] and [48], by (Stat) 43] /\x.mul(X(x), Y(x)) > /\x.Y(x) because [44], by definition 44] /\y.mul*(X(y), Y(y)) >= /\y.Y(y) because [45], by (Abs) 45] mul*(X(x), Y(x)) >= Y(x) because [46], by (Select) 46] Y(x) >= Y(x) because [47], by (Meta) 47] x >= x by (Var) 48] Z >= Z by (Meta) 49] D#(/\x.mul(X(x), Y(x)), Z) > Y(_|_) because [50], by definition 50] D#*(/\x.mul(X(x), Y(x)), Z) >= Y(_|_) because [51], by (Select) 51] mul(X(D#*(/\x.mul(X(x), Y(x)), Z)), Y(D#*(/\y.mul(X(y), Y(y)), Z))) >= Y(_|_) because [52], by (Star) 52] mul*(X(D#*(/\x.mul(X(x), Y(x)), Z)), Y(D#*(/\y.mul(X(y), Y(y)), Z))) >= Y(_|_) because [53], by (Select) 53] Y(D#*(/\x.mul(X(x), Y(x)), Z)) >= Y(_|_) because [54], by (Meta) 54] D#*(/\x.mul(X(x), Y(x)), Z) >= _|_ by (Bot) 55] D#(/\x.sin(X(x)), Y) >= D#(/\x.X(x), Y) because [56], by (Star) 56] D#*(/\x.sin(X(x)), Y) >= D#(/\x.X(x), Y) because D# in Mul, [57] and [62], by (Stat) 57] /\x.sin(X(x)) > /\x.X(x) because [58], by definition 58] /\y.sin*(X(y)) >= /\y.X(y) because [59], by (Abs) 59] sin*(X(x)) >= X(x) because [60], by (Select) 60] X(x) >= X(x) because [61], by (Meta) 61] x >= x by (Var) 62] Y >= Y by (Meta) 63] D#(/\x.cos(X(x)), Y) > D#(/\x.X(x), Y) because [64], by definition 64] D#*(/\x.cos(X(x)), Y) >= D#(/\x.X(x), Y) because D# in Mul, [65] and [70], by (Stat) 65] /\x.cos(X(x)) > /\x.X(x) because [66], by definition 66] /\y.cos*(X(y)) >= /\y.X(y) because [67], by (Abs) 67] cos*(X(x)) >= X(x) because [68], by (Select) 68] X(x) >= X(x) because [69], by (Meta) 69] x >= x by (Var) 70] Y >= Y by (Meta) 71] D#(/\x.cos(X(x)), Y) > X(_|_) because [72], by definition 72] D#*(/\x.cos(X(x)), Y) >= X(_|_) because [73], by (Select) 73] cos(X(D#*(/\x.cos(X(x)), Y))) >= X(_|_) because [74], by (Star) 74] cos*(X(D#*(/\x.cos(X(x)), Y))) >= X(_|_) because [75], by (Select) 75] X(D#*(/\x.cos(X(x)), Y)) >= X(_|_) because [76], by (Meta) 76] D#*(/\x.cos(X(x)), Y) >= _|_ by (Bot) 77] D(/\x.X, Y) >= _|_ by (Bot) 78] D(/\x.x, X) >= _|_ by (Bot) 79] D(/\x.X(x), Y) >= D(/\x.X(x), Y) because D in Mul, [2] and [5], by (Fun) 80] D(/\x.add(X(x), Y(x)), Z) >= add(D(/\x.X(x), Z), D(/\y.Y(y), Z)) because [81], by (Star) 81] D*(/\x.add(X(x), Y(x)), Z) >= add(D(/\x.X(x), Z), D(/\y.Y(y), Z)) because D > add, [82] and [88], by (Copy) 82] D*(/\x.add(X(x), Y(x)), Z) >= D(/\x.X(x), Z) because D in Mul, [83] and [16], by (Stat) 83] /\x.add(X(x), Y(x)) > /\x.X(x) because [84], by definition 84] /\y.add*(X(y), Y(y)) >= /\y.X(y) because [85], by (Abs) 85] add*(X(x), Y(x)) >= X(x) because [86], by (Select) 86] X(x) >= X(x) because [87], by (Meta) 87] x >= x by (Var) 88] D*(/\y.add(X(y), Y(y)), Z) >= D(/\y.Y(y), Z) because D in Mul, [89] and [16], by (Stat) 89] /\y.add(X(y), Y(y)) > /\y.Y(y) because [90], by definition 90] /\z.add*(X(z), Y(z)) >= /\z.Y(z) because [91], by (Abs) 91] add*(X(y), Y(y)) >= Y(y) because [92], by (Select) 92] Y(y) >= Y(y) because [93], by (Meta) 93] y >= y by (Var) 94] D(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\x.X(x), Z), Y(Z)), mul(X(Z), D(/\y.Y(y), Z))) because [95], by (Star) 95] D*(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\x.X(x), Z), Y(Z)), mul(X(Z), D(/\y.Y(y), Z))) because D > add, [96] and [108], by (Copy) 96] D*(/\x.mul(X(x), Y(x)), Z) >= mul(D(/\x.X(x), Z), Y(Z)) because D > mul, [97] and [103], by (Copy) 97] D*(/\x.mul(X(x), Y(x)), Z) >= D(/\x.X(x), Z) because D in Mul, [98] and [48], by (Stat) 98] /\x.mul(X(x), Y(x)) > /\x.X(x) because [99], by definition 99] /\y.mul*(X(y), Y(y)) >= /\y.X(y) because [100], by (Abs) 100] mul*(X(x), Y(x)) >= X(x) because [101], by (Select) 101] X(x) >= X(x) because [102], by (Meta) 102] x >= x by (Var) 103] D*(/\y.mul(X(y), Y(y)), Z) >= Y(Z) because [104], by (Select) 104] mul(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [105], by (Star) 105] mul*(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [106], by (Select) 106] Y(D*(/\y.mul(X(y), Y(y)), Z)) >= Y(Z) because [107], by (Meta) 107] D*(/\y.mul(X(y), Y(y)), Z) >= Z because [48], by (Select) 108] D*(/\y.mul(X(y), Y(y)), Z) >= mul(X(Z), D(/\y.Y(y), Z)) because D > mul, [109] and [113], by (Copy) 109] D*(/\y.mul(X(y), Y(y)), Z) >= X(Z) because [110], by (Select) 110] mul(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [111], by (Star) 111] mul*(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [112], by (Select) 112] X(D*(/\y.mul(X(y), Y(y)), Z)) >= X(Z) because [107], by (Meta) 113] D*(/\y.mul(X(y), Y(y)), Z) >= D(/\y.Y(y), Z) because D in Mul, [43] and [48], by (Stat) 114] D(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) because [115], by (Star) 115] D*(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) because D > mul, [116] and [118], by (Copy) 116] D*(/\x.sin(X(x)), Y) >= cos(Y) because D > cos and [117], by (Copy) 117] D*(/\x.sin(X(x)), Y) >= Y because [62], by (Select) 118] D*(/\x.sin(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [57] and [62], by (Stat) 119] D(/\x.cos(X(x)), Y) >= mul(sin(Y), D(/\x.X(x), Y)) because [120], by (Star) 120] D*(/\x.cos(X(x)), Y) >= mul(sin(Y), D(/\x.X(x), Y)) because D > mul, [121] and [123], by (Copy) 121] D*(/\x.cos(X(x)), Y) >= sin(Y) because D > sin and [122], by (Copy) 122] D*(/\x.cos(X(x)), Y) >= Y because [70], by (Select) 123] D*(/\x.cos(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [65] and [70], by (Stat) 124] D(F, X) >= D#(F, X) because [125], by (Star) 125] D*(F, X) >= D#(F, X) because D > D#, [126] and [128], by (Copy) 126] D*(F, X) >= F because [127], by (Select) 127] F >= F by (Meta) 128] D*(F, X) >= X because [129], by (Select) 129] X >= X by (Meta) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_1, R_0, minimal, all) by (P_2, R_0, minimal, all), where P_2 consists of: D#(/\x.min(X(x)), Y) =#> D#(/\y.X(y), Y) D#(/\x.min(X(x)), Y) =#> X(y) D#(/\x.add(X(x), Y(x)), Z) =#> D#(/\y.X(y), Z) D#(/\x.add(X(x), Y(x)), Z) =#> D#(/\y.Y(y), Z) D#(/\x.add(X(x), Y(x)), Z) =#> Y(y) D#(/\x.mul(X(x), Y(x)), Z) =#> Y(Z) D#(/\x.mul(X(x), Y(x)), Z) =#> X(Z) D#(/\x.sin(X(x)), Y) =#> D#(/\y.X(y), Y) Thus, the original system is terminating if (P_2, R_0, minimal, all) is finite. We consider the dependency pair problem (P_2, R_0, minimal, all). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: D#(/\x.min(X(x)), Y) >? D#(/\y.X(y), Y) D#(/\x.min(X(x)), Y) >? X(~c0) D#(/\x.add(X(x), Y(x)), Z) >? D#(/\y.X(y), Z) D#(/\x.add(X(x), Y(x)), Z) >? D#(/\y.Y(y), Z) D#(/\x.add(X(x), Y(x)), Z) >? Y(~c1) D#(/\x.mul(X(x), Y(x)), Z) >? Y(Z) D#(/\x.mul(X(x), Y(x)), Z) >? X(Z) D#(/\x.sin(X(x)), Y) >? D#(/\y.X(y), Y) D(/\x.X, Y) >= 0 D(/\x.x, X) >= 1 D(/\x.min(X(x)), Y) >= min(D(/\y.X(y), Y)) D(/\x.add(X(x), Y(x)), Z) >= add(D(/\y.X(y), Z), D(/\z.Y(z), Z)) D(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\y.X(y), Z), Y(Z)), mul(X(Z), D(/\z.Y(z), Z))) D(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\y.X(y), Y)) D(/\x.cos(X(x)), Y) >= mul(min(sin(Y)), D(/\y.X(y), Y)) D(F, X) >= D#(F, X) 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]] = _|_ [[1]] = _|_ [[min(x_1)]] = x_1 [[~c0]] = _|_ [[~c1]] = _|_ We choose Lex = {} and Mul = {D, D#, add, cos, mul, sin}, and the following precedence: D > D# > add > cos > mul > sin Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: D#(/\x.X(x), Y) >= D#(/\x.X(x), Y) D#(/\x.X(x), Y) >= X(_|_) D#(/\x.add(X(x), Y(x)), Z) >= D#(/\x.X(x), Z) D#(/\x.add(X(x), Y(x)), Z) > D#(/\x.Y(x), Z) D#(/\x.add(X(x), Y(x)), Z) >= Y(_|_) D#(/\x.mul(X(x), Y(x)), Z) > Y(Z) D#(/\x.mul(X(x), Y(x)), Z) >= X(Z) D#(/\x.sin(X(x)), Y) >= D#(/\x.X(x), Y) D(/\x.X, Y) >= _|_ D(/\x.x, X) >= _|_ D(/\x.X(x), Y) >= D(/\x.X(x), Y) D(/\x.add(X(x), Y(x)), Z) >= add(D(/\x.X(x), Z), D(/\y.Y(y), Z)) D(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\x.X(x), Z), Y(Z)), mul(X(Z), D(/\y.Y(y), Z))) D(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) D(/\x.cos(X(x)), Y) >= mul(sin(Y), D(/\x.X(x), Y)) D(F, X) >= D#(F, X) With these choices, we have: 1] D#(/\x.X(x), Y) >= D#(/\x.X(x), Y) because D# in Mul, [2] and [5], by (Fun) 2] /\y.X(y) >= /\y.X(y) because [3], by (Abs) 3] X(x) >= X(x) because [4], by (Meta) 4] x >= x by (Var) 5] Y >= Y by (Meta) 6] D#(/\x.X(x), Y) >= X(_|_) because [7], by (Star) 7] D#*(/\x.X(x), Y) >= X(_|_) because [8], by (Select) 8] X(D#*(/\x.X(x), Y)) >= X(_|_) because [9], by (Meta) 9] D#*(/\x.X(x), Y) >= _|_ by (Bot) 10] D#(/\x.add(X(x), Y(x)), Z) >= D#(/\x.X(x), Z) because D# in Mul, [11] and [16], by (Fun) 11] /\y.add(X(y), Y(y)) >= /\y.X(y) because [12], by (Abs) 12] add(X(x), Y(x)) >= X(x) because [13], by (Star) 13] add*(X(x), Y(x)) >= X(x) because [14], by (Select) 14] X(x) >= X(x) because [15], by (Meta) 15] x >= x by (Var) 16] Z >= Z by (Meta) 17] D#(/\x.add(X(x), Y(x)), Z) > D#(/\x.Y(x), Z) because [18], by definition 18] D#*(/\x.add(X(x), Y(x)), Z) >= D#(/\x.Y(x), Z) because D# in Mul, [19] and [16], by (Stat) 19] /\x.add(X(x), Y(x)) > /\x.Y(x) because [20], by definition 20] /\y.add*(X(y), Y(y)) >= /\y.Y(y) because [21], by (Abs) 21] add*(X(x), Y(x)) >= Y(x) because [22], by (Select) 22] Y(x) >= Y(x) because [23], by (Meta) 23] x >= x by (Var) 24] D#(/\x.add(X(x), Y(x)), Z) >= Y(_|_) because [25], by (Star) 25] D#*(/\x.add(X(x), Y(x)), Z) >= Y(_|_) because [26], by (Select) 26] add(X(D#*(/\x.add(X(x), Y(x)), Z)), Y(D#*(/\y.add(X(y), Y(y)), Z))) >= Y(_|_) because [27], by (Star) 27] add*(X(D#*(/\x.add(X(x), Y(x)), Z)), Y(D#*(/\y.add(X(y), Y(y)), Z))) >= Y(_|_) because [28], by (Select) 28] Y(D#*(/\x.add(X(x), Y(x)), Z)) >= Y(_|_) because [29], by (Meta) 29] D#*(/\x.add(X(x), Y(x)), Z) >= _|_ by (Bot) 30] D#(/\x.mul(X(x), Y(x)), Z) > Y(Z) because [31], by definition 31] D#*(/\x.mul(X(x), Y(x)), Z) >= Y(Z) because [32], by (Select) 32] mul(X(D#*(/\x.mul(X(x), Y(x)), Z)), Y(D#*(/\y.mul(X(y), Y(y)), Z))) >= Y(Z) because [33], by (Star) 33] mul*(X(D#*(/\x.mul(X(x), Y(x)), Z)), Y(D#*(/\y.mul(X(y), Y(y)), Z))) >= Y(Z) because [34], by (Select) 34] Y(D#*(/\x.mul(X(x), Y(x)), Z)) >= Y(Z) because [35], by (Meta) 35] D#*(/\x.mul(X(x), Y(x)), Z) >= Z because [36], by (Select) 36] Z >= Z by (Meta) 37] D#(/\x.mul(X(x), Y(x)), Z) >= X(Z) because [38], by (Star) 38] D#*(/\x.mul(X(x), Y(x)), Z) >= X(Z) because [39], by (Select) 39] mul(X(D#*(/\x.mul(X(x), Y(x)), Z)), Y(D#*(/\y.mul(X(y), Y(y)), Z))) >= X(Z) because [40], by (Star) 40] mul*(X(D#*(/\x.mul(X(x), Y(x)), Z)), Y(D#*(/\y.mul(X(y), Y(y)), Z))) >= X(Z) because [41], by (Select) 41] X(D#*(/\x.mul(X(x), Y(x)), Z)) >= X(Z) because [35], by (Meta) 42] D#(/\x.sin(X(x)), Y) >= D#(/\x.X(x), Y) because [43], by (Star) 43] D#*(/\x.sin(X(x)), Y) >= D#(/\x.X(x), Y) because D# in Mul, [44] and [49], by (Stat) 44] /\x.sin(X(x)) > /\x.X(x) because [45], by definition 45] /\y.sin*(X(y)) >= /\y.X(y) because [46], by (Abs) 46] sin*(X(x)) >= X(x) because [47], by (Select) 47] X(x) >= X(x) because [48], by (Meta) 48] x >= x by (Var) 49] Y >= Y by (Meta) 50] D(/\x.X, Y) >= _|_ by (Bot) 51] D(/\x.x, X) >= _|_ by (Bot) 52] D(/\x.X(x), Y) >= D(/\x.X(x), Y) because D in Mul, [2] and [5], by (Fun) 53] D(/\x.add(X(x), Y(x)), Z) >= add(D(/\x.X(x), Z), D(/\y.Y(y), Z)) because [54], by (Star) 54] D*(/\x.add(X(x), Y(x)), Z) >= add(D(/\x.X(x), Z), D(/\y.Y(y), Z)) because D > add, [55] and [61], by (Copy) 55] D*(/\x.add(X(x), Y(x)), Z) >= D(/\x.X(x), Z) because D in Mul, [56] and [16], by (Stat) 56] /\x.add(X(x), Y(x)) > /\x.X(x) because [57], by definition 57] /\y.add*(X(y), Y(y)) >= /\y.X(y) because [58], by (Abs) 58] add*(X(x), Y(x)) >= X(x) because [59], by (Select) 59] X(x) >= X(x) because [60], by (Meta) 60] x >= x by (Var) 61] D*(/\y.add(X(y), Y(y)), Z) >= D(/\y.Y(y), Z) because D in Mul, [19] and [16], by (Stat) 62] D(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\x.X(x), Z), Y(Z)), mul(X(Z), D(/\y.Y(y), Z))) because [63], by (Star) 63] D*(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\x.X(x), Z), Y(Z)), mul(X(Z), D(/\y.Y(y), Z))) because D > add, [64] and [77], by (Copy) 64] D*(/\x.mul(X(x), Y(x)), Z) >= mul(D(/\x.X(x), Z), Y(Z)) because D > mul, [65] and [72], by (Copy) 65] D*(/\x.mul(X(x), Y(x)), Z) >= D(/\x.X(x), Z) because D in Mul, [66] and [71], by (Stat) 66] /\x.mul(X(x), Y(x)) > /\x.X(x) because [67], by definition 67] /\y.mul*(X(y), Y(y)) >= /\y.X(y) because [68], by (Abs) 68] mul*(X(x), Y(x)) >= X(x) because [69], by (Select) 69] X(x) >= X(x) because [70], by (Meta) 70] x >= x by (Var) 71] Z >= Z by (Meta) 72] D*(/\y.mul(X(y), Y(y)), Z) >= Y(Z) because [73], by (Select) 73] mul(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [74], by (Star) 74] mul*(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [75], by (Select) 75] Y(D*(/\y.mul(X(y), Y(y)), Z)) >= Y(Z) because [76], by (Meta) 76] D*(/\y.mul(X(y), Y(y)), Z) >= Z because [71], by (Select) 77] D*(/\y.mul(X(y), Y(y)), Z) >= mul(X(Z), D(/\y.Y(y), Z)) because D > mul, [78] and [82], by (Copy) 78] D*(/\y.mul(X(y), Y(y)), Z) >= X(Z) because [79], by (Select) 79] mul(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [80], by (Star) 80] mul*(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [81], by (Select) 81] X(D*(/\y.mul(X(y), Y(y)), Z)) >= X(Z) because [76], by (Meta) 82] D*(/\y.mul(X(y), Y(y)), Z) >= D(/\y.Y(y), Z) because D in Mul, [83] and [71], by (Stat) 83] /\y.mul(X(y), Y(y)) > /\y.Y(y) because [84], by definition 84] /\z.mul*(X(z), Y(z)) >= /\z.Y(z) because [85], by (Abs) 85] mul*(X(y), Y(y)) >= Y(y) because [86], by (Select) 86] Y(y) >= Y(y) because [87], by (Meta) 87] y >= y by (Var) 88] D(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) because [89], by (Star) 89] D*(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) because D > mul, [90] and [92], by (Copy) 90] D*(/\x.sin(X(x)), Y) >= cos(Y) because D > cos and [91], by (Copy) 91] D*(/\x.sin(X(x)), Y) >= Y because [49], by (Select) 92] D*(/\x.sin(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [44] and [49], by (Stat) 93] D(/\x.cos(X(x)), Y) >= mul(sin(Y), D(/\x.X(x), Y)) because [94], by (Star) 94] D*(/\x.cos(X(x)), Y) >= mul(sin(Y), D(/\x.X(x), Y)) because D > mul, [95] and [98], by (Copy) 95] D*(/\x.cos(X(x)), Y) >= sin(Y) because D > sin and [96], by (Copy) 96] D*(/\x.cos(X(x)), Y) >= Y because [97], by (Select) 97] Y >= Y by (Meta) 98] D*(/\x.cos(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [99] and [104], by (Stat) 99] /\x.cos(X(x)) > /\x.X(x) because [100], by definition 100] /\y.cos*(X(y)) >= /\y.X(y) because [101], by (Abs) 101] cos*(X(x)) >= X(x) because [102], by (Select) 102] X(x) >= X(x) because [103], by (Meta) 103] x >= x by (Var) 104] Y >= Y by (Meta) 105] D(F, X) >= D#(F, X) because [106], by (Star) 106] D*(F, X) >= D#(F, X) because D > D#, [107] and [109], by (Copy) 107] D*(F, X) >= F because [108], by (Select) 108] F >= F by (Meta) 109] D*(F, X) >= X because [110], by (Select) 110] X >= X by (Meta) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_2, R_0, minimal, all) by (P_3, R_0, minimal, all), where P_3 consists of: D#(/\x.min(X(x)), Y) =#> D#(/\y.X(y), Y) D#(/\x.min(X(x)), Y) =#> X(y) D#(/\x.add(X(x), Y(x)), Z) =#> D#(/\y.X(y), Z) D#(/\x.add(X(x), Y(x)), Z) =#> Y(y) D#(/\x.mul(X(x), Y(x)), Z) =#> X(Z) D#(/\x.sin(X(x)), Y) =#> D#(/\y.X(y), Y) Thus, the original system is terminating if (P_3, R_0, minimal, all) is finite. We consider the dependency pair problem (P_3, R_0, minimal, all). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: D#(/\x.min(X(x)), Y) >? D#(/\y.X(y), Y) D#(/\x.min(X(x)), Y) >? X(~c0) D#(/\x.add(X(x), Y(x)), Z) >? D#(/\y.X(y), Z) D#(/\x.add(X(x), Y(x)), Z) >? Y(~c1) D#(/\x.mul(X(x), Y(x)), Z) >? X(Z) D#(/\x.sin(X(x)), Y) >? D#(/\y.X(y), Y) D(/\x.X, Y) >= 0 D(/\x.x, X) >= 1 D(/\x.min(X(x)), Y) >= min(D(/\y.X(y), Y)) D(/\x.add(X(x), Y(x)), Z) >= add(D(/\y.X(y), Z), D(/\z.Y(z), Z)) D(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\y.X(y), Z), Y(Z)), mul(X(Z), D(/\z.Y(z), Z))) D(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\y.X(y), Y)) D(/\x.cos(X(x)), Y) >= mul(min(sin(Y)), D(/\y.X(y), Y)) D(F, X) >= D#(F, X) 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]] = _|_ [[1]] = _|_ [[~c0]] = _|_ [[~c1]] = _|_ We choose Lex = {} and Mul = {D, D#, add, cos, min, mul, sin}, and the following precedence: D = cos > D# > add > min > mul > sin Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: D#(/\x.min(X(x)), Y) >= D#(/\x.X(x), Y) D#(/\x.min(X(x)), Y) >= X(_|_) D#(/\x.add(X(x), Y(x)), Z) >= D#(/\x.X(x), Z) D#(/\x.add(X(x), Y(x)), Z) > Y(_|_) D#(/\x.mul(X(x), Y(x)), Z) >= X(Z) D#(/\x.sin(X(x)), Y) >= D#(/\x.X(x), Y) D(/\x.X, Y) >= _|_ D(/\x.x, X) >= _|_ D(/\x.min(X(x)), Y) >= min(D(/\x.X(x), Y)) D(/\x.add(X(x), Y(x)), Z) >= add(D(/\x.X(x), Z), D(/\y.Y(y), Z)) D(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\x.X(x), Z), Y(Z)), mul(X(Z), D(/\y.Y(y), Z))) D(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) D(/\x.cos(X(x)), Y) >= mul(min(sin(Y)), D(/\x.X(x), Y)) D(F, X) >= D#(F, X) With these choices, we have: 1] D#(/\x.min(X(x)), Y) >= D#(/\x.X(x), Y) because D# in Mul, [2] and [7], by (Fun) 2] /\y.min(X(y)) >= /\y.X(y) because [3], by (Abs) 3] min(X(x)) >= X(x) because [4], by (Star) 4] min*(X(x)) >= X(x) because [5], by (Select) 5] X(x) >= X(x) because [6], by (Meta) 6] x >= x by (Var) 7] Y >= Y by (Meta) 8] D#(/\x.min(X(x)), Y) >= X(_|_) because [9], by (Star) 9] D#*(/\x.min(X(x)), Y) >= X(_|_) because [10], by (Select) 10] min(X(D#*(/\x.min(X(x)), Y))) >= X(_|_) because [11], by (Star) 11] min*(X(D#*(/\x.min(X(x)), Y))) >= X(_|_) because [12], by (Select) 12] X(D#*(/\x.min(X(x)), Y)) >= X(_|_) because [13], by (Meta) 13] D#*(/\x.min(X(x)), Y) >= _|_ by (Bot) 14] D#(/\x.add(X(x), Y(x)), Z) >= D#(/\x.X(x), Z) because D# in Mul, [15] and [20], by (Fun) 15] /\y.add(X(y), Y(y)) >= /\y.X(y) because [16], by (Abs) 16] add(X(x), Y(x)) >= X(x) because [17], by (Star) 17] add*(X(x), Y(x)) >= X(x) because [18], by (Select) 18] X(x) >= X(x) because [19], by (Meta) 19] x >= x by (Var) 20] Z >= Z by (Meta) 21] D#(/\x.add(X(x), Y(x)), Z) > Y(_|_) because [22], by definition 22] D#*(/\x.add(X(x), Y(x)), Z) >= Y(_|_) because [23], by (Select) 23] add(X(D#*(/\x.add(X(x), Y(x)), Z)), Y(D#*(/\y.add(X(y), Y(y)), Z))) >= Y(_|_) because [24], by (Star) 24] add*(X(D#*(/\x.add(X(x), Y(x)), Z)), Y(D#*(/\y.add(X(y), Y(y)), Z))) >= Y(_|_) because [25], by (Select) 25] Y(D#*(/\x.add(X(x), Y(x)), Z)) >= Y(_|_) because [26], by (Meta) 26] D#*(/\x.add(X(x), Y(x)), Z) >= _|_ by (Bot) 27] D#(/\x.mul(X(x), Y(x)), Z) >= X(Z) because [28], by (Star) 28] D#*(/\x.mul(X(x), Y(x)), Z) >= X(Z) because [29], by (Select) 29] mul(X(D#*(/\x.mul(X(x), Y(x)), Z)), Y(D#*(/\y.mul(X(y), Y(y)), Z))) >= X(Z) because [30], by (Star) 30] mul*(X(D#*(/\x.mul(X(x), Y(x)), Z)), Y(D#*(/\y.mul(X(y), Y(y)), Z))) >= X(Z) because [31], by (Select) 31] X(D#*(/\x.mul(X(x), Y(x)), Z)) >= X(Z) because [32], by (Meta) 32] D#*(/\x.mul(X(x), Y(x)), Z) >= Z because [33], by (Select) 33] Z >= Z by (Meta) 34] D#(/\x.sin(X(x)), Y) >= D#(/\x.X(x), Y) because D# in Mul, [35] and [40], by (Fun) 35] /\y.sin(X(y)) >= /\y.X(y) because [36], by (Abs) 36] sin(X(x)) >= X(x) because [37], by (Star) 37] sin*(X(x)) >= X(x) because [38], by (Select) 38] X(x) >= X(x) because [39], by (Meta) 39] x >= x by (Var) 40] Y >= Y by (Meta) 41] D(/\x.X, Y) >= _|_ by (Bot) 42] D(/\x.x, X) >= _|_ by (Bot) 43] D(/\x.min(X(x)), Y) >= min(D(/\x.X(x), Y)) because [44], by (Star) 44] D*(/\x.min(X(x)), Y) >= min(D(/\x.X(x), Y)) because D > min and [45], by (Copy) 45] D*(/\x.min(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [46] and [7], by (Stat) 46] /\x.min(X(x)) > /\x.X(x) because [47], by definition 47] /\y.min*(X(y)) >= /\y.X(y) because [48], by (Abs) 48] min*(X(x)) >= X(x) because [49], by (Select) 49] X(x) >= X(x) because [50], by (Meta) 50] x >= x by (Var) 51] D(/\x.add(X(x), Y(x)), Z) >= add(D(/\x.X(x), Z), D(/\y.Y(y), Z)) because [52], by (Star) 52] D*(/\x.add(X(x), Y(x)), Z) >= add(D(/\x.X(x), Z), D(/\y.Y(y), Z)) because D > add, [53] and [59], by (Copy) 53] D*(/\x.add(X(x), Y(x)), Z) >= D(/\x.X(x), Z) because D in Mul, [54] and [20], by (Stat) 54] /\x.add(X(x), Y(x)) > /\x.X(x) because [55], by definition 55] /\y.add*(X(y), Y(y)) >= /\y.X(y) because [56], by (Abs) 56] add*(X(x), Y(x)) >= X(x) because [57], by (Select) 57] X(x) >= X(x) because [58], by (Meta) 58] x >= x by (Var) 59] D*(/\y.add(X(y), Y(y)), Z) >= D(/\y.Y(y), Z) because D in Mul, [60] and [20], by (Stat) 60] /\y.add(X(y), Y(y)) > /\y.Y(y) because [61], by definition 61] /\z.add*(X(z), Y(z)) >= /\z.Y(z) because [62], by (Abs) 62] add*(X(y), Y(y)) >= Y(y) because [63], by (Select) 63] Y(y) >= Y(y) because [64], by (Meta) 64] y >= y by (Var) 65] D(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\x.X(x), Z), Y(Z)), mul(X(Z), D(/\y.Y(y), Z))) because [66], by (Star) 66] D*(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\x.X(x), Z), Y(Z)), mul(X(Z), D(/\y.Y(y), Z))) because D > add, [67] and [80], by (Copy) 67] D*(/\x.mul(X(x), Y(x)), Z) >= mul(D(/\x.X(x), Z), Y(Z)) because D > mul, [68] and [75], by (Copy) 68] D*(/\x.mul(X(x), Y(x)), Z) >= D(/\x.X(x), Z) because D in Mul, [69] and [74], by (Stat) 69] /\x.mul(X(x), Y(x)) > /\x.X(x) because [70], by definition 70] /\y.mul*(X(y), Y(y)) >= /\y.X(y) because [71], by (Abs) 71] mul*(X(x), Y(x)) >= X(x) because [72], by (Select) 72] X(x) >= X(x) because [73], by (Meta) 73] x >= x by (Var) 74] Z >= Z by (Meta) 75] D*(/\y.mul(X(y), Y(y)), Z) >= Y(Z) because [76], by (Select) 76] mul(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [77], by (Star) 77] mul*(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [78], by (Select) 78] Y(D*(/\y.mul(X(y), Y(y)), Z)) >= Y(Z) because [79], by (Meta) 79] D*(/\y.mul(X(y), Y(y)), Z) >= Z because [74], by (Select) 80] D*(/\y.mul(X(y), Y(y)), Z) >= mul(X(Z), D(/\y.Y(y), Z)) because D > mul, [81] and [85], by (Copy) 81] D*(/\y.mul(X(y), Y(y)), Z) >= X(Z) because [82], by (Select) 82] mul(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [83], by (Star) 83] mul*(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [84], by (Select) 84] X(D*(/\y.mul(X(y), Y(y)), Z)) >= X(Z) because [79], by (Meta) 85] D*(/\y.mul(X(y), Y(y)), Z) >= D(/\y.Y(y), Z) because D in Mul, [86] and [74], by (Stat) 86] /\y.mul(X(y), Y(y)) > /\y.Y(y) because [87], by definition 87] /\z.mul*(X(z), Y(z)) >= /\z.Y(z) because [88], by (Abs) 88] mul*(X(y), Y(y)) >= Y(y) because [89], by (Select) 89] Y(y) >= Y(y) because [90], by (Meta) 90] y >= y by (Var) 91] D(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) because [92], by (Star) 92] D*(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) because D > mul, [93] and [94], by (Copy) 93] D*(/\x.sin(X(x)), Y) >= cos(Y) because D = cos, D in Mul and [40], by (Stat) 94] D*(/\x.sin(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [95] and [40], by (Stat) 95] /\x.sin(X(x)) > /\x.X(x) because [96], by definition 96] /\y.sin*(X(y)) >= /\y.X(y) because [97], by (Abs) 97] sin*(X(x)) >= X(x) because [98], by (Select) 98] X(x) >= X(x) because [99], by (Meta) 99] x >= x by (Var) 100] D(/\x.cos(X(x)), Y) >= mul(min(sin(Y)), D(/\x.X(x), Y)) because [101], by (Star) 101] D*(/\x.cos(X(x)), Y) >= mul(min(sin(Y)), D(/\x.X(x), Y)) because D > mul, [102] and [106], by (Copy) 102] D*(/\x.cos(X(x)), Y) >= min(sin(Y)) because D > min and [103], by (Copy) 103] D*(/\x.cos(X(x)), Y) >= sin(Y) because D > sin and [104], by (Copy) 104] D*(/\x.cos(X(x)), Y) >= Y because [105], by (Select) 105] Y >= Y by (Meta) 106] D*(/\x.cos(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [107] and [112], by (Stat) 107] /\x.cos(X(x)) > /\x.X(x) because [108], by definition 108] /\y.cos*(X(y)) >= /\y.X(y) because [109], by (Abs) 109] cos*(X(x)) >= X(x) because [110], by (Select) 110] X(x) >= X(x) because [111], by (Meta) 111] x >= x by (Var) 112] Y >= Y by (Meta) 113] D(F, X) >= D#(F, X) because [114], by (Star) 114] D*(F, X) >= D#(F, X) because D > D#, [115] and [117], by (Copy) 115] D*(F, X) >= F because [116], by (Select) 116] F >= F by (Meta) 117] D*(F, X) >= X because [118], by (Select) 118] X >= X by (Meta) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_3, R_0, minimal, all) by (P_4, R_0, minimal, all), where P_4 consists of: D#(/\x.min(X(x)), Y) =#> D#(/\y.X(y), Y) D#(/\x.min(X(x)), Y) =#> X(y) D#(/\x.add(X(x), Y(x)), Z) =#> D#(/\y.X(y), Z) D#(/\x.mul(X(x), Y(x)), Z) =#> X(Z) D#(/\x.sin(X(x)), Y) =#> D#(/\y.X(y), Y) Thus, the original system is terminating if (P_4, R_0, minimal, all) is finite. We consider the dependency pair problem (P_4, R_0, minimal, all). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: D#(/\x.min(X(x)), Y) >? D#(/\y.X(y), Y) D#(/\x.min(X(x)), Y) >? X(~c0) D#(/\x.add(X(x), Y(x)), Z) >? D#(/\y.X(y), Z) D#(/\x.mul(X(x), Y(x)), Z) >? X(Z) D#(/\x.sin(X(x)), Y) >? D#(/\y.X(y), Y) D(/\x.X, Y) >= 0 D(/\x.x, X) >= 1 D(/\x.min(X(x)), Y) >= min(D(/\y.X(y), Y)) D(/\x.add(X(x), Y(x)), Z) >= add(D(/\y.X(y), Z), D(/\z.Y(z), Z)) D(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\y.X(y), Z), Y(Z)), mul(X(Z), D(/\z.Y(z), Z))) D(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\y.X(y), Y)) D(/\x.cos(X(x)), Y) >= mul(min(sin(Y)), D(/\y.X(y), Y)) D(F, X) >= D#(F, X) 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]] = _|_ [[1]] = _|_ [[~c0]] = _|_ We choose Lex = {} and Mul = {D, D#, add, cos, min, mul, sin}, and the following precedence: D > D# > add > cos > min > mul > sin Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: D#(/\x.min(X(x)), Y) >= D#(/\x.X(x), Y) D#(/\x.min(X(x)), Y) > X(_|_) D#(/\x.add(X(x), Y(x)), Z) >= D#(/\x.X(x), Z) D#(/\x.mul(X(x), Y(x)), Z) >= X(Z) D#(/\x.sin(X(x)), Y) >= D#(/\x.X(x), Y) D(/\x.X, Y) >= _|_ D(/\x.x, X) >= _|_ D(/\x.min(X(x)), Y) >= min(D(/\x.X(x), Y)) D(/\x.add(X(x), Y(x)), Z) >= add(D(/\x.X(x), Z), D(/\y.Y(y), Z)) D(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\x.X(x), Z), Y(Z)), mul(X(Z), D(/\y.Y(y), Z))) D(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) D(/\x.cos(X(x)), Y) >= mul(min(sin(Y)), D(/\x.X(x), Y)) D(F, X) >= D#(F, X) With these choices, we have: 1] D#(/\x.min(X(x)), Y) >= D#(/\x.X(x), Y) because D# in Mul, [2] and [7], by (Fun) 2] /\y.min(X(y)) >= /\y.X(y) because [3], by (Abs) 3] min(X(x)) >= X(x) because [4], by (Star) 4] min*(X(x)) >= X(x) because [5], by (Select) 5] X(x) >= X(x) because [6], by (Meta) 6] x >= x by (Var) 7] Y >= Y by (Meta) 8] D#(/\x.min(X(x)), Y) > X(_|_) because [9], by definition 9] D#*(/\x.min(X(x)), Y) >= X(_|_) because [10], by (Select) 10] min(X(D#*(/\x.min(X(x)), Y))) >= X(_|_) because [11], by (Star) 11] min*(X(D#*(/\x.min(X(x)), Y))) >= X(_|_) because [12], by (Select) 12] X(D#*(/\x.min(X(x)), Y)) >= X(_|_) because [13], by (Meta) 13] D#*(/\x.min(X(x)), Y) >= _|_ by (Bot) 14] D#(/\x.add(X(x), Y(x)), Z) >= D#(/\x.X(x), Z) because D# in Mul, [15] and [20], by (Fun) 15] /\y.add(X(y), Y(y)) >= /\y.X(y) because [16], by (Abs) 16] add(X(x), Y(x)) >= X(x) because [17], by (Star) 17] add*(X(x), Y(x)) >= X(x) because [18], by (Select) 18] X(x) >= X(x) because [19], by (Meta) 19] x >= x by (Var) 20] Z >= Z by (Meta) 21] D#(/\x.mul(X(x), Y(x)), Z) >= X(Z) because [22], by (Star) 22] D#*(/\x.mul(X(x), Y(x)), Z) >= X(Z) because [23], by (Select) 23] mul(X(D#*(/\x.mul(X(x), Y(x)), Z)), Y(D#*(/\y.mul(X(y), Y(y)), Z))) >= X(Z) because [24], by (Star) 24] mul*(X(D#*(/\x.mul(X(x), Y(x)), Z)), Y(D#*(/\y.mul(X(y), Y(y)), Z))) >= X(Z) because [25], by (Select) 25] X(D#*(/\x.mul(X(x), Y(x)), Z)) >= X(Z) because [26], by (Meta) 26] D#*(/\x.mul(X(x), Y(x)), Z) >= Z because [27], by (Select) 27] Z >= Z by (Meta) 28] D#(/\x.sin(X(x)), Y) >= D#(/\x.X(x), Y) because [29], by (Star) 29] D#*(/\x.sin(X(x)), Y) >= D#(/\x.X(x), Y) because D# in Mul, [30] and [35], by (Stat) 30] /\x.sin(X(x)) > /\x.X(x) because [31], by definition 31] /\y.sin*(X(y)) >= /\y.X(y) because [32], by (Abs) 32] sin*(X(x)) >= X(x) because [33], by (Select) 33] X(x) >= X(x) because [34], by (Meta) 34] x >= x by (Var) 35] Y >= Y by (Meta) 36] D(/\x.X, Y) >= _|_ by (Bot) 37] D(/\x.x, X) >= _|_ by (Bot) 38] D(/\x.min(X(x)), Y) >= min(D(/\x.X(x), Y)) because [39], by (Star) 39] D*(/\x.min(X(x)), Y) >= min(D(/\x.X(x), Y)) because D > min and [40], by (Copy) 40] D*(/\x.min(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [41] and [7], by (Stat) 41] /\x.min(X(x)) > /\x.X(x) because [42], by definition 42] /\y.min*(X(y)) >= /\y.X(y) because [43], by (Abs) 43] min*(X(x)) >= X(x) because [44], by (Select) 44] X(x) >= X(x) because [45], by (Meta) 45] x >= x by (Var) 46] D(/\x.add(X(x), Y(x)), Z) >= add(D(/\x.X(x), Z), D(/\y.Y(y), Z)) because [47], by (Star) 47] D*(/\x.add(X(x), Y(x)), Z) >= add(D(/\x.X(x), Z), D(/\y.Y(y), Z)) because D > add, [48] and [54], by (Copy) 48] D*(/\x.add(X(x), Y(x)), Z) >= D(/\x.X(x), Z) because D in Mul, [49] and [20], by (Stat) 49] /\x.add(X(x), Y(x)) > /\x.X(x) because [50], by definition 50] /\y.add*(X(y), Y(y)) >= /\y.X(y) because [51], by (Abs) 51] add*(X(x), Y(x)) >= X(x) because [52], by (Select) 52] X(x) >= X(x) because [53], by (Meta) 53] x >= x by (Var) 54] D*(/\y.add(X(y), Y(y)), Z) >= D(/\y.Y(y), Z) because D in Mul, [55] and [20], by (Stat) 55] /\y.add(X(y), Y(y)) > /\y.Y(y) because [56], by definition 56] /\z.add*(X(z), Y(z)) >= /\z.Y(z) because [57], by (Abs) 57] add*(X(y), Y(y)) >= Y(y) because [58], by (Select) 58] Y(y) >= Y(y) because [59], by (Meta) 59] y >= y by (Var) 60] D(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\x.X(x), Z), Y(Z)), mul(X(Z), D(/\y.Y(y), Z))) because [61], by (Star) 61] D*(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\x.X(x), Z), Y(Z)), mul(X(Z), D(/\y.Y(y), Z))) because D > add, [62] and [75], by (Copy) 62] D*(/\x.mul(X(x), Y(x)), Z) >= mul(D(/\x.X(x), Z), Y(Z)) because D > mul, [63] and [70], by (Copy) 63] D*(/\x.mul(X(x), Y(x)), Z) >= D(/\x.X(x), Z) because D in Mul, [64] and [69], by (Stat) 64] /\x.mul(X(x), Y(x)) > /\x.X(x) because [65], by definition 65] /\y.mul*(X(y), Y(y)) >= /\y.X(y) because [66], by (Abs) 66] mul*(X(x), Y(x)) >= X(x) because [67], by (Select) 67] X(x) >= X(x) because [68], by (Meta) 68] x >= x by (Var) 69] Z >= Z by (Meta) 70] D*(/\y.mul(X(y), Y(y)), Z) >= Y(Z) because [71], by (Select) 71] mul(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [72], by (Star) 72] mul*(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [73], by (Select) 73] Y(D*(/\y.mul(X(y), Y(y)), Z)) >= Y(Z) because [74], by (Meta) 74] D*(/\y.mul(X(y), Y(y)), Z) >= Z because [69], by (Select) 75] D*(/\y.mul(X(y), Y(y)), Z) >= mul(X(Z), D(/\y.Y(y), Z)) because D > mul, [76] and [80], by (Copy) 76] D*(/\y.mul(X(y), Y(y)), Z) >= X(Z) because [77], by (Select) 77] mul(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [78], by (Star) 78] mul*(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [79], by (Select) 79] X(D*(/\y.mul(X(y), Y(y)), Z)) >= X(Z) because [74], by (Meta) 80] D*(/\y.mul(X(y), Y(y)), Z) >= D(/\y.Y(y), Z) because D in Mul, [81] and [69], by (Stat) 81] /\y.mul(X(y), Y(y)) > /\y.Y(y) because [82], by definition 82] /\z.mul*(X(z), Y(z)) >= /\z.Y(z) because [83], by (Abs) 83] mul*(X(y), Y(y)) >= Y(y) because [84], by (Select) 84] Y(y) >= Y(y) because [85], by (Meta) 85] y >= y by (Var) 86] D(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) because [87], by (Star) 87] D*(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) because D > mul, [88] and [90], by (Copy) 88] D*(/\x.sin(X(x)), Y) >= cos(Y) because D > cos and [89], by (Copy) 89] D*(/\x.sin(X(x)), Y) >= Y because [35], by (Select) 90] D*(/\x.sin(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [30] and [35], by (Stat) 91] D(/\x.cos(X(x)), Y) >= mul(min(sin(Y)), D(/\x.X(x), Y)) because [92], by (Star) 92] D*(/\x.cos(X(x)), Y) >= mul(min(sin(Y)), D(/\x.X(x), Y)) because D > mul, [93] and [97], by (Copy) 93] D*(/\x.cos(X(x)), Y) >= min(sin(Y)) because D > min and [94], by (Copy) 94] D*(/\x.cos(X(x)), Y) >= sin(Y) because D > sin and [95], by (Copy) 95] D*(/\x.cos(X(x)), Y) >= Y because [96], by (Select) 96] Y >= Y by (Meta) 97] D*(/\x.cos(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [98] and [103], by (Stat) 98] /\x.cos(X(x)) > /\x.X(x) because [99], by definition 99] /\y.cos*(X(y)) >= /\y.X(y) because [100], by (Abs) 100] cos*(X(x)) >= X(x) because [101], by (Select) 101] X(x) >= X(x) because [102], by (Meta) 102] x >= x by (Var) 103] Y >= Y by (Meta) 104] D(F, X) >= D#(F, X) because [105], by (Star) 105] D*(F, X) >= D#(F, X) because D > D#, [106] and [108], by (Copy) 106] D*(F, X) >= F because [107], by (Select) 107] F >= F by (Meta) 108] D*(F, X) >= X because [109], by (Select) 109] X >= X by (Meta) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_4, R_0, minimal, all) by (P_5, R_0, minimal, all), where P_5 consists of: D#(/\x.min(X(x)), Y) =#> D#(/\y.X(y), Y) D#(/\x.add(X(x), Y(x)), Z) =#> D#(/\y.X(y), Z) D#(/\x.mul(X(x), Y(x)), Z) =#> X(Z) D#(/\x.sin(X(x)), Y) =#> D#(/\y.X(y), Y) Thus, the original system is terminating if (P_5, R_0, minimal, all) is finite. We consider the dependency pair problem (P_5, R_0, minimal, all). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: D#(/\x.min(X(x)), Y) >? D#(/\y.X(y), Y) D#(/\x.add(X(x), Y(x)), Z) >? D#(/\y.X(y), Z) D#(/\x.mul(X(x), Y(x)), Z) >? X(Z) D#(/\x.sin(X(x)), Y) >? D#(/\y.X(y), Y) D(/\x.X, Y) >= 0 D(/\x.x, X) >= 1 D(/\x.min(X(x)), Y) >= min(D(/\y.X(y), Y)) D(/\x.add(X(x), Y(x)), Z) >= add(D(/\y.X(y), Z), D(/\z.Y(z), Z)) D(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\y.X(y), Z), Y(Z)), mul(X(Z), D(/\z.Y(z), Z))) D(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\y.X(y), Y)) D(/\x.cos(X(x)), Y) >= mul(min(sin(Y)), D(/\y.X(y), Y)) D(F, X) >= D#(F, X) 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]] = _|_ [[1]] = _|_ We choose Lex = {} and Mul = {D, D#, add, cos, min, mul, sin}, and the following precedence: D > D# > add > cos > min > mul > sin Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: D#(/\x.min(X(x)), Y) >= D#(/\x.X(x), Y) D#(/\x.add(X(x), Y(x)), Z) > D#(/\x.X(x), Z) D#(/\x.mul(X(x), Y(x)), Z) >= X(Z) D#(/\x.sin(X(x)), Y) >= D#(/\x.X(x), Y) D(/\x.X, Y) >= _|_ D(/\x.x, X) >= _|_ D(/\x.min(X(x)), Y) >= min(D(/\x.X(x), Y)) D(/\x.add(X(x), Y(x)), Z) >= add(D(/\x.X(x), Z), D(/\y.Y(y), Z)) D(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\x.X(x), Z), Y(Z)), mul(X(Z), D(/\y.Y(y), Z))) D(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) D(/\x.cos(X(x)), Y) >= mul(min(sin(Y)), D(/\x.X(x), Y)) D(F, X) >= D#(F, X) With these choices, we have: 1] D#(/\x.min(X(x)), Y) >= D#(/\x.X(x), Y) because [2], by (Star) 2] D#*(/\x.min(X(x)), Y) >= D#(/\x.X(x), Y) because D# in Mul, [3] and [8], by (Stat) 3] /\x.min(X(x)) > /\x.X(x) because [4], by definition 4] /\y.min*(X(y)) >= /\y.X(y) because [5], by (Abs) 5] min*(X(x)) >= X(x) because [6], by (Select) 6] X(x) >= X(x) because [7], by (Meta) 7] x >= x by (Var) 8] Y >= Y by (Meta) 9] D#(/\x.add(X(x), Y(x)), Z) > D#(/\x.X(x), Z) because [10], by definition 10] D#*(/\x.add(X(x), Y(x)), Z) >= D#(/\x.X(x), Z) because D# in Mul, [11] and [16], by (Stat) 11] /\x.add(X(x), Y(x)) > /\x.X(x) because [12], by definition 12] /\y.add*(X(y), Y(y)) >= /\y.X(y) because [13], by (Abs) 13] add*(X(x), Y(x)) >= X(x) because [14], by (Select) 14] X(x) >= X(x) because [15], by (Meta) 15] x >= x by (Var) 16] Z >= Z by (Meta) 17] D#(/\x.mul(X(x), Y(x)), Z) >= X(Z) because [18], by (Star) 18] D#*(/\x.mul(X(x), Y(x)), Z) >= X(Z) because [19], by (Select) 19] mul(X(D#*(/\x.mul(X(x), Y(x)), Z)), Y(D#*(/\y.mul(X(y), Y(y)), Z))) >= X(Z) because [20], by (Star) 20] mul*(X(D#*(/\x.mul(X(x), Y(x)), Z)), Y(D#*(/\y.mul(X(y), Y(y)), Z))) >= X(Z) because [21], by (Select) 21] X(D#*(/\x.mul(X(x), Y(x)), Z)) >= X(Z) because [22], by (Meta) 22] D#*(/\x.mul(X(x), Y(x)), Z) >= Z because [23], by (Select) 23] Z >= Z by (Meta) 24] D#(/\x.sin(X(x)), Y) >= D#(/\x.X(x), Y) because [25], by (Star) 25] D#*(/\x.sin(X(x)), Y) >= D#(/\x.X(x), Y) because D# in Mul, [26] and [31], by (Stat) 26] /\x.sin(X(x)) > /\x.X(x) because [27], by definition 27] /\y.sin*(X(y)) >= /\y.X(y) because [28], by (Abs) 28] sin*(X(x)) >= X(x) because [29], by (Select) 29] X(x) >= X(x) because [30], by (Meta) 30] x >= x by (Var) 31] Y >= Y by (Meta) 32] D(/\x.X, Y) >= _|_ by (Bot) 33] D(/\x.x, X) >= _|_ by (Bot) 34] D(/\x.min(X(x)), Y) >= min(D(/\x.X(x), Y)) because [35], by (Star) 35] D*(/\x.min(X(x)), Y) >= min(D(/\x.X(x), Y)) because D > min and [36], by (Copy) 36] D*(/\x.min(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [3] and [8], by (Stat) 37] D(/\x.add(X(x), Y(x)), Z) >= add(D(/\x.X(x), Z), D(/\y.Y(y), Z)) because [38], by (Star) 38] D*(/\x.add(X(x), Y(x)), Z) >= add(D(/\x.X(x), Z), D(/\y.Y(y), Z)) because D > add, [39] and [40], by (Copy) 39] D*(/\x.add(X(x), Y(x)), Z) >= D(/\x.X(x), Z) because D in Mul, [11] and [16], by (Stat) 40] D*(/\x.add(X(x), Y(x)), Z) >= D(/\x.Y(x), Z) because D in Mul, [41] and [16], by (Stat) 41] /\x.add(X(x), Y(x)) > /\x.Y(x) because [42], by definition 42] /\y.add*(X(y), Y(y)) >= /\y.Y(y) because [43], by (Abs) 43] add*(X(x), Y(x)) >= Y(x) because [44], by (Select) 44] Y(x) >= Y(x) because [45], by (Meta) 45] x >= x by (Var) 46] D(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\x.X(x), Z), Y(Z)), mul(X(Z), D(/\y.Y(y), Z))) because [47], by (Star) 47] D*(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\x.X(x), Z), Y(Z)), mul(X(Z), D(/\y.Y(y), Z))) because D > add, [48] and [61], by (Copy) 48] D*(/\x.mul(X(x), Y(x)), Z) >= mul(D(/\x.X(x), Z), Y(Z)) because D > mul, [49] and [56], by (Copy) 49] D*(/\x.mul(X(x), Y(x)), Z) >= D(/\x.X(x), Z) because D in Mul, [50] and [55], by (Stat) 50] /\x.mul(X(x), Y(x)) > /\x.X(x) because [51], by definition 51] /\y.mul*(X(y), Y(y)) >= /\y.X(y) because [52], by (Abs) 52] mul*(X(x), Y(x)) >= X(x) because [53], by (Select) 53] X(x) >= X(x) because [54], by (Meta) 54] x >= x by (Var) 55] Z >= Z by (Meta) 56] D*(/\y.mul(X(y), Y(y)), Z) >= Y(Z) because [57], by (Select) 57] mul(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [58], by (Star) 58] mul*(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [59], by (Select) 59] Y(D*(/\y.mul(X(y), Y(y)), Z)) >= Y(Z) because [60], by (Meta) 60] D*(/\y.mul(X(y), Y(y)), Z) >= Z because [55], by (Select) 61] D*(/\y.mul(X(y), Y(y)), Z) >= mul(X(Z), D(/\y.Y(y), Z)) because D > mul, [62] and [66], by (Copy) 62] D*(/\y.mul(X(y), Y(y)), Z) >= X(Z) because [63], by (Select) 63] mul(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [64], by (Star) 64] mul*(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [65], by (Select) 65] X(D*(/\y.mul(X(y), Y(y)), Z)) >= X(Z) because [60], by (Meta) 66] D*(/\y.mul(X(y), Y(y)), Z) >= D(/\y.Y(y), Z) because D in Mul, [67] and [55], by (Stat) 67] /\y.mul(X(y), Y(y)) > /\y.Y(y) because [68], by definition 68] /\z.mul*(X(z), Y(z)) >= /\z.Y(z) because [69], by (Abs) 69] mul*(X(y), Y(y)) >= Y(y) because [70], by (Select) 70] Y(y) >= Y(y) because [71], by (Meta) 71] y >= y by (Var) 72] D(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) because [73], by (Star) 73] D*(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) because D > mul, [74] and [76], by (Copy) 74] D*(/\x.sin(X(x)), Y) >= cos(Y) because D > cos and [75], by (Copy) 75] D*(/\x.sin(X(x)), Y) >= Y because [31], by (Select) 76] D*(/\x.sin(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [26] and [31], by (Stat) 77] D(/\x.cos(X(x)), Y) >= mul(min(sin(Y)), D(/\x.X(x), Y)) because [78], by (Star) 78] D*(/\x.cos(X(x)), Y) >= mul(min(sin(Y)), D(/\x.X(x), Y)) because D > mul, [79] and [83], by (Copy) 79] D*(/\x.cos(X(x)), Y) >= min(sin(Y)) because D > min and [80], by (Copy) 80] D*(/\x.cos(X(x)), Y) >= sin(Y) because D > sin and [81], by (Copy) 81] D*(/\x.cos(X(x)), Y) >= Y because [82], by (Select) 82] Y >= Y by (Meta) 83] D*(/\x.cos(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [84] and [89], by (Stat) 84] /\x.cos(X(x)) > /\x.X(x) because [85], by definition 85] /\y.cos*(X(y)) >= /\y.X(y) because [86], by (Abs) 86] cos*(X(x)) >= X(x) because [87], by (Select) 87] X(x) >= X(x) because [88], by (Meta) 88] x >= x by (Var) 89] Y >= Y by (Meta) 90] D(F, X) >= D#(F, X) because [91], by (Star) 91] D*(F, X) >= D#(F, X) because D > D#, [92] and [94], by (Copy) 92] D*(F, X) >= F because [93], by (Select) 93] F >= F by (Meta) 94] D*(F, X) >= X because [95], by (Select) 95] X >= X by (Meta) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_5, R_0, minimal, all) by (P_6, R_0, minimal, all), where P_6 consists of: D#(/\x.min(X(x)), Y) =#> D#(/\y.X(y), Y) D#(/\x.mul(X(x), Y(x)), Z) =#> X(Z) D#(/\x.sin(X(x)), Y) =#> D#(/\y.X(y), Y) Thus, the original system is terminating if (P_6, R_0, minimal, all) is finite. We consider the dependency pair problem (P_6, R_0, minimal, all). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: D#(/\x.min(X(x)), Y) >? D#(/\y.X(y), Y) D#(/\x.mul(X(x), Y(x)), Z) >? X(Z) D#(/\x.sin(X(x)), Y) >? D#(/\y.X(y), Y) D(/\x.X, Y) >= 0 D(/\x.x, X) >= 1 D(/\x.min(X(x)), Y) >= min(D(/\y.X(y), Y)) D(/\x.add(X(x), Y(x)), Z) >= add(D(/\y.X(y), Z), D(/\z.Y(z), Z)) D(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\y.X(y), Z), Y(Z)), mul(X(Z), D(/\z.Y(z), Z))) D(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\y.X(y), Y)) D(/\x.cos(X(x)), Y) >= mul(min(sin(Y)), D(/\y.X(y), Y)) D(F, X) >= D#(F, X) 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]] = _|_ [[1]] = _|_ [[min(x_1)]] = x_1 We choose Lex = {} and Mul = {D, D#, add, cos, mul, sin}, and the following precedence: D > D# > add > cos > mul > sin Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: D#(/\x.X(x), Y) >= D#(/\x.X(x), Y) D#(/\x.mul(X(x), Y(x)), Z) >= X(Z) D#(/\x.sin(X(x)), Y) > D#(/\x.X(x), Y) D(/\x.X, Y) >= _|_ D(/\x.x, X) >= _|_ D(/\x.X(x), Y) >= D(/\x.X(x), Y) D(/\x.add(X(x), Y(x)), Z) >= add(D(/\x.X(x), Z), D(/\y.Y(y), Z)) D(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\x.X(x), Z), Y(Z)), mul(X(Z), D(/\y.Y(y), Z))) D(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) D(/\x.cos(X(x)), Y) >= mul(sin(Y), D(/\x.X(x), Y)) D(F, X) >= D#(F, X) With these choices, we have: 1] D#(/\x.X(x), Y) >= D#(/\x.X(x), Y) because D# in Mul, [2] and [5], by (Fun) 2] /\y.X(y) >= /\y.X(y) because [3], by (Abs) 3] X(x) >= X(x) because [4], by (Meta) 4] x >= x by (Var) 5] Y >= Y by (Meta) 6] D#(/\x.mul(X(x), Y(x)), Z) >= X(Z) because [7], by (Star) 7] D#*(/\x.mul(X(x), Y(x)), Z) >= X(Z) because [8], by (Select) 8] mul(X(D#*(/\x.mul(X(x), Y(x)), Z)), Y(D#*(/\y.mul(X(y), Y(y)), Z))) >= X(Z) because [9], by (Star) 9] mul*(X(D#*(/\x.mul(X(x), Y(x)), Z)), Y(D#*(/\y.mul(X(y), Y(y)), Z))) >= X(Z) because [10], by (Select) 10] X(D#*(/\x.mul(X(x), Y(x)), Z)) >= X(Z) because [11], by (Meta) 11] D#*(/\x.mul(X(x), Y(x)), Z) >= Z because [12], by (Select) 12] Z >= Z by (Meta) 13] D#(/\x.sin(X(x)), Y) > D#(/\x.X(x), Y) because [14], by definition 14] D#*(/\x.sin(X(x)), Y) >= D#(/\x.X(x), Y) because D# in Mul, [15] and [20], by (Stat) 15] /\x.sin(X(x)) > /\x.X(x) because [16], by definition 16] /\y.sin*(X(y)) >= /\y.X(y) because [17], by (Abs) 17] sin*(X(x)) >= X(x) because [18], by (Select) 18] X(x) >= X(x) because [19], by (Meta) 19] x >= x by (Var) 20] Y >= Y by (Meta) 21] D(/\x.X, Y) >= _|_ by (Bot) 22] D(/\x.x, X) >= _|_ by (Bot) 23] D(/\x.X(x), Y) >= D(/\x.X(x), Y) because D in Mul, [2] and [5], by (Fun) 24] D(/\x.add(X(x), Y(x)), Z) >= add(D(/\x.X(x), Z), D(/\y.Y(y), Z)) because [25], by (Star) 25] D*(/\x.add(X(x), Y(x)), Z) >= add(D(/\x.X(x), Z), D(/\y.Y(y), Z)) because D > add, [26] and [33], by (Copy) 26] D*(/\x.add(X(x), Y(x)), Z) >= D(/\x.X(x), Z) because D in Mul, [27] and [32], by (Stat) 27] /\x.add(X(x), Y(x)) > /\x.X(x) because [28], by definition 28] /\y.add*(X(y), Y(y)) >= /\y.X(y) because [29], by (Abs) 29] add*(X(x), Y(x)) >= X(x) because [30], by (Select) 30] X(x) >= X(x) because [31], by (Meta) 31] x >= x by (Var) 32] Z >= Z by (Meta) 33] D*(/\y.add(X(y), Y(y)), Z) >= D(/\y.Y(y), Z) because D in Mul, [34] and [32], by (Stat) 34] /\y.add(X(y), Y(y)) > /\y.Y(y) because [35], by definition 35] /\z.add*(X(z), Y(z)) >= /\z.Y(z) because [36], by (Abs) 36] add*(X(y), Y(y)) >= Y(y) because [37], by (Select) 37] Y(y) >= Y(y) because [38], by (Meta) 38] y >= y by (Var) 39] D(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\x.X(x), Z), Y(Z)), mul(X(Z), D(/\y.Y(y), Z))) because [40], by (Star) 40] D*(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\x.X(x), Z), Y(Z)), mul(X(Z), D(/\y.Y(y), Z))) because D > add, [41] and [54], by (Copy) 41] D*(/\x.mul(X(x), Y(x)), Z) >= mul(D(/\x.X(x), Z), Y(Z)) because D > mul, [42] and [49], by (Copy) 42] D*(/\x.mul(X(x), Y(x)), Z) >= D(/\x.X(x), Z) because D in Mul, [43] and [48], by (Stat) 43] /\x.mul(X(x), Y(x)) > /\x.X(x) because [44], by definition 44] /\y.mul*(X(y), Y(y)) >= /\y.X(y) because [45], by (Abs) 45] mul*(X(x), Y(x)) >= X(x) because [46], by (Select) 46] X(x) >= X(x) because [47], by (Meta) 47] x >= x by (Var) 48] Z >= Z by (Meta) 49] D*(/\y.mul(X(y), Y(y)), Z) >= Y(Z) because [50], by (Select) 50] mul(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [51], by (Star) 51] mul*(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [52], by (Select) 52] Y(D*(/\y.mul(X(y), Y(y)), Z)) >= Y(Z) because [53], by (Meta) 53] D*(/\y.mul(X(y), Y(y)), Z) >= Z because [48], by (Select) 54] D*(/\y.mul(X(y), Y(y)), Z) >= mul(X(Z), D(/\y.Y(y), Z)) because D > mul, [55] and [59], by (Copy) 55] D*(/\y.mul(X(y), Y(y)), Z) >= X(Z) because [56], by (Select) 56] mul(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [57], by (Star) 57] mul*(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [58], by (Select) 58] X(D*(/\y.mul(X(y), Y(y)), Z)) >= X(Z) because [53], by (Meta) 59] D*(/\y.mul(X(y), Y(y)), Z) >= D(/\y.Y(y), Z) because D in Mul, [60] and [48], by (Stat) 60] /\y.mul(X(y), Y(y)) > /\y.Y(y) because [61], by definition 61] /\z.mul*(X(z), Y(z)) >= /\z.Y(z) because [62], by (Abs) 62] mul*(X(y), Y(y)) >= Y(y) because [63], by (Select) 63] Y(y) >= Y(y) because [64], by (Meta) 64] y >= y by (Var) 65] D(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) because [66], by (Star) 66] D*(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) because D > mul, [67] and [69], by (Copy) 67] D*(/\x.sin(X(x)), Y) >= cos(Y) because D > cos and [68], by (Copy) 68] D*(/\x.sin(X(x)), Y) >= Y because [20], by (Select) 69] D*(/\x.sin(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [15] and [20], by (Stat) 70] D(/\x.cos(X(x)), Y) >= mul(sin(Y), D(/\x.X(x), Y)) because [71], by (Star) 71] D*(/\x.cos(X(x)), Y) >= mul(sin(Y), D(/\x.X(x), Y)) because D > mul, [72] and [75], by (Copy) 72] D*(/\x.cos(X(x)), Y) >= sin(Y) because D > sin and [73], by (Copy) 73] D*(/\x.cos(X(x)), Y) >= Y because [74], by (Select) 74] Y >= Y by (Meta) 75] D*(/\x.cos(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [76] and [81], by (Stat) 76] /\x.cos(X(x)) > /\x.X(x) because [77], by definition 77] /\y.cos*(X(y)) >= /\y.X(y) because [78], by (Abs) 78] cos*(X(x)) >= X(x) because [79], by (Select) 79] X(x) >= X(x) because [80], by (Meta) 80] x >= x by (Var) 81] Y >= Y by (Meta) 82] D(F, X) >= D#(F, X) because [83], by (Star) 83] D*(F, X) >= D#(F, X) because D > D#, [84] and [86], by (Copy) 84] D*(F, X) >= F because [85], by (Select) 85] F >= F by (Meta) 86] D*(F, X) >= X because [87], by (Select) 87] X >= X 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, minimal, all) by (P_7, R_0, minimal, all), where P_7 consists of: D#(/\x.min(X(x)), Y) =#> D#(/\y.X(y), Y) D#(/\x.mul(X(x), Y(x)), Z) =#> X(Z) Thus, the original system is terminating if (P_7, R_0, minimal, all) is finite. We consider the dependency pair problem (P_7, R_0, minimal, all). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: D#(/\x.min(X(x)), Y) >? D#(/\y.X(y), Y) D#(/\x.mul(X(x), Y(x)), Z) >? X(Z) D(/\x.X, Y) >= 0 D(/\x.x, X) >= 1 D(/\x.min(X(x)), Y) >= min(D(/\y.X(y), Y)) D(/\x.add(X(x), Y(x)), Z) >= add(D(/\y.X(y), Z), D(/\z.Y(z), Z)) D(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\y.X(y), Z), Y(Z)), mul(X(Z), D(/\z.Y(z), Z))) D(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\y.X(y), Y)) D(/\x.cos(X(x)), Y) >= mul(min(sin(Y)), D(/\y.X(y), Y)) D(F, X) >= D#(F, X) 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]] = _|_ [[1]] = _|_ We choose Lex = {} and Mul = {D, D#, add, cos, min, mul, sin}, and the following precedence: D > D# > add > cos > min > mul > sin Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: D#(/\x.min(X(x)), Y) >= D#(/\x.X(x), Y) D#(/\x.mul(X(x), Y(x)), Z) > X(Z) D(/\x.X, Y) >= _|_ D(/\x.x, X) >= _|_ D(/\x.min(X(x)), Y) >= min(D(/\x.X(x), Y)) D(/\x.add(X(x), Y(x)), Z) >= add(D(/\x.X(x), Z), D(/\y.Y(y), Z)) D(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\x.X(x), Z), Y(Z)), mul(X(Z), D(/\y.Y(y), Z))) D(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) D(/\x.cos(X(x)), Y) >= mul(min(sin(Y)), D(/\x.X(x), Y)) D(F, X) >= D#(F, X) With these choices, we have: 1] D#(/\x.min(X(x)), Y) >= D#(/\x.X(x), Y) because D# in Mul, [2] and [7], by (Fun) 2] /\y.min(X(y)) >= /\y.X(y) because [3], by (Abs) 3] min(X(x)) >= X(x) because [4], by (Star) 4] min*(X(x)) >= X(x) because [5], by (Select) 5] X(x) >= X(x) because [6], by (Meta) 6] x >= x by (Var) 7] Y >= Y by (Meta) 8] D#(/\x.mul(X(x), Y(x)), Z) > X(Z) because [9], by definition 9] D#*(/\x.mul(X(x), Y(x)), Z) >= X(Z) because [10], by (Select) 10] mul(X(D#*(/\x.mul(X(x), Y(x)), Z)), Y(D#*(/\y.mul(X(y), Y(y)), Z))) >= X(Z) because [11], by (Star) 11] mul*(X(D#*(/\x.mul(X(x), Y(x)), Z)), Y(D#*(/\y.mul(X(y), Y(y)), Z))) >= X(Z) because [12], by (Select) 12] X(D#*(/\x.mul(X(x), Y(x)), Z)) >= X(Z) because [13], by (Meta) 13] D#*(/\x.mul(X(x), Y(x)), Z) >= Z because [14], by (Select) 14] Z >= Z by (Meta) 15] D(/\x.X, Y) >= _|_ by (Bot) 16] D(/\x.x, X) >= _|_ by (Bot) 17] D(/\x.min(X(x)), Y) >= min(D(/\x.X(x), Y)) because [18], by (Star) 18] D*(/\x.min(X(x)), Y) >= min(D(/\x.X(x), Y)) because D > min and [19], by (Copy) 19] D*(/\x.min(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [20] and [7], by (Stat) 20] /\x.min(X(x)) > /\x.X(x) because [21], by definition 21] /\y.min*(X(y)) >= /\y.X(y) because [22], by (Abs) 22] min*(X(x)) >= X(x) because [23], by (Select) 23] X(x) >= X(x) because [24], by (Meta) 24] x >= x by (Var) 25] D(/\x.add(X(x), Y(x)), Z) >= add(D(/\x.X(x), Z), D(/\y.Y(y), Z)) because [26], by (Star) 26] D*(/\x.add(X(x), Y(x)), Z) >= add(D(/\x.X(x), Z), D(/\y.Y(y), Z)) because D > add, [27] and [34], by (Copy) 27] D*(/\x.add(X(x), Y(x)), Z) >= D(/\x.X(x), Z) because D in Mul, [28] and [33], by (Stat) 28] /\x.add(X(x), Y(x)) > /\x.X(x) because [29], by definition 29] /\y.add*(X(y), Y(y)) >= /\y.X(y) because [30], by (Abs) 30] add*(X(x), Y(x)) >= X(x) because [31], by (Select) 31] X(x) >= X(x) because [32], by (Meta) 32] x >= x by (Var) 33] Z >= Z by (Meta) 34] D*(/\y.add(X(y), Y(y)), Z) >= D(/\y.Y(y), Z) because D in Mul, [35] and [33], by (Stat) 35] /\y.add(X(y), Y(y)) > /\y.Y(y) because [36], by definition 36] /\z.add*(X(z), Y(z)) >= /\z.Y(z) because [37], by (Abs) 37] add*(X(y), Y(y)) >= Y(y) because [38], by (Select) 38] Y(y) >= Y(y) because [39], by (Meta) 39] y >= y by (Var) 40] D(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\x.X(x), Z), Y(Z)), mul(X(Z), D(/\y.Y(y), Z))) because [41], by (Star) 41] D*(/\x.mul(X(x), Y(x)), Z) >= add(mul(D(/\x.X(x), Z), Y(Z)), mul(X(Z), D(/\y.Y(y), Z))) because D > add, [42] and [55], by (Copy) 42] D*(/\x.mul(X(x), Y(x)), Z) >= mul(D(/\x.X(x), Z), Y(Z)) because D > mul, [43] and [50], by (Copy) 43] D*(/\x.mul(X(x), Y(x)), Z) >= D(/\x.X(x), Z) because D in Mul, [44] and [49], by (Stat) 44] /\x.mul(X(x), Y(x)) > /\x.X(x) because [45], by definition 45] /\y.mul*(X(y), Y(y)) >= /\y.X(y) because [46], by (Abs) 46] mul*(X(x), Y(x)) >= X(x) because [47], by (Select) 47] X(x) >= X(x) because [48], by (Meta) 48] x >= x by (Var) 49] Z >= Z by (Meta) 50] D*(/\y.mul(X(y), Y(y)), Z) >= Y(Z) because [51], by (Select) 51] mul(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [52], by (Star) 52] mul*(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [53], by (Select) 53] Y(D*(/\y.mul(X(y), Y(y)), Z)) >= Y(Z) because [54], by (Meta) 54] D*(/\y.mul(X(y), Y(y)), Z) >= Z because [49], by (Select) 55] D*(/\y.mul(X(y), Y(y)), Z) >= mul(X(Z), D(/\y.Y(y), Z)) because D > mul, [56] and [60], by (Copy) 56] D*(/\y.mul(X(y), Y(y)), Z) >= X(Z) because [57], by (Select) 57] mul(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [58], by (Star) 58] mul*(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [59], by (Select) 59] X(D*(/\y.mul(X(y), Y(y)), Z)) >= X(Z) because [54], by (Meta) 60] D*(/\y.mul(X(y), Y(y)), Z) >= D(/\y.Y(y), Z) because D in Mul, [61] and [49], by (Stat) 61] /\y.mul(X(y), Y(y)) > /\y.Y(y) because [62], by definition 62] /\z.mul*(X(z), Y(z)) >= /\z.Y(z) because [63], by (Abs) 63] mul*(X(y), Y(y)) >= Y(y) because [64], by (Select) 64] Y(y) >= Y(y) because [65], by (Meta) 65] y >= y by (Var) 66] D(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) because [67], by (Star) 67] D*(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) because D > mul, [68] and [71], by (Copy) 68] D*(/\x.sin(X(x)), Y) >= cos(Y) because D > cos and [69], by (Copy) 69] D*(/\x.sin(X(x)), Y) >= Y because [70], by (Select) 70] Y >= Y by (Meta) 71] D*(/\x.sin(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [72] and [77], by (Stat) 72] /\x.sin(X(x)) > /\x.X(x) because [73], by definition 73] /\y.sin*(X(y)) >= /\y.X(y) because [74], by (Abs) 74] sin*(X(x)) >= X(x) because [75], by (Select) 75] X(x) >= X(x) because [76], by (Meta) 76] x >= x by (Var) 77] Y >= Y by (Meta) 78] D(/\x.cos(X(x)), Y) >= mul(min(sin(Y)), D(/\x.X(x), Y)) because [79], by (Star) 79] D*(/\x.cos(X(x)), Y) >= mul(min(sin(Y)), D(/\x.X(x), Y)) because D > mul, [80] and [84], by (Copy) 80] D*(/\x.cos(X(x)), Y) >= min(sin(Y)) because D > min and [81], by (Copy) 81] D*(/\x.cos(X(x)), Y) >= sin(Y) because D > sin and [82], by (Copy) 82] D*(/\x.cos(X(x)), Y) >= Y because [83], by (Select) 83] Y >= Y by (Meta) 84] D*(/\x.cos(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [85] and [90], by (Stat) 85] /\x.cos(X(x)) > /\x.X(x) because [86], by definition 86] /\y.cos*(X(y)) >= /\y.X(y) because [87], by (Abs) 87] cos*(X(x)) >= X(x) because [88], by (Select) 88] X(x) >= X(x) because [89], by (Meta) 89] x >= x by (Var) 90] Y >= Y by (Meta) 91] D(F, X) >= D#(F, X) because [92], by (Star) 92] D*(F, X) >= D#(F, X) because D > D#, [93] and [95], by (Copy) 93] D*(F, X) >= F because [94], by (Select) 94] F >= F by (Meta) 95] D*(F, X) >= X because [96], by (Select) 96] X >= X by (Meta) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_7, R_0, minimal, all) by (P_8, R_0, minimal, all), where P_8 consists of: D#(/\x.min(X(x)), Y) =#> D#(/\y.X(y), Y) Thus, the original system is terminating if (P_8, R_0, minimal, all) is finite. We consider the dependency pair problem (P_8, R_0, minimal, all). 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: D#(/\x.min(X(x)), Y) >? D#(/\y.X(y), Y) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: D# = \G0y1.3G0(0) + 3G0(y1) + y1G0(y1) min = \y0.3 + 3y0 Using this interpretation, the requirements translate to: [[D#(/\x.min(_x0(x)), _x1)]] = 18 + 3x1 + 3x1F0(x1) + 9F0(0) + 9F0(x1) > 3F0(0) + 3F0(x1) + x1F0(x1) = [[D#(/\x._x0(x), _x1)]] 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. 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.