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 rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): 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 a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[1]] = _|_ We choose Lex = {} and Mul = {D, add, cos, min, mul, sin}, and the following precedence: D > add > min > mul > cos > sin Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: 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)) With these choices, we have: 1] D(/\x.X, Y) >= _|_ by (Bot) 2] D(/\x.x, X) >= _|_ by (Bot) 3] D(/\x.min(X(x)), Y) > min(D(/\x.X(x), Y)) because [4], by definition 4] D*(/\x.min(X(x)), Y) >= min(D(/\x.X(x), Y)) because D > min and [5], by (Copy) 5] D*(/\x.min(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [6] and [11], by (Stat) 6] /\x.min(X(x)) > /\x.X(x) because [7], by definition 7] /\y.min*(X(y)) >= /\y.X(y) because [8], by (Abs) 8] min*(X(x)) >= X(x) because [9], by (Select) 9] X(x) >= X(x) because [10], by (Meta) 10] x >= x by (Var) 11] Y >= Y by (Meta) 12] D(/\x.add(X(x), Y(x)), Z) > add(D(/\x.X(x), Z), D(/\y.Y(y), Z)) because [13], by definition 13] D*(/\x.add(X(x), Y(x)), Z) >= add(D(/\x.X(x), Z), D(/\y.Y(y), Z)) because D > add, [14] and [21], by (Copy) 14] D*(/\x.add(X(x), Y(x)), Z) >= D(/\x.X(x), Z) because D in Mul, [15] and [20], by (Stat) 15] /\x.add(X(x), Y(x)) > /\x.X(x) because [16], by definition 16] /\y.add*(X(y), Y(y)) >= /\y.X(y) because [17], by (Abs) 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*(/\y.add(X(y), Y(y)), Z) >= D(/\y.Y(y), Z) because D in Mul, [22] and [20], by (Stat) 22] /\y.add(X(y), Y(y)) > /\y.Y(y) because [23], by definition 23] /\z.add*(X(z), Y(z)) >= /\z.Y(z) because [24], by (Abs) 24] add*(X(y), Y(y)) >= Y(y) because [25], by (Select) 25] Y(y) >= Y(y) because [26], by (Meta) 26] y >= y by (Var) 27] 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 [28], by (Star) 28] 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, [29] and [42], by (Copy) 29] D*(/\x.mul(X(x), Y(x)), Z) >= mul(D(/\x.X(x), Z), Y(Z)) because D > mul, [30] and [37], by (Copy) 30] D*(/\x.mul(X(x), Y(x)), Z) >= D(/\x.X(x), Z) because D in Mul, [31] and [36], by (Stat) 31] /\x.mul(X(x), Y(x)) > /\x.X(x) because [32], by definition 32] /\y.mul*(X(y), Y(y)) >= /\y.X(y) because [33], by (Abs) 33] mul*(X(x), Y(x)) >= X(x) because [34], by (Select) 34] X(x) >= X(x) because [35], by (Meta) 35] x >= x by (Var) 36] Z >= Z by (Meta) 37] D*(/\y.mul(X(y), Y(y)), Z) >= Y(Z) because [38], by (Select) 38] mul(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [39], by (Star) 39] mul*(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [40], by (Select) 40] Y(D*(/\y.mul(X(y), Y(y)), Z)) >= Y(Z) because [41], by (Meta) 41] D*(/\y.mul(X(y), Y(y)), Z) >= Z because [36], by (Select) 42] D*(/\y.mul(X(y), Y(y)), Z) >= mul(X(Z), D(/\y.Y(y), Z)) because D > mul, [43] and [47], by (Copy) 43] D*(/\y.mul(X(y), Y(y)), Z) >= X(Z) because [44], by (Select) 44] mul(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [45], by (Star) 45] mul*(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [46], by (Select) 46] X(D*(/\y.mul(X(y), Y(y)), Z)) >= X(Z) because [41], by (Meta) 47] D*(/\y.mul(X(y), Y(y)), Z) >= D(/\y.Y(y), Z) because D in Mul, [48] and [36], by (Stat) 48] /\y.mul(X(y), Y(y)) > /\y.Y(y) because [49], by definition 49] /\z.mul*(X(z), Y(z)) >= /\z.Y(z) because [50], by (Abs) 50] mul*(X(y), Y(y)) >= Y(y) because [51], by (Select) 51] Y(y) >= Y(y) because [52], by (Meta) 52] y >= y by (Var) 53] D(/\x.sin(X(x)), Y) > mul(cos(Y), D(/\x.X(x), Y)) because [54], by definition 54] D*(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) because D > mul, [55] and [58], by (Copy) 55] D*(/\x.sin(X(x)), Y) >= cos(Y) because D > cos and [56], by (Copy) 56] D*(/\x.sin(X(x)), Y) >= Y because [57], by (Select) 57] Y >= Y by (Meta) 58] D*(/\x.sin(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [59] and [64], by (Stat) 59] /\x.sin(X(x)) > /\x.X(x) because [60], by definition 60] /\y.sin*(X(y)) >= /\y.X(y) because [61], by (Abs) 61] sin*(X(x)) >= X(x) because [62], by (Select) 62] X(x) >= X(x) because [63], by (Meta) 63] x >= x by (Var) 64] Y >= Y by (Meta) 65] D(/\x.cos(X(x)), Y) >= mul(min(sin(Y)), D(/\x.X(x), Y)) because [66], by (Star) 66] D*(/\x.cos(X(x)), Y) >= mul(min(sin(Y)), D(/\x.X(x), Y)) because D > mul, [67] and [71], by (Copy) 67] D*(/\x.cos(X(x)), Y) >= min(sin(Y)) because D > min and [68], by (Copy) 68] D*(/\x.cos(X(x)), Y) >= sin(Y) because D > sin and [69], by (Copy) 69] D*(/\x.cos(X(x)), Y) >= Y because [70], by (Select) 70] Y >= Y by (Meta) 71] D*(/\x.cos(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [72] and [77], by (Stat) 72] /\x.cos(X(x)) > /\x.X(x) because [73], by definition 73] /\y.cos*(X(y)) >= /\y.X(y) because [74], by (Abs) 74] cos*(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) We can thus remove the following rules: 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.sin(X(x)), Y) => mul(cos(Y), D(/\y.X(y), 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(/\x.X, Y) >? 0 D(/\x.x, X) >? 1 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.cos(X(x)), Y) >? mul(min(sin(Y)), D(/\y.X(y), Y)) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[1]] = _|_ [[min(x_1)]] = x_1 [[sin(x_1)]] = x_1 We choose Lex = {} and Mul = {D, add, cos, mul}, and the following precedence: cos > D > mul > add Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: D(/\x.X, Y) >= _|_ D(/\x.x, X) >= _|_ 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.cos(X(x)), Y) >= mul(Y, D(/\x.X(x), Y)) With these choices, we have: 1] D(/\x.X, Y) >= _|_ by (Bot) 2] D(/\x.x, X) >= _|_ by (Bot) 3] 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 [4], by definition 4] 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, [5] and [18], by (Copy) 5] D*(/\x.mul(X(x), Y(x)), Z) >= mul(D(/\x.X(x), Z), Y(Z)) because D > mul, [6] and [13], by (Copy) 6] D*(/\x.mul(X(x), Y(x)), Z) >= D(/\x.X(x), Z) because D in Mul, [7] and [12], by (Stat) 7] /\x.mul(X(x), Y(x)) > /\x.X(x) because [8], by definition 8] /\y.mul*(X(y), Y(y)) >= /\y.X(y) because [9], by (Abs) 9] mul*(X(x), Y(x)) >= X(x) because [10], by (Select) 10] X(x) >= X(x) because [11], by (Meta) 11] x >= x by (Var) 12] Z >= Z by (Meta) 13] D*(/\y.mul(X(y), Y(y)), Z) >= Y(Z) because [14], by (Select) 14] mul(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [15], by (Star) 15] mul*(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [16], by (Select) 16] Y(D*(/\y.mul(X(y), Y(y)), Z)) >= Y(Z) because [17], by (Meta) 17] D*(/\y.mul(X(y), Y(y)), Z) >= Z because [12], by (Select) 18] D*(/\y.mul(X(y), Y(y)), Z) >= mul(X(Z), D(/\y.Y(y), Z)) because D > mul, [19] and [23], by (Copy) 19] D*(/\y.mul(X(y), Y(y)), Z) >= X(Z) because [20], by (Select) 20] mul(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [21], by (Star) 21] mul*(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [22], by (Select) 22] X(D*(/\y.mul(X(y), Y(y)), Z)) >= X(Z) because [17], by (Meta) 23] D*(/\y.mul(X(y), Y(y)), Z) >= D(/\y.Y(y), Z) because D in Mul, [24] and [12], by (Stat) 24] /\y.mul(X(y), Y(y)) > /\y.Y(y) because [25], by definition 25] /\z.mul*(X(z), Y(z)) >= /\z.Y(z) because [26], by (Abs) 26] mul*(X(y), Y(y)) >= Y(y) because [27], by (Select) 27] Y(y) >= Y(y) because [28], by (Meta) 28] y >= y by (Var) 29] D(/\x.cos(X(x)), Y) >= mul(Y, D(/\x.X(x), Y)) because [30], by (Star) 30] D*(/\x.cos(X(x)), Y) >= mul(Y, D(/\x.X(x), Y)) because D > mul, [31] and [33], by (Copy) 31] D*(/\x.cos(X(x)), Y) >= Y because [32], by (Select) 32] Y >= Y by (Meta) 33] D*(/\x.cos(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [34] and [39], by (Stat) 34] /\x.cos(X(x)) > /\x.X(x) because [35], by definition 35] /\y.cos*(X(y)) >= /\y.X(y) because [36], by (Abs) 36] cos*(X(x)) >= X(x) because [37], by (Select) 37] X(x) >= X(x) because [38], by (Meta) 38] x >= x by (Var) 39] Y >= Y by (Meta) We can thus remove the following rules: 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))) 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(/\x.X, Y) >? 0 D(/\x.x, X) >? 1 D(/\x.cos(X(x)), Y) >? mul(min(sin(Y)), D(/\y.X(y), Y)) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 0 1 = 0 D = \G0y1.1 + y1 + 3G0(0) + 3G0(y1) + y1G0(y1) cos = \y0.3 + 3y0 min = \y0.y0 mul = \y0y1.y0 + y1 sin = \y0.y0 Using this interpretation, the requirements translate to: [[D(/\x._x0, _x1)]] = 1 + x1 + 6x0 + x0x1 > 0 = [[0]] [[D(/\x.x, _x0)]] = 1 + 4x0 + x0x0 > 0 = [[1]] [[D(/\x.cos(_x0(x)), _x1)]] = 19 + 4x1 + 3x1F0(x1) + 9F0(0) + 9F0(x1) > 1 + 2x1 + 3F0(0) + 3F0(x1) + x1F0(x1) = [[mul(min(sin(_x1)), D(/\x._x0(x), _x1))]] We can thus remove the following rules: D(/\x.X, Y) => 0 D(/\x.x, X) => 1 D(/\x.cos(X(x)), Y) => mul(min(sin(Y)), D(/\y.X(y), Y)) 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.