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 observe that the rules contain a first-order subset: minus(0) => 0 star(0, X) => 0 star(X, 0) => 0 plus(0, X) => X Moreover, the system is finitely branching. Thus, by [Kop12, Thm. 7.55], we may omit all first-order dependency pairs from the dependency pair problem (DP(R), R) if this first-order part is Ce-terminating when seen as a many-sorted first-order TRS. According to the external first-order termination prover, this system is indeed Ce-terminating: || proof of resources/system.trs || # AProVE Commit ID: d84c10301d352dfd14de2104819581f4682260f5 fuhs 20130616 || || || Termination w.r.t. Q of the given QTRS could be proven: || || (0) QTRS || (1) QTRSRRRProof [EQUIVALENT] || (2) QTRS || (3) RisEmptyProof [EQUIVALENT] || (4) YES || || || ---------------------------------------- || || (0) || Obligation: || Q restricted rewrite system: || The TRS R consists of the following rules: || || minus(0) -> 0 || star(0, %X) -> 0 || star(%X, 0) -> 0 || plus(0, %X) -> %X || ~PAIR(%X, %Y) -> %X || ~PAIR(%X, %Y) -> %Y || || Q is empty. || || ---------------------------------------- || || (1) QTRSRRRProof (EQUIVALENT) || Used ordering: || Polynomial interpretation [POLO]: || || POL(0) = 1 || POL(minus(x_1)) = 2 + 2*x_1 || POL(plus(x_1, x_2)) = 2 + x_1 + x_2 || POL(star(x_1, x_2)) = 2 + 2*x_1 + 2*x_2 || POL(~PAIR(x_1, x_2)) = 2 + x_1 + x_2 || With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly: || || minus(0) -> 0 || star(0, %X) -> 0 || star(%X, 0) -> 0 || plus(0, %X) -> %X || ~PAIR(%X, %Y) -> %X || ~PAIR(%X, %Y) -> %Y || || || || || ---------------------------------------- || || (2) || Obligation: || Q restricted rewrite system: || R is empty. || Q is empty. || || ---------------------------------------- || || (3) RisEmptyProof (EQUIVALENT) || The TRS R is empty. Hence, termination is trivially proven. || ---------------------------------------- || || (4) || YES || 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.minus(X(x)), Y) =#> minus#(d(/\y.X(y), Y)) 1] d#(/\x.minus(X(x)), Y) =#> d#(/\y.X(y), Y) 2] d#(/\x.minus(X(x)), Y) =#> X(y) 3] d#(/\x.plus(X(x), Y(x)), Z) =#> plus#(d(/\y.X(y), Z), d(/\z.Y(z), Z)) 4] d#(/\x.plus(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) 5] d#(/\x.plus(X(x), Y(x)), Z) =#> X(y) 6] d#(/\x.plus(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z) 7] d#(/\x.plus(X(x), Y(x)), Z) =#> Y(y) 8] 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))) 9] d#(/\x.star(X(x), Y(x)), Z) =#> star#(d(/\y.X(y), Z), Y(Z)) 10] d#(/\x.star(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) 11] d#(/\x.star(X(x), Y(x)), Z) =#> X(y) 12] d#(/\x.star(X(x), Y(x)), Z) =#> Y(Z) 13] d#(/\x.star(X(x), Y(x)), Z) =#> star#(X(Z), d(/\y.Y(y), Z)) 14] d#(/\x.star(X(x), Y(x)), Z) =#> X(Z) 15] d#(/\x.star(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z) 16] d#(/\x.star(X(x), Y(x)), Z) =#> Y(y) 17] d#(/\x.sin(X(x)), Y) =#> star#(cos(Y), d(/\y.X(y), Y)) 18] d#(/\x.sin(X(x)), Y) =#> d#(/\y.X(y), Y) 19] d#(/\x.sin(X(x)), Y) =#> X(y) 20] d#(/\x.cos(X(x)), Y) =#> star#(minus(sin(Y)), d(/\y.X(y), Y)) 21] d#(/\x.cos(X(x)), Y) =#> minus#(sin(Y)) 22] d#(/\x.cos(X(x)), Y) =#> d#(/\y.X(y), Y) 23] d#(/\x.cos(X(x)), Y) =#> X(y) Rules R_0: 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 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 place the elements of P in a dependency graph approximation G (see e.g. [Kop12, Thm. 7.27, 7.29], as follows: * 0 : * 1 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 * 2 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 * 3 : * 4 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 * 5 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 * 6 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 * 7 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 * 8 : * 9 : * 10 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 * 11 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 * 12 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 * 13 : * 14 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 * 15 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 * 16 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 * 17 : * 18 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 * 19 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 * 20 : * 21 : * 22 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 * 23 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 This graph has the following strongly connected components: P_1: d#(/\x.minus(X(x)), Y) =#> d#(/\y.X(y), Y) d#(/\x.minus(X(x)), Y) =#> X(y) d#(/\x.plus(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) d#(/\x.plus(X(x), Y(x)), Z) =#> X(y) d#(/\x.plus(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z) d#(/\x.plus(X(x), Y(x)), Z) =#> Y(y) d#(/\x.star(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) d#(/\x.star(X(x), Y(x)), Z) =#> X(y) d#(/\x.star(X(x), Y(x)), Z) =#> Y(Z) d#(/\x.star(X(x), Y(x)), Z) =#> X(Z) d#(/\x.star(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z) d#(/\x.star(X(x), Y(x)), Z) =#> Y(y) d#(/\x.sin(X(x)), Y) =#> d#(/\y.X(y), Y) d#(/\x.sin(X(x)), Y) =#> X(y) d#(/\x.cos(X(x)), Y) =#> d#(/\y.X(y), Y) d#(/\x.cos(X(x)), Y) =#> X(y) By [Kop12, Thm. 7.31], we may replace any dependency pair problem (P_0, R_0, m, f) by (P_1, R_0, m, f). 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.minus(X(x)), Y) >? d#(/\y.X(y), Y) d#(/\x.minus(X(x)), Y) >? X(~c0) d#(/\x.plus(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) d#(/\x.plus(X(x), Y(x)), Z) >? X(~c1) d#(/\x.plus(X(x), Y(x)), Z) >? d#(/\y.Y(y), Z) d#(/\x.plus(X(x), Y(x)), Z) >? Y(~c2) d#(/\x.star(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) d#(/\x.star(X(x), Y(x)), Z) >? X(~c3) d#(/\x.star(X(x), Y(x)), Z) >? Y(Z) d#(/\x.star(X(x), Y(x)), Z) >? X(Z) d#(/\x.star(X(x), Y(x)), Z) >? d#(/\y.Y(y), Z) d#(/\x.star(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.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 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]] = _|_ [[d(x_1, x_2)]] = d(x_2, x_1) [[minus(x_1)]] = x_1 [[~c0]] = _|_ [[~c1]] = _|_ [[~c2]] = _|_ [[~c3]] = _|_ [[~c4]] = _|_ [[~c5]] = _|_ [[~c6]] = _|_ We choose Lex = {d} and Mul = {cos, d#, plus, sin, star}, and the following precedence: d > cos > d# > 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(x), Y) >= d#(/\x.X(x), Y) d#(/\x.X(x), Y) >= X(_|_) d#(/\x.plus(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) d#(/\x.plus(X(x), Y(x)), Z) >= X(_|_) d#(/\x.plus(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) d#(/\x.plus(X(x), Y(x)), Z) >= Y(_|_) d#(/\x.star(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) d#(/\x.star(X(x), Y(x)), Z) > X(_|_) d#(/\x.star(X(x), Y(x)), Z) > Y(Z) d#(/\x.star(X(x), Y(x)), Z) >= X(Z) d#(/\x.star(X(x), Y(x)), Z) > d#(/\x.Y(x), Z) d#(/\x.star(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.plus(X(x), Y(x)), Z) >= plus(d, d (/\x.Y(x)) Z) d(/\x.star(X(x), Y(x)), Z) >= plus(star(d, Y(Z)), star(X(Z), d (/\x.Y(x)) 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 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.plus(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because d# in Mul, [11] and [16], by (Fun) 11] /\y.plus(X(y), Y(y)) >= /\y.X(y) because [12], by (Abs) 12] plus(X(x), Y(x)) >= X(x) because [13], by (Star) 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#(/\x.plus(X(x), Y(x)), Z) >= X(_|_) because [18], by (Star) 18] d#*(/\x.plus(X(x), Y(x)), Z) >= X(_|_) because [19], by (Select) 19] plus(X(d#*(/\x.plus(X(x), Y(x)), Z)), Y(d#*(/\y.plus(X(y), Y(y)), Z))) >= X(_|_) because [20], by (Star) 20] plus*(X(d#*(/\x.plus(X(x), Y(x)), Z)), Y(d#*(/\y.plus(X(y), Y(y)), Z))) >= X(_|_) because [21], by (Select) 21] X(d#*(/\x.plus(X(x), Y(x)), Z)) >= X(_|_) because [22], by (Meta) 22] d#*(/\x.plus(X(x), Y(x)), Z) >= _|_ by (Bot) 23] d#(/\x.plus(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) because d# in Mul, [24] and [16], by (Fun) 24] /\y.plus(X(y), Y(y)) >= /\y.Y(y) because [25], by (Abs) 25] plus(X(x), Y(x)) >= Y(x) because [26], by (Star) 26] plus*(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.plus(X(x), Y(x)), Z) >= Y(_|_) because [30], by (Star) 30] d#*(/\x.plus(X(x), Y(x)), Z) >= Y(_|_) because [31], by (Select) 31] plus(X(d#*(/\x.plus(X(x), Y(x)), Z)), Y(d#*(/\y.plus(X(y), Y(y)), Z))) >= Y(_|_) because [32], by (Star) 32] plus*(X(d#*(/\x.plus(X(x), Y(x)), Z)), Y(d#*(/\y.plus(X(y), Y(y)), Z))) >= Y(_|_) because [33], by (Select) 33] Y(d#*(/\x.plus(X(x), Y(x)), Z)) >= Y(_|_) because [34], by (Meta) 34] d#*(/\x.plus(X(x), Y(x)), Z) >= _|_ by (Bot) 35] d#(/\x.star(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because d# in Mul, [36] and [41], by (Fun) 36] /\y.star(X(y), Y(y)) >= /\y.X(y) because [37], by (Abs) 37] star(X(x), Y(x)) >= X(x) because [38], by (Star) 38] star*(X(x), Y(x)) >= X(x) because [39], by (Select) 39] X(x) >= X(x) because [40], by (Meta) 40] x >= x by (Var) 41] Z >= Z by (Meta) 42] d#(/\x.star(X(x), Y(x)), Z) > X(_|_) because [43], by definition 43] d#*(/\x.star(X(x), Y(x)), Z) >= X(_|_) because [44], by (Select) 44] star(X(d#*(/\x.star(X(x), Y(x)), Z)), Y(d#*(/\y.star(X(y), Y(y)), Z))) >= X(_|_) because [45], by (Star) 45] star*(X(d#*(/\x.star(X(x), Y(x)), Z)), Y(d#*(/\y.star(X(y), Y(y)), Z))) >= X(_|_) because [46], by (Select) 46] X(d#*(/\x.star(X(x), Y(x)), Z)) >= X(_|_) because [47], by (Meta) 47] d#*(/\x.star(X(x), Y(x)), Z) >= _|_ by (Bot) 48] d#(/\x.star(X(x), Y(x)), Z) > Y(Z) because [49], by definition 49] d#*(/\x.star(X(x), Y(x)), Z) >= Y(Z) because [50], by (Select) 50] star(X(d#*(/\x.star(X(x), Y(x)), Z)), Y(d#*(/\y.star(X(y), Y(y)), Z))) >= Y(Z) because [51], by (Star) 51] star*(X(d#*(/\x.star(X(x), Y(x)), Z)), Y(d#*(/\y.star(X(y), Y(y)), Z))) >= Y(Z) because [52], by (Select) 52] Y(d#*(/\x.star(X(x), Y(x)), Z)) >= Y(Z) because [53], by (Meta) 53] d#*(/\x.star(X(x), Y(x)), Z) >= Z because [41], by (Select) 54] d#(/\x.star(X(x), Y(x)), Z) >= X(Z) because [55], by (Star) 55] d#*(/\x.star(X(x), Y(x)), Z) >= X(Z) because [56], by (Select) 56] star(X(d#*(/\x.star(X(x), Y(x)), Z)), Y(d#*(/\y.star(X(y), Y(y)), Z))) >= X(Z) because [57], by (Star) 57] star*(X(d#*(/\x.star(X(x), Y(x)), Z)), Y(d#*(/\y.star(X(y), Y(y)), Z))) >= X(Z) because [58], by (Select) 58] X(d#*(/\x.star(X(x), Y(x)), Z)) >= X(Z) because [53], by (Meta) 59] d#(/\x.star(X(x), Y(x)), Z) > d#(/\x.Y(x), Z) because [60], by definition 60] d#*(/\x.star(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) because d# in Mul, [61] and [41], by (Stat) 61] /\x.star(X(x), Y(x)) > /\x.Y(x) because [62], by definition 62] /\y.star*(X(y), Y(y)) >= /\y.Y(y) because [63], by (Abs) 63] star*(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.star(X(x), Y(x)), Z) > Y(_|_) because [67], by definition 67] d#*(/\x.star(X(x), Y(x)), Z) >= Y(_|_) because [68], by (Select) 68] star(X(d#*(/\x.star(X(x), Y(x)), Z)), Y(d#*(/\y.star(X(y), Y(y)), Z))) >= Y(_|_) because [69], by (Star) 69] star*(X(d#*(/\x.star(X(x), Y(x)), Z)), Y(d#*(/\y.star(X(y), Y(y)), Z))) >= Y(_|_) because [70], by (Select) 70] Y(d#*(/\x.star(X(x), Y(x)), Z)) >= Y(_|_) because [71], by (Meta) 71] d#*(/\x.star(X(x), Y(x)), Z) >= _|_ by (Bot) 72] d#(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y) because [73], by (Star) 73] d#*(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y) because d# in Mul, [74] and [79], by (Stat) 74] /\x.sin(X(x)) > /\x.X(x) because [75], by definition 75] /\y.sin*(X(y)) >= /\y.X(y) because [76], by (Abs) 76] sin*(X(x)) >= X(x) because [77], by (Select) 77] X(x) >= X(x) because [78], by (Meta) 78] x >= x by (Var) 79] Y >= Y by (Meta) 80] d#(/\x.sin(X(x)), Y) >= X(_|_) because [81], by (Star) 81] d#*(/\x.sin(X(x)), Y) >= X(_|_) because [82], by (Select) 82] sin(X(d#*(/\x.sin(X(x)), Y))) >= X(_|_) because [83], by (Star) 83] sin*(X(d#*(/\x.sin(X(x)), Y))) >= X(_|_) because [84], by (Select) 84] X(d#*(/\x.sin(X(x)), Y)) >= X(_|_) because [85], by (Meta) 85] d#*(/\x.sin(X(x)), Y) >= _|_ by (Bot) 86] d#(/\x.cos(X(x)), Y) >= d#(/\x.X(x), Y) because [87], by (Star) 87] d#*(/\x.cos(X(x)), Y) >= d#(/\x.X(x), Y) because d# in Mul, [88] and [93], by (Stat) 88] /\x.cos(X(x)) > /\x.X(x) because [89], by definition 89] /\y.cos*(X(y)) >= /\y.X(y) because [90], by (Abs) 90] cos*(X(x)) >= X(x) because [91], by (Select) 91] X(x) >= X(x) because [92], by (Meta) 92] x >= x by (Var) 93] Y >= Y by (Meta) 94] d#(/\x.cos(X(x)), Y) >= X(_|_) because [95], by (Star) 95] d#*(/\x.cos(X(x)), Y) >= X(_|_) because [96], by (Select) 96] cos(X(d#*(/\x.cos(X(x)), Y))) >= X(_|_) because [97], by (Star) 97] cos*(X(d#*(/\x.cos(X(x)), Y))) >= X(_|_) because [98], by (Select) 98] X(d#*(/\x.cos(X(x)), Y)) >= X(_|_) because [99], by (Meta) 99] d#*(/\x.cos(X(x)), Y) >= _|_ by (Bot) 100] d(/\x.X, Y) >= _|_ by (Bot) 101] d(/\x.x, X) >= _|_ by (Bot) 102] d(/\x.X(x), Y) >= d(/\x.X(x), Y) because [2] and [5], by (Fun) 103] d(/\x.plus(X(x), Y(x)), Z) >= plus(d, d (/\x.Y(x)) Z) because [104], by (Star) 104] d*(/\x.plus(X(x), Y(x)), Z) >= plus(d, d (/\x.Y(x)) Z) because d > plus, [105] and [119], by (Copy) 105] d*(/\x.plus(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because [106], [16], [111] and [118], by (Stat) 106] /\x.plus(X(x), Y(x)) > /\x.X(x) because [107], by definition 107] /\y.plus*(X(y), Y(y)) >= /\y.X(y) because [108], by (Abs) 108] plus*(X(x), Y(x)) >= X(x) because [109], by (Select) 109] X(x) >= X(x) because [110], by (Meta) 110] x >= x by (Var) 111] d*(/\y.plus(X(y), Y(y)), Z) >= /\y.X(y) because [112], by (F-Abs) 112] d*(/\y.plus(X(y), Y(y)), Z, z) >= X(z) because [113], by (Select) 113] plus(X(d*(/\y.plus(X(y), Y(y)), Z, z)), Y(d*(/\u.plus(X(u), Y(u)), Z, z))) >= X(z) because [114], by (Star) 114] plus*(X(d*(/\y.plus(X(y), Y(y)), Z, z)), Y(d*(/\u.plus(X(u), Y(u)), Z, z))) >= X(z) because [115], by (Select) 115] X(d*(/\y.plus(X(y), Y(y)), Z, z)) >= X(z) because [116], by (Meta) 116] d*(/\y.plus(X(y), Y(y)), Z, z) >= z because [117], by (Select) 117] z >= z by (Var) 118] d*(/\y.plus(X(y), Y(y)), Z) >= Z because [16], by (Select) 119] d*(/\y.plus(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because [120], [16], [125] and [118], by (Stat) 120] /\y.plus(X(y), Y(y)) > /\y.Y(y) because [121], by definition 121] /\u.plus*(X(u), Y(u)) >= /\u.Y(u) because [122], by (Abs) 122] plus*(X(y), Y(y)) >= Y(y) because [123], by (Select) 123] Y(y) >= Y(y) because [124], by (Meta) 124] y >= y by (Var) 125] d*(/\u.plus(X(u), Y(u)), Z) >= /\u.Y(u) because [24], by (Select) 126] d(/\x.star(X(x), Y(x)), Z) >= plus(star(d, Y(Z)), star(X(Z), d (/\x.Y(x)) Z)) because [127], by (Star) 127] d*(/\x.star(X(x), Y(x)), Z) >= plus(star(d, Y(Z)), star(X(Z), d (/\x.Y(x)) Z)) because d > plus, [128] and [147], by (Copy) 128] d*(/\x.star(X(x), Y(x)), Z) >= star(d(/\x.X(x), Z), Y(Z)) because d > star, [129] and [143], by (Copy) 129] d*(/\x.star(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because [130], [41], [135] and [142], by (Stat) 130] /\x.star(X(x), Y(x)) > /\x.X(x) because [131], by definition 131] /\y.star*(X(y), Y(y)) >= /\y.X(y) because [132], by (Abs) 132] star*(X(x), Y(x)) >= X(x) because [133], by (Select) 133] X(x) >= X(x) because [134], by (Meta) 134] x >= x by (Var) 135] d*(/\y.star(X(y), Y(y)), Z) >= /\y.X(y) because [136], by (F-Abs) 136] d*(/\y.star(X(y), Y(y)), Z, z) >= X(z) because [137], by (Select) 137] star(X(d*(/\y.star(X(y), Y(y)), Z, z)), Y(d*(/\u.star(X(u), Y(u)), Z, z))) >= X(z) because [138], by (Star) 138] star*(X(d*(/\y.star(X(y), Y(y)), Z, z)), Y(d*(/\u.star(X(u), Y(u)), Z, z))) >= X(z) because [139], by (Select) 139] X(d*(/\y.star(X(y), Y(y)), Z, z)) >= X(z) because [140], by (Meta) 140] d*(/\y.star(X(y), Y(y)), Z, z) >= z because [141], by (Select) 141] z >= z by (Var) 142] d*(/\y.star(X(y), Y(y)), Z) >= Z because [41], by (Select) 143] d*(/\y.star(X(y), Y(y)), Z) >= Y(Z) because [144], by (Select) 144] star(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\u.star(X(u), Y(u)), Z))) >= Y(Z) because [145], by (Star) 145] star*(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\u.star(X(u), Y(u)), Z))) >= Y(Z) because [146], by (Select) 146] Y(d*(/\y.star(X(y), Y(y)), Z)) >= Y(Z) because [142], by (Meta) 147] d*(/\y.star(X(y), Y(y)), Z) >= star(X(Z), d(/\y.Y(y), Z)) because d > star, [148] and [152], by (Copy) 148] d*(/\y.star(X(y), Y(y)), Z) >= X(Z) because [149], by (Select) 149] star(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\u.star(X(u), Y(u)), Z))) >= X(Z) because [150], by (Star) 150] star*(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\u.star(X(u), Y(u)), Z))) >= X(Z) because [151], by (Select) 151] X(d*(/\y.star(X(y), Y(y)), Z)) >= X(Z) because [142], by (Meta) 152] d*(/\y.star(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because [61], [41], [153] and [142], by (Stat) 153] d*(/\y.star(X(y), Y(y)), Z) >= /\y.Y(y) because [154], by (Select) 154] /\u.star(X(u), Y(u)) >= /\u.Y(u) because [155], by (Abs) 155] star(X(y), Y(y)) >= Y(y) because [156], by (Star) 156] star*(X(y), Y(y)) >= Y(y) because [157], by (Select) 157] Y(y) >= Y(y) because [158], by (Meta) 158] y >= y by (Var) 159] d(/\x.sin(X(x)), Y) >= star(cos(Y), d(/\x.X(x), Y)) because [160], by (Star) 160] d*(/\x.sin(X(x)), Y) >= star(cos(Y), d(/\x.X(x), Y)) because d > star, [161] and [163], by (Copy) 161] d*(/\x.sin(X(x)), Y) >= cos(Y) because d > cos and [162], by (Copy) 162] d*(/\x.sin(X(x)), Y) >= Y because [79], by (Select) 163] d*(/\x.sin(X(x)), Y) >= d(/\x.X(x), Y) because [74], [79], [164] and [162], by (Stat) 164] d*(/\x.sin(X(x)), Y) >= /\x.X(x) because [165], by (Select) 165] /\y.sin(X(y)) >= /\y.X(y) because [166], by (Abs) 166] sin(X(x)) >= X(x) because [167], by (Star) 167] sin*(X(x)) >= X(x) because [168], by (Select) 168] X(x) >= X(x) because [169], by (Meta) 169] x >= x by (Var) 170] d(/\x.cos(X(x)), Y) >= star(sin(Y), d(/\x.X(x), Y)) because [171], by (Star) 171] d*(/\x.cos(X(x)), Y) >= star(sin(Y), d(/\x.X(x), Y)) because d > star, [172] and [174], by (Copy) 172] d*(/\x.cos(X(x)), Y) >= sin(Y) because d > sin and [173], by (Copy) 173] d*(/\x.cos(X(x)), Y) >= Y because [93], by (Select) 174] d*(/\x.cos(X(x)), Y) >= d(/\x.X(x), Y) because [88], [93], [175] and [173], by (Stat) 175] d*(/\x.cos(X(x)), Y) >= /\x.X(x) because [176], by (Select) 176] /\y.cos(X(y)) >= /\y.X(y) because [177], by (Abs) 177] cos(X(x)) >= X(x) because [178], by (Star) 178] cos*(X(x)) >= X(x) because [179], by (Select) 179] X(x) >= X(x) because [180], by (Meta) 180] x >= x by (Var) 181] _|_ >= _|_ by (Bot) 182] star(_|_, X) >= _|_ by (Bot) 183] star(X, _|_) >= _|_ by (Bot) 184] plus(_|_, X) >= X because [185], by (Star) 185] plus*(_|_, X) >= X because [186], by (Select) 186] X >= X by (Meta) 187] d(F, X) >= d#(F, X) because [188], by (Star) 188] d*(F, X) >= d#(F, X) because d > d#, [189] and [191], by (Copy) 189] d*(F, X) >= F because [190], by (Select) 190] F >= F by (Meta) 191] d*(F, X) >= X because [192], by (Select) 192] 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.minus(X(x)), Y) =#> d#(/\y.X(y), Y) d#(/\x.minus(X(x)), Y) =#> X(y) d#(/\x.plus(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) d#(/\x.plus(X(x), Y(x)), Z) =#> X(y) d#(/\x.plus(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z) d#(/\x.plus(X(x), Y(x)), Z) =#> Y(y) d#(/\x.star(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) d#(/\x.star(X(x), Y(x)), Z) =#> X(Z) d#(/\x.sin(X(x)), Y) =#> d#(/\y.X(y), Y) d#(/\x.sin(X(x)), Y) =#> X(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_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.minus(X(x)), Y) >? d#(/\y.X(y), Y) d#(/\x.minus(X(x)), Y) >? X(~c0) d#(/\x.plus(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) d#(/\x.plus(X(x), Y(x)), Z) >? X(~c1) d#(/\x.plus(X(x), Y(x)), Z) >? d#(/\y.Y(y), Z) d#(/\x.plus(X(x), Y(x)), Z) >? Y(~c2) d#(/\x.star(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) d#(/\x.star(X(x), Y(x)), Z) >? X(Z) d#(/\x.sin(X(x)), Y) >? d#(/\y.X(y), Y) d#(/\x.sin(X(x)), Y) >? X(~c3) d#(/\x.cos(X(x)), Y) >? d#(/\y.X(y), Y) d#(/\x.cos(X(x)), Y) >? X(~c4) 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 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]] = _|_ [[minus(x_1)]] = x_1 [[~c0]] = _|_ [[~c1]] = _|_ [[~c2]] = _|_ [[~c3]] = _|_ [[~c4]] = _|_ We choose Lex = {} and Mul = {cos, d, d#, plus, sin, star}, and the following precedence: d > cos > d# > sin > star > plus 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.plus(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) d#(/\x.plus(X(x), Y(x)), Z) > X(_|_) d#(/\x.plus(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) d#(/\x.plus(X(x), Y(x)), Z) >= Y(_|_) d#(/\x.star(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) d#(/\x.star(X(x), Y(x)), Z) > X(Z) 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.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 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.plus(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because d# in Mul, [11] and [16], by (Fun) 11] /\y.plus(X(y), Y(y)) >= /\y.X(y) because [12], by (Abs) 12] plus(X(x), Y(x)) >= X(x) because [13], by (Star) 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#(/\x.plus(X(x), Y(x)), Z) > X(_|_) because [18], by definition 18] d#*(/\x.plus(X(x), Y(x)), Z) >= X(_|_) because [19], by (Select) 19] plus(X(d#*(/\x.plus(X(x), Y(x)), Z)), Y(d#*(/\y.plus(X(y), Y(y)), Z))) >= X(_|_) because [20], by (Star) 20] plus*(X(d#*(/\x.plus(X(x), Y(x)), Z)), Y(d#*(/\y.plus(X(y), Y(y)), Z))) >= X(_|_) because [21], by (Select) 21] X(d#*(/\x.plus(X(x), Y(x)), Z)) >= X(_|_) because [22], by (Meta) 22] d#*(/\x.plus(X(x), Y(x)), Z) >= _|_ by (Bot) 23] d#(/\x.plus(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) because d# in Mul, [24] and [16], by (Fun) 24] /\y.plus(X(y), Y(y)) >= /\y.Y(y) because [25], by (Abs) 25] plus(X(x), Y(x)) >= Y(x) because [26], by (Star) 26] plus*(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.plus(X(x), Y(x)), Z) >= Y(_|_) because [30], by (Star) 30] d#*(/\x.plus(X(x), Y(x)), Z) >= Y(_|_) because [31], by (Select) 31] plus(X(d#*(/\x.plus(X(x), Y(x)), Z)), Y(d#*(/\y.plus(X(y), Y(y)), Z))) >= Y(_|_) because [32], by (Star) 32] plus*(X(d#*(/\x.plus(X(x), Y(x)), Z)), Y(d#*(/\y.plus(X(y), Y(y)), Z))) >= Y(_|_) because [33], by (Select) 33] Y(d#*(/\x.plus(X(x), Y(x)), Z)) >= Y(_|_) because [34], by (Meta) 34] d#*(/\x.plus(X(x), Y(x)), Z) >= _|_ by (Bot) 35] d#(/\x.star(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because d# in Mul, [36] and [41], by (Fun) 36] /\y.star(X(y), Y(y)) >= /\y.X(y) because [37], by (Abs) 37] star(X(x), Y(x)) >= X(x) because [38], by (Star) 38] star*(X(x), Y(x)) >= X(x) because [39], by (Select) 39] X(x) >= X(x) because [40], by (Meta) 40] x >= x by (Var) 41] Z >= Z by (Meta) 42] d#(/\x.star(X(x), Y(x)), Z) > X(Z) because [43], by definition 43] d#*(/\x.star(X(x), Y(x)), Z) >= X(Z) because [44], by (Select) 44] star(X(d#*(/\x.star(X(x), Y(x)), Z)), Y(d#*(/\y.star(X(y), Y(y)), Z))) >= X(Z) because [45], by (Star) 45] star*(X(d#*(/\x.star(X(x), Y(x)), Z)), Y(d#*(/\y.star(X(y), Y(y)), Z))) >= X(Z) because [46], by (Select) 46] X(d#*(/\x.star(X(x), Y(x)), Z)) >= X(Z) because [47], by (Meta) 47] d#*(/\x.star(X(x), Y(x)), Z) >= Z because [41], by (Select) 48] d#(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y) because [49], by (Star) 49] d#*(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y) because d# in Mul, [50] and [55], by (Stat) 50] /\x.sin(X(x)) > /\x.X(x) because [51], by definition 51] /\y.sin*(X(y)) >= /\y.X(y) because [52], by (Abs) 52] sin*(X(x)) >= X(x) because [53], by (Select) 53] X(x) >= X(x) because [54], by (Meta) 54] x >= x by (Var) 55] Y >= Y by (Meta) 56] d#(/\x.sin(X(x)), Y) > X(_|_) because [57], by definition 57] d#*(/\x.sin(X(x)), Y) >= X(_|_) because [58], by (Select) 58] sin(X(d#*(/\x.sin(X(x)), Y))) >= X(_|_) because [59], by (Star) 59] sin*(X(d#*(/\x.sin(X(x)), Y))) >= X(_|_) because [60], by (Select) 60] X(d#*(/\x.sin(X(x)), Y)) >= X(_|_) because [61], by (Meta) 61] d#*(/\x.sin(X(x)), Y) >= _|_ by (Bot) 62] d#(/\x.cos(X(x)), Y) >= d#(/\x.X(x), Y) because [63], by (Star) 63] d#*(/\x.cos(X(x)), Y) >= d#(/\x.X(x), Y) because d# in Mul, [64] and [69], by (Stat) 64] /\x.cos(X(x)) > /\x.X(x) because [65], by definition 65] /\y.cos*(X(y)) >= /\y.X(y) because [66], by (Abs) 66] cos*(X(x)) >= X(x) because [67], by (Select) 67] X(x) >= X(x) because [68], by (Meta) 68] x >= x by (Var) 69] Y >= Y by (Meta) 70] d#(/\x.cos(X(x)), Y) > X(_|_) because [71], by definition 71] d#*(/\x.cos(X(x)), Y) >= X(_|_) because [72], by (Select) 72] cos(X(d#*(/\x.cos(X(x)), Y))) >= X(_|_) because [73], by (Star) 73] cos*(X(d#*(/\x.cos(X(x)), Y))) >= X(_|_) because [74], by (Select) 74] X(d#*(/\x.cos(X(x)), Y)) >= X(_|_) because [75], by (Meta) 75] d#*(/\x.cos(X(x)), Y) >= _|_ by (Bot) 76] d(/\x.X, Y) >= _|_ by (Bot) 77] d(/\x.x, X) >= _|_ by (Bot) 78] d(/\x.X(x), Y) >= d(/\x.X(x), Y) because d in Mul, [2] and [5], by (Fun) 79] d(/\x.plus(X(x), Y(x)), Z) >= plus(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because [80], by (Star) 80] d*(/\x.plus(X(x), Y(x)), Z) >= plus(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because d > plus, [81] and [87], by (Copy) 81] d*(/\x.plus(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [82] and [16], by (Stat) 82] /\x.plus(X(x), Y(x)) > /\x.X(x) because [83], by definition 83] /\y.plus*(X(y), Y(y)) >= /\y.X(y) because [84], by (Abs) 84] plus*(X(x), Y(x)) >= X(x) because [85], by (Select) 85] X(x) >= X(x) because [86], by (Meta) 86] x >= x by (Var) 87] d*(/\y.plus(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because d in Mul, [88] and [16], by (Stat) 88] /\y.plus(X(y), Y(y)) > /\y.Y(y) because [89], by definition 89] /\z.plus*(X(z), Y(z)) >= /\z.Y(z) because [90], by (Abs) 90] plus*(X(y), Y(y)) >= Y(y) because [91], by (Select) 91] Y(y) >= Y(y) because [92], by (Meta) 92] y >= y by (Var) 93] 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 [94], by (Star) 94] 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, [95] and [107], by (Copy) 95] d*(/\x.star(X(x), Y(x)), Z) >= star(d(/\x.X(x), Z), Y(Z)) because d > star, [96] and [102], by (Copy) 96] d*(/\x.star(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [97] and [41], by (Stat) 97] /\x.star(X(x), Y(x)) > /\x.X(x) because [98], by definition 98] /\y.star*(X(y), Y(y)) >= /\y.X(y) because [99], by (Abs) 99] star*(X(x), Y(x)) >= X(x) because [100], by (Select) 100] X(x) >= X(x) because [101], by (Meta) 101] x >= x by (Var) 102] d*(/\y.star(X(y), Y(y)), Z) >= Y(Z) because [103], by (Select) 103] star(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= Y(Z) because [104], by (Star) 104] star*(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= Y(Z) because [105], by (Select) 105] Y(d*(/\y.star(X(y), Y(y)), Z)) >= Y(Z) because [106], by (Meta) 106] d*(/\y.star(X(y), Y(y)), Z) >= Z because [41], by (Select) 107] d*(/\y.star(X(y), Y(y)), Z) >= star(X(Z), d(/\y.Y(y), Z)) because d > star, [108] and [112], by (Copy) 108] d*(/\y.star(X(y), Y(y)), Z) >= X(Z) because [109], by (Select) 109] star(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= X(Z) because [110], by (Star) 110] star*(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= X(Z) because [111], by (Select) 111] X(d*(/\y.star(X(y), Y(y)), Z)) >= X(Z) because [106], by (Meta) 112] d*(/\y.star(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because d in Mul, [113] and [41], by (Stat) 113] /\y.star(X(y), Y(y)) > /\y.Y(y) because [114], by definition 114] /\z.star*(X(z), Y(z)) >= /\z.Y(z) because [115], by (Abs) 115] star*(X(y), Y(y)) >= Y(y) because [116], by (Select) 116] Y(y) >= Y(y) because [117], by (Meta) 117] y >= y by (Var) 118] d(/\x.sin(X(x)), Y) >= star(cos(Y), d(/\x.X(x), Y)) because [119], by (Star) 119] d*(/\x.sin(X(x)), Y) >= star(cos(Y), d(/\x.X(x), Y)) because d > star, [120] and [122], by (Copy) 120] d*(/\x.sin(X(x)), Y) >= cos(Y) because d > cos and [121], by (Copy) 121] d*(/\x.sin(X(x)), Y) >= Y because [55], by (Select) 122] d*(/\x.sin(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [50] and [55], by (Stat) 123] d(/\x.cos(X(x)), Y) >= star(sin(Y), d(/\x.X(x), Y)) because [124], by (Star) 124] d*(/\x.cos(X(x)), Y) >= star(sin(Y), d(/\x.X(x), Y)) because d > star, [125] and [127], by (Copy) 125] d*(/\x.cos(X(x)), Y) >= sin(Y) because d > sin and [126], by (Copy) 126] d*(/\x.cos(X(x)), Y) >= Y because [69], by (Select) 127] d*(/\x.cos(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [64] and [69], by (Stat) 128] _|_ >= _|_ by (Bot) 129] star(_|_, X) >= _|_ by (Bot) 130] star(X, _|_) >= _|_ by (Bot) 131] plus(_|_, X) >= X because [132], by (Star) 132] plus*(_|_, X) >= X because [133], by (Select) 133] X >= X by (Meta) 134] d(F, X) >= d#(F, X) because [135], by (Star) 135] d*(F, X) >= d#(F, X) because d > d#, [136] and [138], by (Copy) 136] d*(F, X) >= F because [137], by (Select) 137] F >= F by (Meta) 138] d*(F, X) >= X because [139], by (Select) 139] 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.minus(X(x)), Y) =#> d#(/\y.X(y), Y) d#(/\x.minus(X(x)), Y) =#> X(y) d#(/\x.plus(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) d#(/\x.plus(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z) d#(/\x.plus(X(x), Y(x)), Z) =#> Y(y) d#(/\x.star(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) d#(/\x.sin(X(x)), Y) =#> d#(/\y.X(y), Y) d#(/\x.cos(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.minus(X(x)), Y) >? d#(/\y.X(y), Y) d#(/\x.minus(X(x)), Y) >? X(~c0) d#(/\x.plus(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) d#(/\x.plus(X(x), Y(x)), Z) >? d#(/\y.Y(y), Z) d#(/\x.plus(X(x), Y(x)), Z) >? Y(~c1) d#(/\x.star(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) d#(/\x.sin(X(x)), Y) >? d#(/\y.X(y), Y) d#(/\x.cos(X(x)), Y) >? d#(/\y.X(y), Y) 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 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 = {d} and Mul = {cos, d#, minus, plus, sin, star}, and the following precedence: d > cos > 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.minus(X(x)), Y) >= d#(/\x.X(x), Y) d#(/\x.minus(X(x)), Y) >= X(_|_) d#(/\x.plus(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) d#(/\x.plus(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) d#(/\x.plus(X(x), Y(x)), Z) >= Y(_|_) d#(/\x.star(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) d#(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y) d#(/\x.cos(X(x)), Y) > d#(/\x.X(x), Y) d(/\x.X, Y) >= _|_ 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(_|_) >= _|_ star(_|_, X) >= _|_ star(X, _|_) >= _|_ plus(_|_, X) >= X d(F, X) >= d#(F, X) With these choices, we have: 1] d#(/\x.minus(X(x)), Y) >= d#(/\x.X(x), Y) because d# in Mul, [2] and [7], by (Fun) 2] /\y.minus(X(y)) >= /\y.X(y) because [3], by (Abs) 3] minus(X(x)) >= X(x) because [4], by (Star) 4] minus*(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.minus(X(x)), Y) >= X(_|_) because [9], by (Star) 9] d#*(/\x.minus(X(x)), Y) >= X(_|_) because [10], by (Select) 10] minus(X(d#*(/\x.minus(X(x)), Y))) >= X(_|_) because [11], by (Star) 11] minus*(X(d#*(/\x.minus(X(x)), Y))) >= X(_|_) because [12], by (Select) 12] X(d#*(/\x.minus(X(x)), Y)) >= X(_|_) because [13], by (Meta) 13] d#*(/\x.minus(X(x)), Y) >= _|_ by (Bot) 14] d#(/\x.plus(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because d# in Mul, [15] and [20], by (Fun) 15] /\y.plus(X(y), Y(y)) >= /\y.X(y) because [16], by (Abs) 16] plus(X(x), Y(x)) >= X(x) because [17], by (Star) 17] plus*(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.plus(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) because d# in Mul, [22] and [20], by (Fun) 22] /\y.plus(X(y), Y(y)) >= /\y.Y(y) because [23], by (Abs) 23] plus(X(x), Y(x)) >= Y(x) because [24], by (Star) 24] plus*(X(x), Y(x)) >= Y(x) because [25], by (Select) 25] Y(x) >= Y(x) because [26], by (Meta) 26] x >= x by (Var) 27] d#(/\x.plus(X(x), Y(x)), Z) >= Y(_|_) because [28], by (Star) 28] d#*(/\x.plus(X(x), Y(x)), Z) >= Y(_|_) because [29], by (Select) 29] plus(X(d#*(/\x.plus(X(x), Y(x)), Z)), Y(d#*(/\y.plus(X(y), Y(y)), Z))) >= Y(_|_) because [30], by (Star) 30] plus*(X(d#*(/\x.plus(X(x), Y(x)), Z)), Y(d#*(/\y.plus(X(y), Y(y)), Z))) >= Y(_|_) because [31], by (Select) 31] Y(d#*(/\x.plus(X(x), Y(x)), Z)) >= Y(_|_) because [32], by (Meta) 32] d#*(/\x.plus(X(x), Y(x)), Z) >= _|_ by (Bot) 33] d#(/\x.star(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because d# in Mul, [34] and [39], by (Fun) 34] /\y.star(X(y), Y(y)) >= /\y.X(y) because [35], by (Abs) 35] star(X(x), Y(x)) >= X(x) because [36], by (Star) 36] star*(X(x), Y(x)) >= X(x) because [37], by (Select) 37] X(x) >= X(x) because [38], by (Meta) 38] x >= x by (Var) 39] Z >= Z by (Meta) 40] d#(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y) because [41], by (Star) 41] d#*(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y) because d# in Mul, [42] and [47], by (Stat) 42] /\x.sin(X(x)) > /\x.X(x) because [43], by definition 43] /\y.sin*(X(y)) >= /\y.X(y) because [44], by (Abs) 44] sin*(X(x)) >= X(x) because [45], by (Select) 45] X(x) >= X(x) because [46], by (Meta) 46] x >= x by (Var) 47] Y >= Y by (Meta) 48] d#(/\x.cos(X(x)), Y) > d#(/\x.X(x), Y) because [49], by definition 49] d#*(/\x.cos(X(x)), Y) >= d#(/\x.X(x), Y) because d# in Mul, [50] and [55], by (Stat) 50] /\x.cos(X(x)) > /\x.X(x) because [51], by definition 51] /\y.cos*(X(y)) >= /\y.X(y) because [52], by (Abs) 52] cos*(X(x)) >= X(x) because [53], by (Select) 53] X(x) >= X(x) because [54], by (Meta) 54] x >= x by (Var) 55] Y >= Y by (Meta) 56] d(/\x.X, Y) >= _|_ by (Bot) 57] d(/\x.x, X) >= _|_ by (Bot) 58] d(/\x.minus(X(x)), Y) >= minus(d(/\x.X(x), Y)) because [59], by (Star) 59] d*(/\x.minus(X(x)), Y) >= minus(d(/\x.X(x), Y)) because d > minus and [60], by (Copy) 60] d*(/\x.minus(X(x)), Y) >= d(/\x.X(x), Y) because [61], [66] and [67], by (Stat) 61] /\x.minus(X(x)) > /\x.X(x) because [62], by definition 62] /\y.minus*(X(y)) >= /\y.X(y) because [63], by (Abs) 63] minus*(X(x)) >= X(x) because [64], by (Select) 64] X(x) >= X(x) because [65], by (Meta) 65] x >= x by (Var) 66] d*(/\y.minus(X(y)), Y) >= /\y.X(y) because [2], by (Select) 67] d*(/\y.minus(X(y)), Y) >= Y because [7], by (Select) 68] d(/\x.plus(X(x), Y(x)), Z) >= plus(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because [69], by (Star) 69] d*(/\x.plus(X(x), Y(x)), Z) >= plus(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because d > plus, [70] and [78], by (Copy) 70] d*(/\x.plus(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because [71], [76] and [77], by (Stat) 71] /\x.plus(X(x), Y(x)) > /\x.X(x) because [72], by definition 72] /\y.plus*(X(y), Y(y)) >= /\y.X(y) because [73], by (Abs) 73] plus*(X(x), Y(x)) >= X(x) because [74], by (Select) 74] X(x) >= X(x) because [75], by (Meta) 75] x >= x by (Var) 76] d*(/\y.plus(X(y), Y(y)), Z) >= /\y.X(y) because [15], by (Select) 77] d*(/\y.plus(X(y), Y(y)), Z) >= Z because [20], by (Select) 78] d*(/\y.plus(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because [79], [84] and [77], by (Stat) 79] /\y.plus(X(y), Y(y)) > /\y.Y(y) because [80], by definition 80] /\z.plus*(X(z), Y(z)) >= /\z.Y(z) because [81], by (Abs) 81] plus*(X(y), Y(y)) >= Y(y) because [82], by (Select) 82] Y(y) >= Y(y) because [83], by (Meta) 83] y >= y by (Var) 84] d*(/\z.plus(X(z), Y(z)), Z) >= /\z.Y(z) because [22], by (Select) 85] 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 [86], by (Star) 86] 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, [87] and [106], by (Copy) 87] d*(/\x.star(X(x), Y(x)), Z) >= star(d(/\x.X(x), Z), Y(Z)) because d > star, [88] and [102], by (Copy) 88] d*(/\x.star(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because [89], [94] and [101], by (Stat) 89] /\x.star(X(x), Y(x)) > /\x.X(x) because [90], by definition 90] /\y.star*(X(y), Y(y)) >= /\y.X(y) because [91], by (Abs) 91] star*(X(x), Y(x)) >= X(x) because [92], by (Select) 92] X(x) >= X(x) because [93], by (Meta) 93] x >= x by (Var) 94] d*(/\y.star(X(y), Y(y)), Z) >= /\y.X(y) because [95], by (F-Abs) 95] d*(/\y.star(X(y), Y(y)), Z, z) >= X(z) because [96], by (Select) 96] star(X(d*(/\y.star(X(y), Y(y)), Z, z)), Y(d*(/\u.star(X(u), Y(u)), Z, z))) >= X(z) because [97], by (Star) 97] star*(X(d*(/\y.star(X(y), Y(y)), Z, z)), Y(d*(/\u.star(X(u), Y(u)), Z, z))) >= X(z) because [98], by (Select) 98] X(d*(/\y.star(X(y), Y(y)), Z, z)) >= X(z) because [99], by (Meta) 99] d*(/\y.star(X(y), Y(y)), Z, z) >= z because [100], by (Select) 100] z >= z by (Var) 101] d*(/\y.star(X(y), Y(y)), Z) >= Z because [39], by (Select) 102] d*(/\y.star(X(y), Y(y)), Z) >= Y(Z) because [103], by (Select) 103] star(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\u.star(X(u), Y(u)), Z))) >= Y(Z) because [104], by (Star) 104] star*(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\u.star(X(u), Y(u)), Z))) >= Y(Z) because [105], by (Select) 105] Y(d*(/\y.star(X(y), Y(y)), Z)) >= Y(Z) because [101], by (Meta) 106] d*(/\y.star(X(y), Y(y)), Z) >= star(X(Z), d(/\y.Y(y), Z)) because d > star, [107] and [111], by (Copy) 107] d*(/\y.star(X(y), Y(y)), Z) >= X(Z) because [108], by (Select) 108] star(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\u.star(X(u), Y(u)), Z))) >= X(Z) because [109], by (Star) 109] star*(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\u.star(X(u), Y(u)), Z))) >= X(Z) because [110], by (Select) 110] X(d*(/\y.star(X(y), Y(y)), Z)) >= X(Z) because [101], by (Meta) 111] d*(/\y.star(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because [112], [117] and [101], by (Stat) 112] /\y.star(X(y), Y(y)) > /\y.Y(y) because [113], by definition 113] /\u.star*(X(u), Y(u)) >= /\u.Y(u) because [114], by (Abs) 114] star*(X(y), Y(y)) >= Y(y) because [115], by (Select) 115] Y(y) >= Y(y) because [116], by (Meta) 116] y >= y by (Var) 117] d*(/\u.star(X(u), Y(u)), Z) >= /\u.Y(u) because [118], by (Select) 118] /\v.star(X(v), Y(v)) >= /\v.Y(v) because [119], by (Abs) 119] star(X(u), Y(u)) >= Y(u) because [120], by (Star) 120] star*(X(u), Y(u)) >= Y(u) because [121], by (Select) 121] Y(u) >= Y(u) because [122], by (Meta) 122] u >= u by (Var) 123] d(/\x.sin(X(x)), Y) >= star(cos(Y), d(/\x.X(x), Y)) because [124], by (Star) 124] d*(/\x.sin(X(x)), Y) >= star(cos(Y), d(/\x.X(x), Y)) because d > star, [125] and [127], by (Copy) 125] d*(/\x.sin(X(x)), Y) >= cos(Y) because d > cos and [126], by (Copy) 126] d*(/\x.sin(X(x)), Y) >= Y because [47], by (Select) 127] d*(/\x.sin(X(x)), Y) >= d(/\x.X(x), Y) because [42], [128] and [126], by (Stat) 128] d*(/\x.sin(X(x)), Y) >= /\x.X(x) because [129], by (Select) 129] /\y.sin(X(y)) >= /\y.X(y) because [130], by (Abs) 130] sin(X(x)) >= X(x) because [131], by (Star) 131] sin*(X(x)) >= X(x) because [132], by (Select) 132] X(x) >= X(x) because [133], by (Meta) 133] x >= x by (Var) 134] d(/\x.cos(X(x)), Y) >= star(minus(sin(Y)), d(/\x.X(x), Y)) because [135], by (Star) 135] d*(/\x.cos(X(x)), Y) >= star(minus(sin(Y)), d(/\x.X(x), Y)) because d > star, [136] and [139], by (Copy) 136] d*(/\x.cos(X(x)), Y) >= minus(sin(Y)) because d > minus and [137], by (Copy) 137] d*(/\x.cos(X(x)), Y) >= sin(Y) because d > sin and [138], by (Copy) 138] d*(/\x.cos(X(x)), Y) >= Y because [55], by (Select) 139] d*(/\x.cos(X(x)), Y) >= d(/\x.X(x), Y) because [50], [140] and [138], by (Stat) 140] d*(/\x.cos(X(x)), Y) >= /\x.X(x) because [141], by (Select) 141] /\y.cos(X(y)) >= /\y.X(y) because [142], by (Abs) 142] cos(X(x)) >= X(x) because [143], by (Star) 143] cos*(X(x)) >= X(x) because [144], by (Select) 144] X(x) >= X(x) because [145], by (Meta) 145] x >= x by (Var) 146] minus(_|_) >= _|_ by (Bot) 147] star(_|_, X) >= _|_ by (Bot) 148] star(X, _|_) >= _|_ by (Bot) 149] plus(_|_, X) >= X because [150], by (Star) 150] plus*(_|_, X) >= X because [151], by (Select) 151] X >= X by (Meta) 152] d(F, X) >= d#(F, X) because [153], by (Star) 153] d*(F, X) >= d#(F, X) because d > d#, [154] and [156], by (Copy) 154] d*(F, X) >= F because [155], by (Select) 155] F >= F by (Meta) 156] d*(F, X) >= X because [157], by (Select) 157] 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.minus(X(x)), Y) =#> d#(/\y.X(y), Y) d#(/\x.minus(X(x)), Y) =#> X(y) d#(/\x.plus(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) d#(/\x.plus(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z) d#(/\x.plus(X(x), Y(x)), Z) =#> Y(y) d#(/\x.star(X(x), Y(x)), Z) =#> d#(/\y.X(y), 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.minus(X(x)), Y) >? d#(/\y.X(y), Y) d#(/\x.minus(X(x)), Y) >? X(~c0) d#(/\x.plus(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) d#(/\x.plus(X(x), Y(x)), Z) >? d#(/\y.Y(y), Z) d#(/\x.plus(X(x), Y(x)), Z) >? Y(~c1) d#(/\x.star(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) d#(/\x.sin(X(x)), Y) >? d#(/\y.X(y), Y) 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 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]] = _|_ [[minus(x_1)]] = x_1 [[~c0]] = _|_ [[~c1]] = _|_ We choose Lex = {} and Mul = {cos, d, d#, plus, sin, star}, and the following precedence: d > cos > d# > 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(x), Y) >= d#(/\x.X(x), Y) d#(/\x.X(x), Y) >= X(_|_) d#(/\x.plus(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) d#(/\x.plus(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) d#(/\x.plus(X(x), Y(x)), Z) >= Y(_|_) d#(/\x.star(X(x), Y(x)), Z) >= d#(/\x.X(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.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 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.plus(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because d# in Mul, [11] and [16], by (Fun) 11] /\y.plus(X(y), Y(y)) >= /\y.X(y) because [12], by (Abs) 12] plus(X(x), Y(x)) >= X(x) because [13], by (Star) 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#(/\x.plus(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) because d# in Mul, [18] and [16], by (Fun) 18] /\y.plus(X(y), Y(y)) >= /\y.Y(y) because [19], by (Abs) 19] plus(X(x), Y(x)) >= Y(x) because [20], by (Star) 20] plus*(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.plus(X(x), Y(x)), Z) >= Y(_|_) because [24], by (Star) 24] d#*(/\x.plus(X(x), Y(x)), Z) >= Y(_|_) because [25], by (Select) 25] plus(X(d#*(/\x.plus(X(x), Y(x)), Z)), Y(d#*(/\y.plus(X(y), Y(y)), Z))) >= Y(_|_) because [26], by (Star) 26] plus*(X(d#*(/\x.plus(X(x), Y(x)), Z)), Y(d#*(/\y.plus(X(y), Y(y)), Z))) >= Y(_|_) because [27], by (Select) 27] Y(d#*(/\x.plus(X(x), Y(x)), Z)) >= Y(_|_) because [28], by (Meta) 28] d#*(/\x.plus(X(x), Y(x)), Z) >= _|_ by (Bot) 29] d#(/\x.star(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because [30], by (Star) 30] d#*(/\x.star(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because d# in Mul, [31] and [36], by (Stat) 31] /\x.star(X(x), Y(x)) > /\x.X(x) because [32], by definition 32] /\y.star*(X(y), Y(y)) >= /\y.X(y) because [33], by (Abs) 33] star*(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#(/\x.sin(X(x)), Y) > d#(/\x.X(x), Y) because [38], by definition 38] d#*(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y) because d# in Mul, [39] and [44], by (Stat) 39] /\x.sin(X(x)) > /\x.X(x) because [40], by definition 40] /\y.sin*(X(y)) >= /\y.X(y) because [41], by (Abs) 41] sin*(X(x)) >= X(x) because [42], by (Select) 42] X(x) >= X(x) because [43], by (Meta) 43] x >= x by (Var) 44] Y >= Y by (Meta) 45] d(/\x.X, Y) >= _|_ by (Bot) 46] d(/\x.x, X) >= _|_ by (Bot) 47] d(/\x.X(x), Y) >= d(/\x.X(x), Y) because d in Mul, [2] and [5], by (Fun) 48] d(/\x.plus(X(x), Y(x)), Z) >= plus(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because [49], by (Star) 49] d*(/\x.plus(X(x), Y(x)), Z) >= plus(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because d > plus, [50] and [56], by (Copy) 50] d*(/\x.plus(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [51] and [16], by (Stat) 51] /\x.plus(X(x), Y(x)) > /\x.X(x) because [52], by definition 52] /\y.plus*(X(y), Y(y)) >= /\y.X(y) because [53], by (Abs) 53] plus*(X(x), Y(x)) >= X(x) because [54], by (Select) 54] X(x) >= X(x) because [55], by (Meta) 55] x >= x by (Var) 56] d*(/\y.plus(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because d in Mul, [57] and [16], by (Stat) 57] /\y.plus(X(y), Y(y)) > /\y.Y(y) because [58], by definition 58] /\z.plus*(X(z), Y(z)) >= /\z.Y(z) because [59], by (Abs) 59] plus*(X(y), Y(y)) >= Y(y) because [60], by (Select) 60] Y(y) >= Y(y) because [61], by (Meta) 61] y >= y by (Var) 62] 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 [63], by (Star) 63] 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, [64] and [71], by (Copy) 64] d*(/\x.star(X(x), Y(x)), Z) >= star(d(/\x.X(x), Z), Y(Z)) because d > star, [65] and [66], by (Copy) 65] d*(/\x.star(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [31] and [36], by (Stat) 66] d*(/\x.star(X(x), Y(x)), Z) >= Y(Z) because [67], by (Select) 67] star(X(d*(/\x.star(X(x), Y(x)), Z)), Y(d*(/\y.star(X(y), Y(y)), Z))) >= Y(Z) because [68], by (Star) 68] star*(X(d*(/\x.star(X(x), Y(x)), Z)), Y(d*(/\y.star(X(y), Y(y)), Z))) >= Y(Z) because [69], by (Select) 69] Y(d*(/\x.star(X(x), Y(x)), Z)) >= Y(Z) because [70], by (Meta) 70] d*(/\x.star(X(x), Y(x)), Z) >= Z because [36], by (Select) 71] d*(/\x.star(X(x), Y(x)), Z) >= star(X(Z), d(/\x.Y(x), Z)) because d > star, [72] and [76], by (Copy) 72] d*(/\x.star(X(x), Y(x)), Z) >= X(Z) because [73], by (Select) 73] star(X(d*(/\x.star(X(x), Y(x)), Z)), Y(d*(/\y.star(X(y), Y(y)), Z))) >= X(Z) because [74], by (Star) 74] star*(X(d*(/\x.star(X(x), Y(x)), Z)), Y(d*(/\y.star(X(y), Y(y)), Z))) >= X(Z) because [75], by (Select) 75] X(d*(/\x.star(X(x), Y(x)), Z)) >= X(Z) because [70], by (Meta) 76] d*(/\x.star(X(x), Y(x)), Z) >= d(/\x.Y(x), Z) because d in Mul, [77] and [36], by (Stat) 77] /\x.star(X(x), Y(x)) > /\x.Y(x) because [78], by definition 78] /\y.star*(X(y), Y(y)) >= /\y.Y(y) because [79], by (Abs) 79] star*(X(x), Y(x)) >= Y(x) because [80], by (Select) 80] Y(x) >= Y(x) because [81], by (Meta) 81] x >= x by (Var) 82] d(/\x.sin(X(x)), Y) >= star(cos(Y), d(/\x.X(x), Y)) because [83], by (Star) 83] d*(/\x.sin(X(x)), Y) >= star(cos(Y), d(/\x.X(x), Y)) because d > star, [84] and [86], by (Copy) 84] d*(/\x.sin(X(x)), Y) >= cos(Y) because d > cos and [85], by (Copy) 85] d*(/\x.sin(X(x)), Y) >= Y because [44], by (Select) 86] d*(/\x.sin(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [39] and [44], by (Stat) 87] d(/\x.cos(X(x)), Y) >= star(sin(Y), d(/\x.X(x), Y)) because [88], by (Star) 88] d*(/\x.cos(X(x)), Y) >= star(sin(Y), d(/\x.X(x), Y)) because d > star, [89] and [92], by (Copy) 89] d*(/\x.cos(X(x)), Y) >= sin(Y) because d > sin and [90], by (Copy) 90] d*(/\x.cos(X(x)), Y) >= Y because [91], by (Select) 91] Y >= Y by (Meta) 92] d*(/\x.cos(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [93] and [98], by (Stat) 93] /\x.cos(X(x)) > /\x.X(x) because [94], by definition 94] /\y.cos*(X(y)) >= /\y.X(y) because [95], by (Abs) 95] cos*(X(x)) >= X(x) because [96], by (Select) 96] X(x) >= X(x) because [97], by (Meta) 97] x >= x by (Var) 98] Y >= Y by (Meta) 99] _|_ >= _|_ by (Bot) 100] star(_|_, X) >= _|_ by (Bot) 101] star(X, _|_) >= _|_ by (Bot) 102] plus(_|_, X) >= X because [103], by (Star) 103] plus*(_|_, X) >= X because [104], by (Select) 104] X >= X 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_4, R_0, minimal, all) by (P_5, R_0, minimal, all), where P_5 consists of: d#(/\x.minus(X(x)), Y) =#> d#(/\y.X(y), Y) d#(/\x.minus(X(x)), Y) =#> X(y) d#(/\x.plus(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) d#(/\x.plus(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z) d#(/\x.plus(X(x), Y(x)), Z) =#> Y(y) d#(/\x.star(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) 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.minus(X(x)), Y) >? d#(/\y.X(y), Y) d#(/\x.minus(X(x)), Y) >? X(~c0) d#(/\x.plus(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) d#(/\x.plus(X(x), Y(x)), Z) >? d#(/\y.Y(y), Z) d#(/\x.plus(X(x), Y(x)), Z) >? Y(~c1) d#(/\x.star(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) 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 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]] = _|_ [[minus(x_1)]] = x_1 [[~c0]] = _|_ [[~c1]] = _|_ We choose Lex = {} and Mul = {cos, d, d#, plus, sin, star}, and the following precedence: d > d# > cos > 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(x), Y) >= d#(/\x.X(x), Y) d#(/\x.X(x), Y) > X(_|_) d#(/\x.plus(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) d#(/\x.plus(X(x), Y(x)), Z) > d#(/\x.Y(x), Z) d#(/\x.plus(X(x), Y(x)), Z) >= Y(_|_) d#(/\x.star(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) 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 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 definition 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.plus(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because d# in Mul, [11] and [16], by (Fun) 11] /\y.plus(X(y), Y(y)) >= /\y.X(y) because [12], by (Abs) 12] plus(X(x), Y(x)) >= X(x) because [13], by (Star) 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#(/\x.plus(X(x), Y(x)), Z) > d#(/\x.Y(x), Z) because [18], by definition 18] d#*(/\x.plus(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) because d# in Mul, [19] and [16], by (Stat) 19] /\x.plus(X(x), Y(x)) > /\x.Y(x) because [20], by definition 20] /\y.plus*(X(y), Y(y)) >= /\y.Y(y) because [21], by (Abs) 21] plus*(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.plus(X(x), Y(x)), Z) >= Y(_|_) because [25], by (Star) 25] d#*(/\x.plus(X(x), Y(x)), Z) >= Y(_|_) because [26], by (Select) 26] plus(X(d#*(/\x.plus(X(x), Y(x)), Z)), Y(d#*(/\y.plus(X(y), Y(y)), Z))) >= Y(_|_) because [27], by (Star) 27] plus*(X(d#*(/\x.plus(X(x), Y(x)), Z)), Y(d#*(/\y.plus(X(y), Y(y)), Z))) >= Y(_|_) because [28], by (Select) 28] Y(d#*(/\x.plus(X(x), Y(x)), Z)) >= Y(_|_) because [29], by (Meta) 29] d#*(/\x.plus(X(x), Y(x)), Z) >= _|_ by (Bot) 30] d#(/\x.star(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because [31], by (Star) 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(/\x.X, Y) >= _|_ by (Bot) 39] d(/\x.x, X) >= _|_ by (Bot) 40] d(/\x.X(x), Y) >= d(/\x.X(x), Y) because d in Mul, [2] and [5], by (Fun) 41] d(/\x.plus(X(x), Y(x)), Z) >= plus(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because [42], by (Star) 42] d*(/\x.plus(X(x), Y(x)), Z) >= plus(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because d > plus, [43] and [49], by (Copy) 43] d*(/\x.plus(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [44] and [16], by (Stat) 44] /\x.plus(X(x), Y(x)) > /\x.X(x) because [45], by definition 45] /\y.plus*(X(y), Y(y)) >= /\y.X(y) because [46], by (Abs) 46] plus*(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] d*(/\y.plus(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because d in Mul, [19] and [16], by (Stat) 50] 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 [51], by (Star) 51] 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, [52] and [59], by (Copy) 52] d*(/\x.star(X(x), Y(x)), Z) >= star(d(/\x.X(x), Z), Y(Z)) because d > star, [53] and [54], by (Copy) 53] d*(/\x.star(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [32] and [37], by (Stat) 54] d*(/\x.star(X(x), Y(x)), Z) >= Y(Z) because [55], by (Select) 55] star(X(d*(/\x.star(X(x), Y(x)), Z)), Y(d*(/\y.star(X(y), Y(y)), Z))) >= Y(Z) because [56], by (Star) 56] star*(X(d*(/\x.star(X(x), Y(x)), Z)), Y(d*(/\y.star(X(y), Y(y)), Z))) >= Y(Z) because [57], by (Select) 57] Y(d*(/\x.star(X(x), Y(x)), Z)) >= Y(Z) because [58], by (Meta) 58] d*(/\x.star(X(x), Y(x)), Z) >= Z because [37], by (Select) 59] d*(/\x.star(X(x), Y(x)), Z) >= star(X(Z), d(/\x.Y(x), Z)) because d > star, [60] and [64], by (Copy) 60] d*(/\x.star(X(x), Y(x)), Z) >= X(Z) because [61], by (Select) 61] star(X(d*(/\x.star(X(x), Y(x)), Z)), Y(d*(/\y.star(X(y), Y(y)), Z))) >= X(Z) because [62], by (Star) 62] star*(X(d*(/\x.star(X(x), Y(x)), Z)), Y(d*(/\y.star(X(y), Y(y)), Z))) >= X(Z) because [63], by (Select) 63] X(d*(/\x.star(X(x), Y(x)), Z)) >= X(Z) because [58], by (Meta) 64] d*(/\x.star(X(x), Y(x)), Z) >= d(/\x.Y(x), Z) because d in Mul, [65] and [37], by (Stat) 65] /\x.star(X(x), Y(x)) > /\x.Y(x) because [66], by definition 66] /\y.star*(X(y), Y(y)) >= /\y.Y(y) because [67], by (Abs) 67] star*(X(x), Y(x)) >= Y(x) because [68], by (Select) 68] Y(x) >= Y(x) because [69], by (Meta) 69] x >= x by (Var) 70] d(/\x.sin(X(x)), Y) >= star(cos(Y), d(/\x.X(x), Y)) because [71], by (Star) 71] d*(/\x.sin(X(x)), Y) >= star(cos(Y), d(/\x.X(x), Y)) because d > star, [72] and [75], by (Copy) 72] d*(/\x.sin(X(x)), Y) >= cos(Y) because d > cos and [73], by (Copy) 73] d*(/\x.sin(X(x)), Y) >= Y because [74], by (Select) 74] Y >= Y by (Meta) 75] d*(/\x.sin(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [76] and [81], by (Stat) 76] /\x.sin(X(x)) > /\x.X(x) because [77], by definition 77] /\y.sin*(X(y)) >= /\y.X(y) because [78], by (Abs) 78] sin*(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(/\x.cos(X(x)), Y) >= star(sin(Y), d(/\x.X(x), Y)) because [83], by (Star) 83] d*(/\x.cos(X(x)), Y) >= star(sin(Y), d(/\x.X(x), Y)) because d > star, [84] and [87], by (Copy) 84] d*(/\x.cos(X(x)), Y) >= sin(Y) because d > sin and [85], by (Copy) 85] d*(/\x.cos(X(x)), Y) >= Y because [86], by (Select) 86] Y >= Y by (Meta) 87] d*(/\x.cos(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [88] and [93], by (Stat) 88] /\x.cos(X(x)) > /\x.X(x) because [89], by definition 89] /\y.cos*(X(y)) >= /\y.X(y) because [90], by (Abs) 90] cos*(X(x)) >= X(x) because [91], by (Select) 91] X(x) >= X(x) because [92], by (Meta) 92] x >= x by (Var) 93] Y >= Y by (Meta) 94] _|_ >= _|_ by (Bot) 95] star(_|_, X) >= _|_ by (Bot) 96] star(X, _|_) >= _|_ by (Bot) 97] plus(_|_, X) >= X because [98], by (Star) 98] plus*(_|_, X) >= X because [99], by (Select) 99] X >= X by (Meta) 100] d(F, X) >= d#(F, X) because [101], by (Star) 101] d*(F, X) >= d#(F, X) because d > d#, [102] and [104], by (Copy) 102] d*(F, X) >= F because [103], by (Select) 103] F >= F by (Meta) 104] d*(F, X) >= X because [105], by (Select) 105] 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.minus(X(x)), Y) =#> d#(/\y.X(y), Y) d#(/\x.plus(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) d#(/\x.plus(X(x), Y(x)), Z) =#> Y(y) d#(/\x.star(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) 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.minus(X(x)), Y) >? d#(/\y.X(y), Y) d#(/\x.plus(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) d#(/\x.plus(X(x), Y(x)), Z) >? Y(~c0) d#(/\x.star(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) 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 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]] = _|_ [[minus(x_1)]] = x_1 [[~c0]] = _|_ We choose Lex = {} and Mul = {cos, d, d#, plus, sin, star}, and the following precedence: cos = d > d# > 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(x), Y) >= d#(/\x.X(x), Y) d#(/\x.plus(X(x), Y(x)), Z) > d#(/\x.X(x), Z) d#(/\x.plus(X(x), Y(x)), Z) >= Y(_|_) d#(/\x.star(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) 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 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.plus(X(x), Y(x)), Z) > d#(/\x.X(x), Z) because [7], by definition 7] d#*(/\x.plus(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because d# in Mul, [8] and [13], by (Stat) 8] /\x.plus(X(x), Y(x)) > /\x.X(x) because [9], by definition 9] /\y.plus*(X(y), Y(y)) >= /\y.X(y) because [10], by (Abs) 10] plus*(X(x), Y(x)) >= X(x) because [11], by (Select) 11] X(x) >= X(x) because [12], by (Meta) 12] x >= x by (Var) 13] Z >= Z by (Meta) 14] d#(/\x.plus(X(x), Y(x)), Z) >= Y(_|_) because [15], by (Star) 15] d#*(/\x.plus(X(x), Y(x)), Z) >= Y(_|_) because [16], by (Select) 16] plus(X(d#*(/\x.plus(X(x), Y(x)), Z)), Y(d#*(/\y.plus(X(y), Y(y)), Z))) >= Y(_|_) because [17], by (Star) 17] plus*(X(d#*(/\x.plus(X(x), Y(x)), Z)), Y(d#*(/\y.plus(X(y), Y(y)), Z))) >= Y(_|_) because [18], by (Select) 18] Y(d#*(/\x.plus(X(x), Y(x)), Z)) >= Y(_|_) because [19], by (Meta) 19] d#*(/\x.plus(X(x), Y(x)), Z) >= _|_ by (Bot) 20] d#(/\x.star(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because [21], by (Star) 21] d#*(/\x.star(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because d# in Mul, [22] and [27], by (Stat) 22] /\x.star(X(x), Y(x)) > /\x.X(x) because [23], by definition 23] /\y.star*(X(y), Y(y)) >= /\y.X(y) because [24], by (Abs) 24] star*(X(x), Y(x)) >= X(x) because [25], by (Select) 25] X(x) >= X(x) because [26], by (Meta) 26] x >= x by (Var) 27] Z >= Z by (Meta) 28] d(/\x.X, Y) >= _|_ by (Bot) 29] d(/\x.x, X) >= _|_ by (Bot) 30] d(/\x.X(x), Y) >= d(/\x.X(x), Y) because d in Mul, [2] and [5], by (Fun) 31] d(/\x.plus(X(x), Y(x)), Z) >= plus(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because [32], by (Star) 32] d*(/\x.plus(X(x), Y(x)), Z) >= plus(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because d > plus, [33] and [34], by (Copy) 33] d*(/\x.plus(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [8] and [13], by (Stat) 34] d*(/\x.plus(X(x), Y(x)), Z) >= d(/\x.Y(x), Z) because d in Mul, [35] and [13], by (Stat) 35] /\x.plus(X(x), Y(x)) > /\x.Y(x) because [36], by definition 36] /\y.plus*(X(y), Y(y)) >= /\y.Y(y) because [37], by (Abs) 37] plus*(X(x), Y(x)) >= Y(x) because [38], by (Select) 38] Y(x) >= Y(x) because [39], by (Meta) 39] x >= x by (Var) 40] 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 [41], by (Star) 41] 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, [42] and [49], by (Copy) 42] d*(/\x.star(X(x), Y(x)), Z) >= star(d(/\x.X(x), Z), Y(Z)) because d > star, [43] and [44], by (Copy) 43] d*(/\x.star(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [22] and [27], by (Stat) 44] d*(/\x.star(X(x), Y(x)), Z) >= Y(Z) because [45], by (Select) 45] star(X(d*(/\x.star(X(x), Y(x)), Z)), Y(d*(/\y.star(X(y), Y(y)), Z))) >= Y(Z) because [46], by (Star) 46] star*(X(d*(/\x.star(X(x), Y(x)), Z)), Y(d*(/\y.star(X(y), Y(y)), Z))) >= Y(Z) because [47], by (Select) 47] Y(d*(/\x.star(X(x), Y(x)), Z)) >= Y(Z) because [48], by (Meta) 48] d*(/\x.star(X(x), Y(x)), Z) >= Z because [27], by (Select) 49] d*(/\x.star(X(x), Y(x)), Z) >= star(X(Z), d(/\x.Y(x), Z)) because d > star, [50] and [54], by (Copy) 50] d*(/\x.star(X(x), Y(x)), Z) >= X(Z) because [51], by (Select) 51] star(X(d*(/\x.star(X(x), Y(x)), Z)), Y(d*(/\y.star(X(y), Y(y)), Z))) >= X(Z) because [52], by (Star) 52] star*(X(d*(/\x.star(X(x), Y(x)), Z)), Y(d*(/\y.star(X(y), Y(y)), Z))) >= X(Z) because [53], by (Select) 53] X(d*(/\x.star(X(x), Y(x)), Z)) >= X(Z) because [48], by (Meta) 54] d*(/\x.star(X(x), Y(x)), Z) >= d(/\x.Y(x), Z) because d in Mul, [55] and [27], by (Stat) 55] /\x.star(X(x), Y(x)) > /\x.Y(x) because [56], by definition 56] /\y.star*(X(y), Y(y)) >= /\y.Y(y) because [57], by (Abs) 57] star*(X(x), Y(x)) >= Y(x) because [58], by (Select) 58] Y(x) >= Y(x) because [59], by (Meta) 59] x >= x by (Var) 60] d(/\x.sin(X(x)), Y) >= star(cos(Y), d(/\x.X(x), Y)) because [61], by (Star) 61] d*(/\x.sin(X(x)), Y) >= star(cos(Y), d(/\x.X(x), Y)) because d > star, [62] and [64], by (Copy) 62] d*(/\x.sin(X(x)), Y) >= cos(Y) because d = cos, d in Mul and [63], by (Stat) 63] Y >= Y by (Meta) 64] d*(/\x.sin(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [65] and [63], by (Stat) 65] /\x.sin(X(x)) > /\x.X(x) because [66], by definition 66] /\y.sin*(X(y)) >= /\y.X(y) because [67], by (Abs) 67] sin*(X(x)) >= X(x) because [68], by (Select) 68] X(x) >= X(x) because [69], by (Meta) 69] x >= x by (Var) 70] d(/\x.cos(X(x)), Y) >= star(sin(Y), d(/\x.X(x), Y)) because [71], by (Star) 71] d*(/\x.cos(X(x)), Y) >= star(sin(Y), d(/\x.X(x), Y)) because d > star, [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] _|_ >= _|_ by (Bot) 83] star(_|_, X) >= _|_ by (Bot) 84] star(X, _|_) >= _|_ by (Bot) 85] plus(_|_, X) >= X because [86], by (Star) 86] plus*(_|_, X) >= X because [87], by (Select) 87] X >= X by (Meta) 88] d(F, X) >= d#(F, X) because [89], by (Star) 89] d*(F, X) >= d#(F, X) because d > d#, [90] and [92], by (Copy) 90] d*(F, X) >= F because [91], by (Select) 91] F >= F by (Meta) 92] d*(F, X) >= X because [93], by (Select) 93] 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.minus(X(x)), Y) =#> d#(/\y.X(y), Y) d#(/\x.plus(X(x), Y(x)), Z) =#> Y(y) d#(/\x.star(X(x), Y(x)), Z) =#> d#(/\y.X(y), 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.minus(X(x)), Y) >? d#(/\y.X(y), Y) d#(/\x.plus(X(x), Y(x)), Z) >? Y(~c0) d#(/\x.star(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) 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 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]] = _|_ [[minus(x_1)]] = x_1 [[~c0]] = _|_ We choose Lex = {} and Mul = {cos, d, d#, plus, sin, star}, and the following precedence: d > cos > d# > 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(x), Y) >= d#(/\x.X(x), Y) d#(/\x.plus(X(x), Y(x)), Z) > Y(_|_) d#(/\x.star(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) 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 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.plus(X(x), Y(x)), Z) > Y(_|_) because [7], by definition 7] d#*(/\x.plus(X(x), Y(x)), Z) >= Y(_|_) because [8], by (Select) 8] plus(X(d#*(/\x.plus(X(x), Y(x)), Z)), Y(d#*(/\y.plus(X(y), Y(y)), Z))) >= Y(_|_) because [9], by (Star) 9] plus*(X(d#*(/\x.plus(X(x), Y(x)), Z)), Y(d#*(/\y.plus(X(y), Y(y)), Z))) >= Y(_|_) because [10], by (Select) 10] Y(d#*(/\x.plus(X(x), Y(x)), Z)) >= Y(_|_) because [11], by (Meta) 11] d#*(/\x.plus(X(x), Y(x)), Z) >= _|_ by (Bot) 12] d#(/\x.star(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because [13], by (Star) 13] d#*(/\x.star(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because d# in Mul, [14] and [19], by (Stat) 14] /\x.star(X(x), Y(x)) > /\x.X(x) because [15], by definition 15] /\y.star*(X(y), Y(y)) >= /\y.X(y) because [16], by (Abs) 16] star*(X(x), Y(x)) >= X(x) because [17], by (Select) 17] X(x) >= X(x) because [18], by (Meta) 18] x >= x by (Var) 19] Z >= Z by (Meta) 20] d(/\x.X, Y) >= _|_ by (Bot) 21] d(/\x.x, X) >= _|_ by (Bot) 22] d(/\x.X(x), Y) >= d(/\x.X(x), Y) because d in Mul, [2] and [5], by (Fun) 23] d(/\x.plus(X(x), Y(x)), Z) >= plus(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because [24], by (Star) 24] d*(/\x.plus(X(x), Y(x)), Z) >= plus(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because d > plus, [25] and [32], by (Copy) 25] d*(/\x.plus(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [26] and [31], by (Stat) 26] /\x.plus(X(x), Y(x)) > /\x.X(x) because [27], by definition 27] /\y.plus*(X(y), Y(y)) >= /\y.X(y) because [28], by (Abs) 28] plus*(X(x), Y(x)) >= X(x) because [29], by (Select) 29] X(x) >= X(x) because [30], by (Meta) 30] x >= x by (Var) 31] Z >= Z by (Meta) 32] d*(/\y.plus(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because d in Mul, [33] and [31], by (Stat) 33] /\y.plus(X(y), Y(y)) > /\y.Y(y) because [34], by definition 34] /\z.plus*(X(z), Y(z)) >= /\z.Y(z) because [35], by (Abs) 35] plus*(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.star(X(x), Y(x)), Z) >= plus(star(d(/\x.X(x), Z), Y(Z)), star(X(Z), d(/\y.Y(y), Z))) because [39], by (Star) 39] 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, [40] and [47], by (Copy) 40] d*(/\x.star(X(x), Y(x)), Z) >= star(d(/\x.X(x), Z), Y(Z)) because d > star, [41] and [42], by (Copy) 41] d*(/\x.star(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [14] and [19], by (Stat) 42] d*(/\x.star(X(x), Y(x)), Z) >= Y(Z) because [43], by (Select) 43] star(X(d*(/\x.star(X(x), Y(x)), Z)), Y(d*(/\y.star(X(y), Y(y)), Z))) >= Y(Z) because [44], by (Star) 44] star*(X(d*(/\x.star(X(x), Y(x)), Z)), Y(d*(/\y.star(X(y), Y(y)), Z))) >= Y(Z) because [45], by (Select) 45] Y(d*(/\x.star(X(x), Y(x)), Z)) >= Y(Z) because [46], by (Meta) 46] d*(/\x.star(X(x), Y(x)), Z) >= Z because [19], by (Select) 47] d*(/\x.star(X(x), Y(x)), Z) >= star(X(Z), d(/\x.Y(x), Z)) because d > star, [48] and [52], by (Copy) 48] d*(/\x.star(X(x), Y(x)), Z) >= X(Z) because [49], by (Select) 49] star(X(d*(/\x.star(X(x), Y(x)), Z)), Y(d*(/\y.star(X(y), Y(y)), Z))) >= X(Z) because [50], by (Star) 50] star*(X(d*(/\x.star(X(x), Y(x)), Z)), Y(d*(/\y.star(X(y), Y(y)), Z))) >= X(Z) because [51], by (Select) 51] X(d*(/\x.star(X(x), Y(x)), Z)) >= X(Z) because [46], by (Meta) 52] d*(/\x.star(X(x), Y(x)), Z) >= d(/\x.Y(x), Z) because d in Mul, [53] and [19], by (Stat) 53] /\x.star(X(x), Y(x)) > /\x.Y(x) because [54], by definition 54] /\y.star*(X(y), Y(y)) >= /\y.Y(y) because [55], by (Abs) 55] star*(X(x), Y(x)) >= Y(x) because [56], by (Select) 56] Y(x) >= Y(x) because [57], by (Meta) 57] x >= x by (Var) 58] d(/\x.sin(X(x)), Y) >= star(cos(Y), d(/\x.X(x), Y)) because [59], by (Star) 59] d*(/\x.sin(X(x)), Y) >= star(cos(Y), d(/\x.X(x), Y)) because d > star, [60] and [63], by (Copy) 60] d*(/\x.sin(X(x)), Y) >= cos(Y) because d > cos and [61], by (Copy) 61] d*(/\x.sin(X(x)), Y) >= Y because [62], by (Select) 62] Y >= Y by (Meta) 63] d*(/\x.sin(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [64] and [69], by (Stat) 64] /\x.sin(X(x)) > /\x.X(x) because [65], by definition 65] /\y.sin*(X(y)) >= /\y.X(y) because [66], by (Abs) 66] sin*(X(x)) >= X(x) because [67], by (Select) 67] X(x) >= X(x) because [68], by (Meta) 68] x >= x by (Var) 69] Y >= Y by (Meta) 70] d(/\x.cos(X(x)), Y) >= star(sin(Y), d(/\x.X(x), Y)) because [71], by (Star) 71] d*(/\x.cos(X(x)), Y) >= star(sin(Y), d(/\x.X(x), Y)) because d > star, [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] _|_ >= _|_ by (Bot) 83] star(_|_, X) >= _|_ by (Bot) 84] star(X, _|_) >= _|_ by (Bot) 85] plus(_|_, X) >= X because [86], by (Star) 86] plus*(_|_, X) >= X because [87], by (Select) 87] X >= X by (Meta) 88] d(F, X) >= d#(F, X) because [89], by (Star) 89] d*(F, X) >= d#(F, X) because d > d#, [90] and [92], by (Copy) 90] d*(F, X) >= F because [91], by (Select) 91] F >= F by (Meta) 92] d*(F, X) >= X because [93], by (Select) 93] 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.minus(X(x)), Y) =#> d#(/\y.X(y), Y) d#(/\x.star(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) 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.minus(X(x)), Y) >? d#(/\y.X(y), Y) d#(/\x.star(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) 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) minus = \y0.3 + 3y0 star = \y0y1.3 + 3y0 Using this interpretation, the requirements translate to: [[d#(/\x.minus(_x0(x)), _x1)]] = 18 + 3x1 + 3x1F0(x1) + 9F0(0) + 9F0(x1) > 3F0(0) + 3F0(x1) + x1F0(x1) = [[d#(/\x._x0(x), _x1)]] [[d#(/\x.star(_x0(x), _x1(x)), _x2)]] = 18 + 3x2 + 3x2F0(x2) + 9F0(0) + 9F0(x2) > 3F0(0) + 3F0(x2) + x2F0(x2) = [[d#(/\x._x0(x), _x2)]] 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.