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: [[0]] = _|_ [[1]] = _|_ [[minus(x_1)]] = x_1 We choose Lex = {} and Mul = {cos, d, plus, sin, star}, and the following precedence: d > plus > star > 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.X(x), Y) >= 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(sin(Y), d(/\x.X(x), Y)) _|_ >= _|_ star(_|_, X) >= _|_ star(X, _|_) >= _|_ plus(_|_, X) >= X 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.plus(X(x), Y(x)), Z) > plus(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because [9], by definition 9] d*(/\x.plus(X(x), Y(x)), Z) >= plus(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because d > plus, [10] and [17], by (Copy) 10] d*(/\x.plus(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [11] and [16], by (Stat) 11] /\x.plus(X(x), Y(x)) > /\x.X(x) because [12], by definition 12] /\y.plus*(X(y), Y(y)) >= /\y.X(y) because [13], by (Abs) 13] plus*(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.plus(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because d in Mul, [18] and [16], by (Stat) 18] /\y.plus(X(y), Y(y)) > /\y.Y(y) because [19], by definition 19] /\z.plus*(X(z), Y(z)) >= /\z.Y(z) because [20], by (Abs) 20] plus*(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.star(X(x), Y(x)), Z) >= plus(star(d(/\x.X(x), Z), Y(Z)), star(X(Z), d(/\y.Y(y), Z))) because [24], by (Star) 24] 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, [25] and [38], by (Copy) 25] d*(/\x.star(X(x), Y(x)), Z) >= star(d(/\x.X(x), Z), Y(Z)) because d > star, [26] and [33], by (Copy) 26] d*(/\x.star(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [27] and [32], by (Stat) 27] /\x.star(X(x), Y(x)) > /\x.X(x) because [28], by definition 28] /\y.star*(X(y), Y(y)) >= /\y.X(y) because [29], by (Abs) 29] star*(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.star(X(y), Y(y)), Z) >= Y(Z) because [34], by (Select) 34] star(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= Y(Z) because [35], by (Star) 35] star*(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= Y(Z) because [36], by (Select) 36] Y(d*(/\y.star(X(y), Y(y)), Z)) >= Y(Z) because [37], by (Meta) 37] d*(/\y.star(X(y), Y(y)), Z) >= Z because [32], by (Select) 38] d*(/\y.star(X(y), Y(y)), Z) >= star(X(Z), d(/\y.Y(y), Z)) because d > star, [39] and [43], by (Copy) 39] d*(/\y.star(X(y), Y(y)), Z) >= X(Z) because [40], by (Select) 40] star(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= X(Z) because [41], by (Star) 41] star*(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= X(Z) because [42], by (Select) 42] X(d*(/\y.star(X(y), Y(y)), Z)) >= X(Z) because [37], by (Meta) 43] d*(/\y.star(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because d in Mul, [44] and [32], by (Stat) 44] /\y.star(X(y), Y(y)) > /\y.Y(y) because [45], by definition 45] /\z.star*(X(z), Y(z)) >= /\z.Y(z) because [46], by (Abs) 46] star*(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) >= star(cos(Y), d(/\x.X(x), Y)) because [50], by (Star) 50] d*(/\x.sin(X(x)), Y) >= star(cos(Y), d(/\x.X(x), Y)) because d > star, [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) > star(sin(Y), d(/\x.X(x), Y)) because [62], by definition 62] d*(/\x.cos(X(x)), Y) >= star(sin(Y), d(/\x.X(x), Y)) because d > star, [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) 73] _|_ >= _|_ by (Bot) 74] star(_|_, X) >= _|_ by (Bot) 75] star(X, _|_) >= _|_ by (Bot) 76] plus(_|_, X) >= X because [77], by (Star) 77] plus*(_|_, X) >= X because [78], by (Select) 78] X >= X by (Meta) We can thus remove the following rules: d(/\x.plus(X(x), Y(x)), Z) => plus(d(/\y.X(y), Z), d(/\z.Y(z), Z)) 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, Y) >? 0 d(/\x.x, X) >? 1 d(/\x.minus(X(x)), Y) >? minus(d(/\y.X(y), Y)) 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)) 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: [[0]] = _|_ [[1]] = _|_ [[cos(x_1)]] = x_1 We choose Lex = {} and Mul = {d, minus, plus, sin, star}, and the following precedence: d > minus > plus > sin > star 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.minus(X(x)), Y) > minus(d(/\x.X(x), Y)) 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(Y, d(/\x.X(x), Y)) minus(_|_) >= _|_ star(_|_, X) >= _|_ star(X, _|_) >= _|_ plus(_|_, X) > X With these choices, we have: 1] d(/\x.X, Y) >= _|_ by (Bot) 2] d(/\x.x, X) >= _|_ by (Bot) 3] d(/\x.minus(X(x)), Y) > minus(d(/\x.X(x), Y)) because [4], by definition 4] d*(/\x.minus(X(x)), Y) >= minus(d(/\x.X(x), Y)) because d > minus and [5], by (Copy) 5] d*(/\x.minus(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [6] and [11], by (Stat) 6] /\x.minus(X(x)) > /\x.X(x) because [7], by definition 7] /\y.minus*(X(y)) >= /\y.X(y) because [8], by (Abs) 8] minus*(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.star(X(x), Y(x)), Z) >= plus(star(d(/\x.X(x), Z), Y(Z)), star(X(Z), d(/\y.Y(y), Z))) because [13], by (Star) 13] 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, [14] and [27], by (Copy) 14] d*(/\x.star(X(x), Y(x)), Z) >= star(d(/\x.X(x), Z), Y(Z)) because d > star, [15] and [22], by (Copy) 15] d*(/\x.star(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [16] and [21], by (Stat) 16] /\x.star(X(x), Y(x)) > /\x.X(x) because [17], by definition 17] /\y.star*(X(y), Y(y)) >= /\y.X(y) because [18], by (Abs) 18] star*(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.star(X(y), Y(y)), Z) >= Y(Z) because [23], by (Select) 23] star(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= Y(Z) because [24], by (Star) 24] star*(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= Y(Z) because [25], by (Select) 25] Y(d*(/\y.star(X(y), Y(y)), Z)) >= Y(Z) because [26], by (Meta) 26] d*(/\y.star(X(y), Y(y)), Z) >= Z because [21], by (Select) 27] d*(/\y.star(X(y), Y(y)), Z) >= star(X(Z), d(/\y.Y(y), Z)) because d > star, [28] and [32], by (Copy) 28] d*(/\y.star(X(y), Y(y)), Z) >= X(Z) because [29], by (Select) 29] star(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= X(Z) because [30], by (Star) 30] star*(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= X(Z) because [31], by (Select) 31] X(d*(/\y.star(X(y), Y(y)), Z)) >= X(Z) because [26], by (Meta) 32] d*(/\y.star(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because d in Mul, [33] and [21], by (Stat) 33] /\y.star(X(y), Y(y)) > /\y.Y(y) because [34], by definition 34] /\z.star*(X(z), Y(z)) >= /\z.Y(z) because [35], by (Abs) 35] star*(X(y), Y(y)) >= Y(y) because [36], by (Select) 36] Y(y) >= Y(y) because [37], by (Meta) 37] y >= y by (Var) 38] d(/\x.sin(X(x)), Y) >= star(Y, d(/\x.X(x), Y)) because [39], by (Star) 39] d*(/\x.sin(X(x)), Y) >= star(Y, d(/\x.X(x), Y)) because d > star, [40] and [42], by (Copy) 40] d*(/\x.sin(X(x)), Y) >= Y because [41], by (Select) 41] Y >= Y by (Meta) 42] d*(/\x.sin(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [43] and [48], by (Stat) 43] /\x.sin(X(x)) > /\x.X(x) because [44], by definition 44] /\y.sin*(X(y)) >= /\y.X(y) because [45], by (Abs) 45] sin*(X(x)) >= X(x) because [46], by (Select) 46] X(x) >= X(x) because [47], by (Meta) 47] x >= x by (Var) 48] Y >= Y by (Meta) 49] minus(_|_) >= _|_ by (Bot) 50] star(_|_, X) >= _|_ by (Bot) 51] star(X, _|_) >= _|_ by (Bot) 52] plus(_|_, X) > X because [53], by definition 53] plus*(_|_, X) >= X because [54], by (Select) 54] X >= X by (Meta) We can thus remove the following rules: d(/\x.minus(X(x)), Y) => minus(d(/\y.X(y), Y)) 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.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)) minus(0) >? 0 star(0, X) >? 0 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, plus, sin, star}, and the following precedence: sin > d > cos > plus > star 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.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)) _|_ >= _|_ star(_|_, X) >= _|_ star(X, _|_) >= _|_ With these choices, we have: 1] d(/\x.X, Y) >= _|_ by (Bot) 2] d(/\x.x, X) >= _|_ by (Bot) 3] 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 [4], by (Star) 4] 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, [5] and [18], by (Copy) 5] d*(/\x.star(X(x), Y(x)), Z) >= star(d(/\x.X(x), Z), Y(Z)) because d > star, [6] and [13], by (Copy) 6] d*(/\x.star(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [7] and [12], by (Stat) 7] /\x.star(X(x), Y(x)) > /\x.X(x) because [8], by definition 8] /\y.star*(X(y), Y(y)) >= /\y.X(y) because [9], by (Abs) 9] star*(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.star(X(y), Y(y)), Z) >= Y(Z) because [14], by (Select) 14] star(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= Y(Z) because [15], by (Star) 15] star*(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= Y(Z) because [16], by (Select) 16] Y(d*(/\y.star(X(y), Y(y)), Z)) >= Y(Z) because [17], by (Meta) 17] d*(/\y.star(X(y), Y(y)), Z) >= Z because [12], by (Select) 18] d*(/\y.star(X(y), Y(y)), Z) >= star(X(Z), d(/\y.Y(y), Z)) because d > star, [19] and [23], by (Copy) 19] d*(/\y.star(X(y), Y(y)), Z) >= X(Z) because [20], by (Select) 20] star(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= X(Z) because [21], by (Star) 21] star*(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= X(Z) because [22], by (Select) 22] X(d*(/\y.star(X(y), Y(y)), Z)) >= X(Z) because [17], by (Meta) 23] d*(/\y.star(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because d in Mul, [24] and [12], by (Stat) 24] /\y.star(X(y), Y(y)) > /\y.Y(y) because [25], by definition 25] /\z.star*(X(z), Y(z)) >= /\z.Y(z) because [26], by (Abs) 26] star*(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.sin(X(x)), Y) > star(cos(Y), d(/\x.X(x), Y)) because [30], by definition 30] d*(/\x.sin(X(x)), Y) >= star(cos(Y), d(/\x.X(x), Y)) because d > star, [31] and [34], by (Copy) 31] d*(/\x.sin(X(x)), Y) >= cos(Y) because d > cos and [32], by (Copy) 32] d*(/\x.sin(X(x)), Y) >= Y because [33], by (Select) 33] Y >= Y by (Meta) 34] d*(/\x.sin(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [35] and [40], by (Stat) 35] /\x.sin(X(x)) > /\x.X(x) because [36], by definition 36] /\y.sin*(X(y)) >= /\y.X(y) because [37], by (Abs) 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] _|_ >= _|_ by (Bot) 42] star(_|_, X) >= _|_ by (Bot) 43] star(X, _|_) >= _|_ by (Bot) We can thus remove the following rules: d(/\x.sin(X(x)), Y) => star(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.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 star(X, 0) >? 0 We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[1]] = _|_ We choose Lex = {} and Mul = {d, minus, plus, star}, and the following precedence: minus > d > plus > star 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.star(X(x), Y(x)), Z) > plus(star(d(/\x.X(x), Z), Y(Z)), star(X(Z), d(/\y.Y(y), Z))) minus(_|_) >= _|_ star(_|_, X) >= _|_ star(X, _|_) >= _|_ With these choices, we have: 1] d(/\x.X, Y) >= _|_ by (Bot) 2] d(/\x.x, X) >= _|_ by (Bot) 3] 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 [4], by definition 4] 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, [5] and [18], by (Copy) 5] d*(/\x.star(X(x), Y(x)), Z) >= star(d(/\x.X(x), Z), Y(Z)) because d > star, [6] and [13], by (Copy) 6] d*(/\x.star(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [7] and [12], by (Stat) 7] /\x.star(X(x), Y(x)) > /\x.X(x) because [8], by definition 8] /\y.star*(X(y), Y(y)) >= /\y.X(y) because [9], by (Abs) 9] star*(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.star(X(y), Y(y)), Z) >= Y(Z) because [14], by (Select) 14] star(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= Y(Z) because [15], by (Star) 15] star*(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= Y(Z) because [16], by (Select) 16] Y(d*(/\y.star(X(y), Y(y)), Z)) >= Y(Z) because [17], by (Meta) 17] d*(/\y.star(X(y), Y(y)), Z) >= Z because [12], by (Select) 18] d*(/\y.star(X(y), Y(y)), Z) >= star(X(Z), d(/\y.Y(y), Z)) because d > star, [19] and [23], by (Copy) 19] d*(/\y.star(X(y), Y(y)), Z) >= X(Z) because [20], by (Select) 20] star(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= X(Z) because [21], by (Star) 21] star*(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= X(Z) because [22], by (Select) 22] X(d*(/\y.star(X(y), Y(y)), Z)) >= X(Z) because [17], by (Meta) 23] d*(/\y.star(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because d in Mul, [24] and [12], by (Stat) 24] /\y.star(X(y), Y(y)) > /\y.Y(y) because [25], by definition 25] /\z.star*(X(z), Y(z)) >= /\z.Y(z) because [26], by (Abs) 26] star*(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] minus(_|_) >= _|_ by (Bot) 30] star(_|_, X) >= _|_ by (Bot) 31] star(X, _|_) >= _|_ by (Bot) We can thus remove the following rules: 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))) 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 minus(0) >? 0 star(0, X) >? 0 star(X, 0) >? 0 We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 0 1 = 0 d = \G0y1.3 + y1 + G0(0) minus = \y0.3 + 3y0 star = \y0y1.3 + 3y0 + 3y1 Using this interpretation, the requirements translate to: [[d(/\x._x0, _x1)]] = 3 + x0 + x1 > 0 = [[0]] [[d(/\x.x, _x0)]] = 3 + x0 > 0 = [[1]] [[minus(0)]] = 3 > 0 = [[0]] [[star(0, _x0)]] = 3 + 3x0 > 0 = [[0]] [[star(_x0, 0)]] = 3 + 3x0 > 0 = [[0]] We can thus remove the following rules: d(/\x.X, Y) => 0 d(/\x.x, X) => 1 minus(0) => 0 star(0, X) => 0 star(X, 0) => 0 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.