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]] = _|_ [[min(x_1)]] = x_1 We choose Lex = {} and Mul = {D, add, cos, mul, sin}, and the following precedence: D > sin > mul > add > cos 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.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)) With these choices, we have: 1] D(/\x.X, Y) >= _|_ by (Bot) 2] D(/\x.x, X) >= _|_ by (Bot) 3] D(/\x.X(x), Y) >= D(/\x.X(x), Y) because D in Mul, [4] and [7], by (Fun) 4] /\y.X(y) >= /\y.X(y) because [5], by (Abs) 5] X(x) >= X(x) because [6], by (Meta) 6] x >= x by (Var) 7] Y >= Y by (Meta) 8] D(/\x.add(X(x), Y(x)), Z) > add(D(/\x.X(x), Z), D(/\y.Y(y), Z)) because [9], by definition 9] D*(/\x.add(X(x), Y(x)), Z) >= add(D(/\x.X(x), Z), D(/\y.Y(y), Z)) because D > add, [10] and [17], by (Copy) 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*(/\y.add(X(y), Y(y)), Z) >= D(/\y.Y(y), Z) because D in Mul, [18] and [16], by (Stat) 18] /\y.add(X(y), Y(y)) > /\y.Y(y) because [19], by definition 19] /\z.add*(X(z), Y(z)) >= /\z.Y(z) because [20], by (Abs) 20] add*(X(y), Y(y)) >= Y(y) because [21], by (Select) 21] Y(y) >= Y(y) because [22], by (Meta) 22] y >= y by (Var) 23] 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 [24], by definition 24] 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, [25] and [38], by (Copy) 25] D*(/\x.mul(X(x), Y(x)), Z) >= mul(D(/\x.X(x), Z), Y(Z)) because D > mul, [26] and [33], by (Copy) 26] D*(/\x.mul(X(x), Y(x)), Z) >= D(/\x.X(x), Z) because D in Mul, [27] and [32], by (Stat) 27] /\x.mul(X(x), Y(x)) > /\x.X(x) because [28], by definition 28] /\y.mul*(X(y), Y(y)) >= /\y.X(y) because [29], by (Abs) 29] mul*(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.mul(X(y), Y(y)), Z) >= Y(Z) because [34], by (Select) 34] mul(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [35], by (Star) 35] mul*(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [36], by (Select) 36] Y(D*(/\y.mul(X(y), Y(y)), Z)) >= Y(Z) because [37], by (Meta) 37] D*(/\y.mul(X(y), Y(y)), Z) >= Z because [32], by (Select) 38] D*(/\y.mul(X(y), Y(y)), Z) >= mul(X(Z), D(/\y.Y(y), Z)) because D > mul, [39] and [43], by (Copy) 39] D*(/\y.mul(X(y), Y(y)), Z) >= X(Z) because [40], by (Select) 40] mul(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [41], by (Star) 41] mul*(X(D*(/\y.mul(X(y), Y(y)), Z)), Y(D*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [42], by (Select) 42] X(D*(/\y.mul(X(y), Y(y)), Z)) >= X(Z) because [37], by (Meta) 43] D*(/\y.mul(X(y), Y(y)), Z) >= D(/\y.Y(y), Z) because D in Mul, [44] and [32], by (Stat) 44] /\y.mul(X(y), Y(y)) > /\y.Y(y) because [45], by definition 45] /\z.mul*(X(z), Y(z)) >= /\z.Y(z) because [46], by (Abs) 46] mul*(X(y), Y(y)) >= Y(y) because [47], by (Select) 47] Y(y) >= Y(y) because [48], by (Meta) 48] y >= y by (Var) 49] D(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) because [50], by (Star) 50] D*(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) because D > mul, [51] and [54], by (Copy) 51] D*(/\x.sin(X(x)), Y) >= cos(Y) because D > cos and [52], by (Copy) 52] D*(/\x.sin(X(x)), Y) >= Y because [53], by (Select) 53] Y >= Y by (Meta) 54] D*(/\x.sin(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [55] and [60], by (Stat) 55] /\x.sin(X(x)) > /\x.X(x) because [56], by definition 56] /\y.sin*(X(y)) >= /\y.X(y) because [57], by (Abs) 57] sin*(X(x)) >= X(x) because [58], by (Select) 58] X(x) >= X(x) because [59], by (Meta) 59] x >= x by (Var) 60] Y >= Y by (Meta) 61] D(/\x.cos(X(x)), Y) >= mul(sin(Y), D(/\x.X(x), Y)) because [62], by (Star) 62] D*(/\x.cos(X(x)), Y) >= mul(sin(Y), D(/\x.X(x), Y)) because D > mul, [63] and [66], by (Copy) 63] D*(/\x.cos(X(x)), Y) >= sin(Y) because D > sin and [64], by (Copy) 64] D*(/\x.cos(X(x)), Y) >= Y because [65], by (Select) 65] Y >= Y by (Meta) 66] D*(/\x.cos(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [67] and [72], by (Stat) 67] /\x.cos(X(x)) > /\x.X(x) because [68], by definition 68] /\y.cos*(X(y)) >= /\y.X(y) because [69], by (Abs) 69] cos*(X(x)) >= X(x) because [70], by (Select) 70] X(x) >= X(x) because [71], by (Meta) 71] x >= x by (Var) 72] Y >= Y by (Meta) We can thus remove the following rules: 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))) 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.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]] = _|_ [[min(x_1)]] = x_1 We choose Lex = {} and Mul = {D, cos, mul, sin}, and the following precedence: D > cos > sin > mul 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.X(x), Y) >= D(/\x.X(x), Y) 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)) With these choices, we have: 1] D(/\x.X, Y) >= _|_ by (Bot) 2] D(/\x.x, X) > _|_ because [3], by definition 3] D*(/\x.x, X) >= _|_ by (Bot) 4] D(/\x.X(x), Y) >= D(/\x.X(x), Y) because D in Mul, [5] and [8], by (Fun) 5] /\y.X(y) >= /\y.X(y) because [6], by (Abs) 6] X(x) >= X(x) because [7], by (Meta) 7] x >= x by (Var) 8] Y >= Y by (Meta) 9] D(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) because [10], by (Star) 10] D*(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) because D > mul, [11] and [14], by (Copy) 11] D*(/\x.sin(X(x)), Y) >= cos(Y) because D > cos and [12], by (Copy) 12] D*(/\x.sin(X(x)), Y) >= Y because [13], by (Select) 13] Y >= Y by (Meta) 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.cos(X(x)), Y) >= mul(sin(Y), D(/\x.X(x), Y)) because [22], by (Star) 22] D*(/\x.cos(X(x)), Y) >= mul(sin(Y), D(/\x.X(x), Y)) because D > mul, [23] and [26], by (Copy) 23] D*(/\x.cos(X(x)), Y) >= sin(Y) because D > sin and [24], by (Copy) 24] D*(/\x.cos(X(x)), Y) >= Y because [25], by (Select) 25] Y >= Y by (Meta) 26] D*(/\x.cos(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [27] and [32], by (Stat) 27] /\x.cos(X(x)) > /\x.X(x) because [28], by definition 28] /\y.cos*(X(y)) >= /\y.X(y) because [29], by (Abs) 29] cos*(X(x)) >= X(x) because [30], by (Select) 30] X(x) >= X(x) because [31], by (Meta) 31] x >= x by (Var) 32] Y >= Y by (Meta) We can thus remove the following rules: D(/\x.x, X) => 1 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.min(X(x)), Y) >? min(D(/\y.X(y), Y)) 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]] = _|_ We choose Lex = {} and Mul = {D, cos, min, mul, sin}, and the following precedence: D > mul > min > 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.min(X(x)), Y) > min(D(/\x.X(x), Y)) 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.min(X(x)), Y) > min(D(/\x.X(x), Y)) because [3], by definition 3] D*(/\x.min(X(x)), Y) >= min(D(/\x.X(x), Y)) because D > min and [4], by (Copy) 4] D*(/\x.min(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [5] and [10], by (Stat) 5] /\x.min(X(x)) > /\x.X(x) because [6], by definition 6] /\y.min*(X(y)) >= /\y.X(y) because [7], by (Abs) 7] min*(X(x)) >= X(x) because [8], by (Select) 8] X(x) >= X(x) because [9], by (Meta) 9] x >= x by (Var) 10] Y >= Y by (Meta) 11] D(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) because [12], by (Star) 12] D*(/\x.sin(X(x)), Y) >= mul(cos(Y), D(/\x.X(x), Y)) because D > mul, [13] and [16], by (Copy) 13] D*(/\x.sin(X(x)), Y) >= cos(Y) because D > cos and [14], by (Copy) 14] D*(/\x.sin(X(x)), Y) >= Y because [15], by (Select) 15] Y >= Y by (Meta) 16] D*(/\x.sin(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [17] and [22], by (Stat) 17] /\x.sin(X(x)) > /\x.X(x) because [18], by definition 18] /\y.sin*(X(y)) >= /\y.X(y) because [19], by (Abs) 19] sin*(X(x)) >= X(x) because [20], by (Select) 20] X(x) >= X(x) because [21], by (Meta) 21] x >= x by (Var) 22] Y >= Y by (Meta) 23] D(/\x.cos(X(x)), Y) > mul(min(sin(Y)), D(/\x.X(x), Y)) because [24], by definition 24] D*(/\x.cos(X(x)), Y) >= mul(min(sin(Y)), D(/\x.X(x), Y)) because D > mul, [25] and [29], by (Copy) 25] D*(/\x.cos(X(x)), Y) >= min(sin(Y)) because D > min and [26], by (Copy) 26] D*(/\x.cos(X(x)), Y) >= sin(Y) because D > sin and [27], by (Copy) 27] D*(/\x.cos(X(x)), Y) >= Y because [28], by (Select) 28] Y >= Y by (Meta) 29] D*(/\x.cos(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [30] and [35], by (Stat) 30] /\x.cos(X(x)) > /\x.X(x) because [31], by definition 31] /\y.cos*(X(y)) >= /\y.X(y) because [32], by (Abs) 32] cos*(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) We can thus remove the following rules: D(/\x.min(X(x)), Y) => min(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.sin(X(x)), Y) >? mul(cos(Y), D(/\y.X(y), Y)) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[cos(x_1)]] = x_1 We choose Lex = {} and Mul = {D, mul, sin}, and the following precedence: D > sin > mul 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.sin(X(x)), Y) >= mul(Y, D(/\x.X(x), Y)) With these choices, we have: 1] D(/\x.X, Y) > _|_ because [2], by definition 2] D*(/\x.X, Y) >= _|_ by (Bot) 3] D(/\x.sin(X(x)), Y) >= mul(Y, D(/\x.X(x), Y)) because [4], by (Star) 4] D*(/\x.sin(X(x)), Y) >= mul(Y, D(/\x.X(x), Y)) because D > mul, [5] and [7], by (Copy) 5] D*(/\x.sin(X(x)), Y) >= Y because [6], by (Select) 6] Y >= Y by (Meta) 7] D*(/\x.sin(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [8] and [13], by (Stat) 8] /\x.sin(X(x)) > /\x.X(x) because [9], by definition 9] /\y.sin*(X(y)) >= /\y.X(y) because [10], by (Abs) 10] sin*(X(x)) >= X(x) because [11], by (Select) 11] X(x) >= X(x) because [12], by (Meta) 12] x >= x by (Var) 13] Y >= Y by (Meta) We can thus remove the following rules: D(/\x.X, Y) => 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(/\x.sin(X(x)), Y) >? mul(cos(Y), D(/\y.X(y), Y)) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[cos(x_1)]] = x_1 We choose Lex = {} and Mul = {D, mul, sin}, and the following precedence: sin > D > mul Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: D(/\x.sin(X(x)), Y) > mul(Y, D(/\x.X(x), Y)) With these choices, we have: 1] D(/\x.sin(X(x)), Y) > mul(Y, D(/\x.X(x), Y)) because [2], by definition 2] D*(/\x.sin(X(x)), Y) >= mul(Y, D(/\x.X(x), Y)) because D > mul, [3] and [5], by (Copy) 3] D*(/\x.sin(X(x)), Y) >= Y because [4], by (Select) 4] Y >= Y by (Meta) 5] D*(/\x.sin(X(x)), Y) >= D(/\x.X(x), Y) because D in Mul, [6] and [11], by (Stat) 6] /\x.sin(X(x)) > /\x.X(x) because [7], by definition 7] /\y.sin*(X(y)) >= /\y.X(y) because [8], by (Abs) 8] sin*(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) We can thus remove the following rules: D(/\x.sin(X(x)), Y) => mul(cos(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.