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