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]] = _|_ [[~c0]] = _|_ [[~c1]] = _|_ [[~c2]] = _|_ [[~c3]] = _|_ [[~c4]] = _|_ [[~c5]] = _|_ [[~c6]] = _|_ We choose Lex = {} and Mul = {cos, d, d#, minus, plus, sin, star}, and the following precedence: d > cos > d# > minus > plus > star > sin 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) >= 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.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 [2], by definition 2] d#*(/\x.minus(X(x)), Y) >= d#(/\x.X(x), Y) because d# in Mul, [3] and [8], by (Stat) 3] /\x.minus(X(x)) > /\x.X(x) because [4], by definition 4] /\y.minus*(X(y)) >= /\y.X(y) because [5], by (Abs) 5] minus*(X(x)) >= X(x) because [6], by (Select) 6] X(x) >= X(x) because [7], by (Meta) 7] x >= x by (Var) 8] Y >= Y by (Meta) 9] d#(/\x.minus(X(x)), Y) >= X(_|_) because [10], by (Star) 10] d#*(/\x.minus(X(x)), Y) >= X(_|_) because [11], by (Select) 11] minus(X(d#*(/\x.minus(X(x)), Y))) >= X(_|_) because [12], by (Star) 12] minus*(X(d#*(/\x.minus(X(x)), Y))) >= X(_|_) because [13], by (Select) 13] X(d#*(/\x.minus(X(x)), Y)) >= X(_|_) because [14], by (Meta) 14] d#*(/\x.minus(X(x)), Y) >= _|_ by (Bot) 15] d#(/\x.plus(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because d# in Mul, [16] and [21], by (Fun) 16] /\y.plus(X(y), Y(y)) >= /\y.X(y) because [17], by (Abs) 17] plus(X(x), Y(x)) >= X(x) because [18], by (Star) 18] plus*(X(x), Y(x)) >= X(x) because [19], by (Select) 19] X(x) >= X(x) because [20], by (Meta) 20] x >= x by (Var) 21] Z >= Z by (Meta) 22] d#(/\x.plus(X(x), Y(x)), Z) >= X(_|_) because [23], by (Star) 23] d#*(/\x.plus(X(x), Y(x)), Z) >= X(_|_) because [24], by (Select) 24] plus(X(d#*(/\x.plus(X(x), Y(x)), Z)), Y(d#*(/\y.plus(X(y), Y(y)), Z))) >= X(_|_) because [25], by (Star) 25] plus*(X(d#*(/\x.plus(X(x), Y(x)), Z)), Y(d#*(/\y.plus(X(y), Y(y)), Z))) >= X(_|_) because [26], by (Select) 26] X(d#*(/\x.plus(X(x), Y(x)), Z)) >= X(_|_) because [27], by (Meta) 27] d#*(/\x.plus(X(x), Y(x)), Z) >= _|_ by (Bot) 28] d#(/\x.plus(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) because d# in Mul, [29] and [21], by (Fun) 29] /\y.plus(X(y), Y(y)) >= /\y.Y(y) because [30], by (Abs) 30] plus(X(x), Y(x)) >= Y(x) because [31], by (Star) 31] plus*(X(x), Y(x)) >= Y(x) because [32], by (Select) 32] Y(x) >= Y(x) because [33], by (Meta) 33] x >= x by (Var) 34] d#(/\x.plus(X(x), Y(x)), Z) > Y(_|_) because [35], by definition 35] d#*(/\x.plus(X(x), Y(x)), Z) >= Y(_|_) because [36], by (Select) 36] plus(X(d#*(/\x.plus(X(x), Y(x)), Z)), Y(d#*(/\y.plus(X(y), Y(y)), Z))) >= Y(_|_) because [37], by (Star) 37] plus*(X(d#*(/\x.plus(X(x), Y(x)), Z)), Y(d#*(/\y.plus(X(y), Y(y)), Z))) >= Y(_|_) because [38], by (Select) 38] Y(d#*(/\x.plus(X(x), Y(x)), Z)) >= Y(_|_) because [39], by (Meta) 39] d#*(/\x.plus(X(x), Y(x)), Z) >= _|_ by (Bot) 40] d#(/\x.star(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because d# in Mul, [41] and [46], by (Fun) 41] /\y.star(X(y), Y(y)) >= /\y.X(y) because [42], by (Abs) 42] star(X(x), Y(x)) >= X(x) because [43], by (Star) 43] star*(X(x), Y(x)) >= X(x) because [44], by (Select) 44] X(x) >= X(x) because [45], by (Meta) 45] x >= x by (Var) 46] Z >= Z by (Meta) 47] d#(/\x.star(X(x), Y(x)), Z) > X(_|_) because [48], by definition 48] d#*(/\x.star(X(x), Y(x)), Z) >= X(_|_) 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(_|_) 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(_|_) because [51], by (Select) 51] X(d#*(/\x.star(X(x), Y(x)), Z)) >= X(_|_) because [52], by (Meta) 52] d#*(/\x.star(X(x), Y(x)), Z) >= _|_ by (Bot) 53] d#(/\x.star(X(x), Y(x)), Z) > Y(Z) because [54], by definition 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 [46], by (Select) 59] d#(/\x.star(X(x), Y(x)), Z) >= X(Z) because [60], by (Star) 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 [46], by (Fun) 65] /\y.star(X(y), Y(y)) >= /\y.Y(y) because [66], by (Abs) 66] star(X(x), Y(x)) >= Y(x) because [67], by (Star) 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.star(X(x), Y(x)), Z) >= Y(_|_) because [71], by (Star) 71] d#*(/\x.star(X(x), Y(x)), Z) >= Y(_|_) because [72], by (Select) 72] star(X(d#*(/\x.star(X(x), Y(x)), Z)), Y(d#*(/\y.star(X(y), Y(y)), Z))) >= Y(_|_) because [73], by (Star) 73] star*(X(d#*(/\x.star(X(x), Y(x)), Z)), Y(d#*(/\y.star(X(y), Y(y)), Z))) >= Y(_|_) because [74], by (Select) 74] Y(d#*(/\x.star(X(x), Y(x)), Z)) >= Y(_|_) because [75], by (Meta) 75] d#*(/\x.star(X(x), Y(x)), Z) >= _|_ by (Bot) 76] d#(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y) because d# in Mul, [77] and [82], by (Fun) 77] /\y.sin(X(y)) >= /\y.X(y) because [78], by (Abs) 78] sin(X(x)) >= X(x) because [79], by (Star) 79] sin*(X(x)) >= X(x) because [80], by (Select) 80] X(x) >= X(x) because [81], by (Meta) 81] x >= x by (Var) 82] Y >= Y by (Meta) 83] d#(/\x.sin(X(x)), Y) > X(_|_) because [84], by definition 84] d#*(/\x.sin(X(x)), Y) >= X(_|_) because [85], by (Select) 85] sin(X(d#*(/\x.sin(X(x)), Y))) >= X(_|_) because [86], by (Star) 86] sin*(X(d#*(/\x.sin(X(x)), Y))) >= X(_|_) because [87], by (Select) 87] X(d#*(/\x.sin(X(x)), Y)) >= X(_|_) because [88], by (Meta) 88] d#*(/\x.sin(X(x)), Y) >= _|_ by (Bot) 89] d#(/\x.cos(X(x)), Y) >= d#(/\x.X(x), Y) because d# in Mul, [90] and [95], by (Fun) 90] /\y.cos(X(y)) >= /\y.X(y) because [91], by (Abs) 91] cos(X(x)) >= X(x) because [92], by (Star) 92] cos*(X(x)) >= X(x) because [93], by (Select) 93] X(x) >= X(x) because [94], by (Meta) 94] x >= x by (Var) 95] Y >= Y by (Meta) 96] d#(/\x.cos(X(x)), Y) >= X(_|_) because [97], by (Star) 97] d#*(/\x.cos(X(x)), Y) >= X(_|_) because [98], by (Select) 98] cos(X(d#*(/\x.cos(X(x)), Y))) >= X(_|_) because [99], by (Star) 99] cos*(X(d#*(/\x.cos(X(x)), Y))) >= X(_|_) because [100], by (Select) 100] X(d#*(/\x.cos(X(x)), Y)) >= X(_|_) because [101], by (Meta) 101] d#*(/\x.cos(X(x)), Y) >= _|_ by (Bot) 102] d(/\x.X, Y) >= _|_ by (Bot) 103] d(/\x.x, X) >= _|_ by (Bot) 104] d(/\x.minus(X(x)), Y) >= minus(d(/\x.X(x), Y)) because [105], by (Star) 105] d*(/\x.minus(X(x)), Y) >= minus(d(/\x.X(x), Y)) because d > minus and [106], by (Copy) 106] d*(/\x.minus(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [3] and [8], by (Stat) 107] d(/\x.plus(X(x), Y(x)), Z) >= plus(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because [108], by (Star) 108] d*(/\x.plus(X(x), Y(x)), Z) >= plus(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because d > plus, [109] and [115], by (Copy) 109] d*(/\x.plus(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [110] and [21], by (Stat) 110] /\x.plus(X(x), Y(x)) > /\x.X(x) because [111], by definition 111] /\y.plus*(X(y), Y(y)) >= /\y.X(y) because [112], by (Abs) 112] plus*(X(x), Y(x)) >= X(x) because [113], by (Select) 113] X(x) >= X(x) because [114], by (Meta) 114] x >= x by (Var) 115] d*(/\y.plus(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because d in Mul, [116] and [21], by (Stat) 116] /\y.plus(X(y), Y(y)) > /\y.Y(y) because [117], by definition 117] /\z.plus*(X(z), Y(z)) >= /\z.Y(z) because [118], by (Abs) 118] plus*(X(y), Y(y)) >= Y(y) because [119], by (Select) 119] Y(y) >= Y(y) because [120], by (Meta) 120] y >= y by (Var) 121] 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 [122], by (Star) 122] 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, [123] and [135], by (Copy) 123] d*(/\x.star(X(x), Y(x)), Z) >= star(d(/\x.X(x), Z), Y(Z)) because d > star, [124] and [130], by (Copy) 124] d*(/\x.star(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [125] and [46], by (Stat) 125] /\x.star(X(x), Y(x)) > /\x.X(x) because [126], by definition 126] /\y.star*(X(y), Y(y)) >= /\y.X(y) because [127], by (Abs) 127] star*(X(x), Y(x)) >= X(x) because [128], by (Select) 128] X(x) >= X(x) because [129], by (Meta) 129] x >= x by (Var) 130] d*(/\y.star(X(y), Y(y)), Z) >= Y(Z) because [131], by (Select) 131] star(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= Y(Z) because [132], by (Star) 132] star*(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= Y(Z) because [133], by (Select) 133] Y(d*(/\y.star(X(y), Y(y)), Z)) >= Y(Z) because [134], by (Meta) 134] d*(/\y.star(X(y), Y(y)), Z) >= Z because [46], by (Select) 135] d*(/\y.star(X(y), Y(y)), Z) >= star(X(Z), d(/\y.Y(y), Z)) because d > star, [136] and [140], by (Copy) 136] d*(/\y.star(X(y), Y(y)), Z) >= X(Z) because [137], by (Select) 137] star(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= X(Z) because [138], by (Star) 138] star*(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= X(Z) because [139], by (Select) 139] X(d*(/\y.star(X(y), Y(y)), Z)) >= X(Z) because [134], by (Meta) 140] d*(/\y.star(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because d in Mul, [141] and [46], by (Stat) 141] /\y.star(X(y), Y(y)) > /\y.Y(y) because [142], by definition 142] /\z.star*(X(z), Y(z)) >= /\z.Y(z) because [143], by (Abs) 143] star*(X(y), Y(y)) >= Y(y) because [144], by (Select) 144] Y(y) >= Y(y) because [145], by (Meta) 145] y >= y by (Var) 146] d(/\x.sin(X(x)), Y) >= star(cos(Y), d(/\x.X(x), Y)) because [147], by (Star) 147] d*(/\x.sin(X(x)), Y) >= star(cos(Y), d(/\x.X(x), Y)) because d > star, [148] and [150], by (Copy) 148] d*(/\x.sin(X(x)), Y) >= cos(Y) because d > cos and [149], by (Copy) 149] d*(/\x.sin(X(x)), Y) >= Y because [82], by (Select) 150] d*(/\x.sin(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [151] and [82], by (Stat) 151] /\x.sin(X(x)) > /\x.X(x) because [152], by definition 152] /\y.sin*(X(y)) >= /\y.X(y) because [153], by (Abs) 153] sin*(X(x)) >= X(x) because [154], by (Select) 154] X(x) >= X(x) because [155], by (Meta) 155] x >= x by (Var) 156] d(/\x.cos(X(x)), Y) >= star(minus(sin(Y)), d(/\x.X(x), Y)) because [157], by (Star) 157] d*(/\x.cos(X(x)), Y) >= star(minus(sin(Y)), d(/\x.X(x), Y)) because d > star, [158] and [161], by (Copy) 158] d*(/\x.cos(X(x)), Y) >= minus(sin(Y)) because d > minus and [159], by (Copy) 159] d*(/\x.cos(X(x)), Y) >= sin(Y) because d > sin and [160], by (Copy) 160] d*(/\x.cos(X(x)), Y) >= Y because [95], by (Select) 161] d*(/\x.cos(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [162] and [95], by (Stat) 162] /\x.cos(X(x)) > /\x.X(x) because [163], by definition 163] /\y.cos*(X(y)) >= /\y.X(y) because [164], by (Abs) 164] cos*(X(x)) >= X(x) because [165], by (Select) 165] X(x) >= X(x) because [166], by (Meta) 166] x >= x by (Var) 167] minus(_|_) >= _|_ by (Bot) 168] star(_|_, X) >= _|_ by (Bot) 169] star(X, _|_) >= _|_ by (Bot) 170] plus(_|_, X) >= X because [171], by (Star) 171] plus*(_|_, X) >= X because [172], by (Select) 172] X >= X by (Meta) 173] d(F, X) >= d#(F, X) because [174], by (Star) 174] d*(F, X) >= d#(F, X) because d > d#, [175] and [177], by (Copy) 175] d*(F, X) >= F because [176], by (Select) 176] F >= F by (Meta) 177] d*(F, X) >= X because [178], by (Select) 178] 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) =#> 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.star(X(x), Y(x)), Z) =#> d#(/\y.X(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.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) >? 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.star(X(x), Y(x)), Z) >? d#(/\y.X(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(~c2) d#(/\x.sin(X(x)), Y) >? d#(/\y.X(y), Y) d#(/\x.cos(X(x)), Y) >? d#(/\y.X(y), Y) d#(/\x.cos(X(x)), Y) >? X(~c3) 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]] = _|_ 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) >= 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.star(X(x), Y(x)), Z) >= d#(/\x.X(x), 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.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) >= X(_|_) because [2], by (Star) 2] d#*(/\x.X(x), Y) >= X(_|_) because [3], by (Select) 3] X(d#*(/\x.X(x), Y)) >= X(_|_) because [4], by (Meta) 4] d#*(/\x.X(x), Y) >= _|_ by (Bot) 5] d#(/\x.plus(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because d# in Mul, [6] and [11], by (Fun) 6] /\y.plus(X(y), Y(y)) >= /\y.X(y) because [7], by (Abs) 7] plus(X(x), Y(x)) >= X(x) because [8], by (Star) 8] plus*(X(x), Y(x)) >= X(x) because [9], by (Select) 9] X(x) >= X(x) because [10], by (Meta) 10] x >= x by (Var) 11] Z >= Z by (Meta) 12] d#(/\x.plus(X(x), Y(x)), Z) > X(_|_) because [13], by definition 13] d#*(/\x.plus(X(x), Y(x)), Z) >= X(_|_) because [14], by (Select) 14] plus(X(d#*(/\x.plus(X(x), Y(x)), Z)), Y(d#*(/\y.plus(X(y), Y(y)), Z))) >= X(_|_) because [15], by (Star) 15] plus*(X(d#*(/\x.plus(X(x), Y(x)), Z)), Y(d#*(/\y.plus(X(y), Y(y)), Z))) >= X(_|_) because [16], by (Select) 16] X(d#*(/\x.plus(X(x), Y(x)), Z)) >= X(_|_) because [17], by (Meta) 17] d#*(/\x.plus(X(x), Y(x)), Z) >= _|_ by (Bot) 18] d#(/\x.plus(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) because d# in Mul, [19] and [11], by (Fun) 19] /\y.plus(X(y), Y(y)) >= /\y.Y(y) because [20], by (Abs) 20] plus(X(x), Y(x)) >= Y(x) because [21], by (Star) 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.star(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because d# in Mul, [25] and [30], by (Fun) 25] /\y.star(X(y), Y(y)) >= /\y.X(y) because [26], by (Abs) 26] star(X(x), Y(x)) >= X(x) because [27], by (Star) 27] star*(X(x), Y(x)) >= X(x) because [28], by (Select) 28] X(x) >= X(x) because [29], by (Meta) 29] x >= x by (Var) 30] Z >= Z by (Meta) 31] d#(/\x.star(X(x), Y(x)), Z) >= X(Z) because [32], by (Star) 32] d#*(/\x.star(X(x), Y(x)), Z) >= X(Z) because [33], by (Select) 33] star(X(d#*(/\x.star(X(x), Y(x)), Z)), Y(d#*(/\y.star(X(y), Y(y)), Z))) >= X(Z) because [34], by (Star) 34] star*(X(d#*(/\x.star(X(x), Y(x)), Z)), Y(d#*(/\y.star(X(y), Y(y)), Z))) >= X(Z) because [35], by (Select) 35] X(d#*(/\x.star(X(x), Y(x)), Z)) >= X(Z) because [36], by (Meta) 36] d#*(/\x.star(X(x), Y(x)), Z) >= Z because [30], by (Select) 37] d#(/\x.star(X(x), Y(x)), Z) > d#(/\x.Y(x), Z) because [38], by definition 38] d#*(/\x.star(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) because d# in Mul, [39] and [30], by (Stat) 39] /\x.star(X(x), Y(x)) > /\x.Y(x) because [40], by definition 40] /\y.star*(X(y), Y(y)) >= /\y.Y(y) because [41], by (Abs) 41] star*(X(x), Y(x)) >= Y(x) because [42], by (Select) 42] Y(x) >= Y(x) because [43], by (Meta) 43] x >= x by (Var) 44] d#(/\x.star(X(x), Y(x)), Z) >= Y(_|_) because [45], by (Star) 45] d#*(/\x.star(X(x), Y(x)), Z) >= Y(_|_) because [46], by (Select) 46] star(X(d#*(/\x.star(X(x), Y(x)), Z)), Y(d#*(/\y.star(X(y), Y(y)), Z))) >= Y(_|_) because [47], by (Star) 47] star*(X(d#*(/\x.star(X(x), Y(x)), Z)), Y(d#*(/\y.star(X(y), Y(y)), Z))) >= Y(_|_) because [48], by (Select) 48] Y(d#*(/\x.star(X(x), Y(x)), Z)) >= Y(_|_) because [49], by (Meta) 49] d#*(/\x.star(X(x), Y(x)), Z) >= _|_ by (Bot) 50] d#(/\x.sin(X(x)), Y) > d#(/\x.X(x), Y) because [51], by definition 51] d#*(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y) because d# in Mul, [52] and [57], by (Stat) 52] /\x.sin(X(x)) > /\x.X(x) because [53], by definition 53] /\y.sin*(X(y)) >= /\y.X(y) because [54], by (Abs) 54] sin*(X(x)) >= X(x) because [55], by (Select) 55] X(x) >= X(x) because [56], by (Meta) 56] x >= x by (Var) 57] Y >= Y by (Meta) 58] d#(/\x.cos(X(x)), Y) > d#(/\x.X(x), Y) because [59], by definition 59] d#*(/\x.cos(X(x)), Y) >= d#(/\x.X(x), Y) because d# in Mul, [60] and [65], by (Stat) 60] /\x.cos(X(x)) > /\x.X(x) because [61], by definition 61] /\y.cos*(X(y)) >= /\y.X(y) because [62], by (Abs) 62] cos*(X(x)) >= X(x) because [63], by (Select) 63] X(x) >= X(x) because [64], by (Meta) 64] x >= x by (Var) 65] Y >= Y by (Meta) 66] d#(/\x.cos(X(x)), Y) > X(_|_) because [67], by definition 67] d#*(/\x.cos(X(x)), Y) >= X(_|_) because [68], by (Select) 68] cos(X(d#*(/\x.cos(X(x)), Y))) >= X(_|_) because [69], by (Star) 69] cos*(X(d#*(/\x.cos(X(x)), Y))) >= X(_|_) because [70], by (Select) 70] X(d#*(/\x.cos(X(x)), Y)) >= X(_|_) because [71], by (Meta) 71] d#*(/\x.cos(X(x)), Y) >= _|_ by (Bot) 72] d(/\x.X, Y) >= _|_ by (Bot) 73] d(/\x.x, X) >= _|_ by (Bot) 74] d(/\x.X(x), Y) >= d(/\x.X(x), Y) because d in Mul, [75] and [78], by (Fun) 75] /\y.X(y) >= /\y.X(y) because [76], by (Abs) 76] X(x) >= X(x) because [77], by (Meta) 77] x >= x by (Var) 78] Y >= Y by (Meta) 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 [11], 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 [11], 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 [30], 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 [30], 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, [39] and [30], by (Stat) 113] d(/\x.sin(X(x)), Y) >= star(cos(Y), d(/\x.X(x), Y)) because [114], by (Star) 114] d*(/\x.sin(X(x)), Y) >= star(cos(Y), d(/\x.X(x), Y)) because d > star, [115] and [117], by (Copy) 115] d*(/\x.sin(X(x)), Y) >= cos(Y) because d > cos and [116], by (Copy) 116] d*(/\x.sin(X(x)), Y) >= Y because [57], by (Select) 117] d*(/\x.sin(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [52] and [57], by (Stat) 118] d(/\x.cos(X(x)), Y) >= star(sin(Y), d(/\x.X(x), Y)) because [119], by (Star) 119] d*(/\x.cos(X(x)), Y) >= star(sin(Y), d(/\x.X(x), Y)) because d > star, [120] and [122], by (Copy) 120] d*(/\x.cos(X(x)), Y) >= sin(Y) because d > sin and [121], by (Copy) 121] d*(/\x.cos(X(x)), Y) >= Y because [65], by (Select) 122] d*(/\x.cos(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [60] and [65], by (Stat) 123] _|_ >= _|_ by (Bot) 124] star(_|_, X) >= _|_ by (Bot) 125] star(X, _|_) >= _|_ by (Bot) 126] plus(_|_, X) >= X because [127], by (Star) 127] plus*(_|_, X) >= X because [128], by (Select) 128] X >= X by (Meta) 129] d(F, X) >= d#(F, X) because [130], by (Star) 130] d*(F, X) >= d#(F, X) because d > d#, [131] and [133], by (Copy) 131] d*(F, X) >= F because [132], by (Select) 132] F >= F by (Meta) 133] d*(F, X) >= X because [134], by (Select) 134] 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) =#> 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.star(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) d#(/\x.star(X(x), Y(x)), Z) =#> X(Z) d#(/\x.star(X(x), Y(x)), Z) =#> 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) >? 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.star(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) d#(/\x.star(X(x), Y(x)), Z) >? X(Z) d#(/\x.star(X(x), Y(x)), Z) >? Y(~c1) 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# > plus > sin > cos > 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) >= 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.star(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) d#(/\x.star(X(x), Y(x)), Z) > X(Z) d#(/\x.star(X(x), Y(x)), Z) >= 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) >= X(_|_) because [2], by (Star) 2] d#*(/\x.X(x), Y) >= X(_|_) because [3], by (Select) 3] X(d#*(/\x.X(x), Y)) >= X(_|_) because [4], by (Meta) 4] d#*(/\x.X(x), Y) >= _|_ by (Bot) 5] d#(/\x.plus(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because d# in Mul, [6] and [11], by (Fun) 6] /\y.plus(X(y), Y(y)) >= /\y.X(y) because [7], by (Abs) 7] plus(X(x), Y(x)) >= X(x) because [8], by (Star) 8] plus*(X(x), Y(x)) >= X(x) because [9], by (Select) 9] X(x) >= X(x) because [10], by (Meta) 10] x >= x by (Var) 11] Z >= Z by (Meta) 12] d#(/\x.plus(X(x), Y(x)), Z) > d#(/\x.Y(x), Z) because [13], by definition 13] d#*(/\x.plus(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) because d# in Mul, [14] and [11], by (Stat) 14] /\x.plus(X(x), Y(x)) > /\x.Y(x) because [15], by definition 15] /\y.plus*(X(y), Y(y)) >= /\y.Y(y) because [16], by (Abs) 16] plus*(X(x), Y(x)) >= Y(x) because [17], by (Select) 17] Y(x) >= Y(x) because [18], by (Meta) 18] x >= x by (Var) 19] d#(/\x.star(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because [20], by (Star) 20] d#*(/\x.star(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because d# in Mul, [21] and [26], by (Stat) 21] /\x.star(X(x), Y(x)) > /\x.X(x) because [22], by definition 22] /\y.star*(X(y), Y(y)) >= /\y.X(y) because [23], by (Abs) 23] star*(X(x), Y(x)) >= X(x) because [24], by (Select) 24] X(x) >= X(x) because [25], by (Meta) 25] x >= x by (Var) 26] Z >= Z by (Meta) 27] d#(/\x.star(X(x), Y(x)), Z) > X(Z) because [28], by definition 28] d#*(/\x.star(X(x), Y(x)), Z) >= X(Z) because [29], by (Select) 29] star(X(d#*(/\x.star(X(x), Y(x)), Z)), Y(d#*(/\y.star(X(y), Y(y)), Z))) >= X(Z) because [30], by (Star) 30] star*(X(d#*(/\x.star(X(x), Y(x)), Z)), Y(d#*(/\y.star(X(y), Y(y)), Z))) >= X(Z) because [31], by (Select) 31] X(d#*(/\x.star(X(x), Y(x)), Z)) >= X(Z) because [32], by (Meta) 32] d#*(/\x.star(X(x), Y(x)), Z) >= Z because [26], by (Select) 33] d#(/\x.star(X(x), Y(x)), Z) >= Y(_|_) because [34], by (Star) 34] d#*(/\x.star(X(x), Y(x)), Z) >= Y(_|_) because [35], by (Select) 35] star(X(d#*(/\x.star(X(x), Y(x)), Z)), Y(d#*(/\y.star(X(y), Y(y)), Z))) >= Y(_|_) because [36], by (Star) 36] star*(X(d#*(/\x.star(X(x), Y(x)), Z)), Y(d#*(/\y.star(X(y), Y(y)), Z))) >= Y(_|_) because [37], by (Select) 37] Y(d#*(/\x.star(X(x), Y(x)), Z)) >= Y(_|_) because [38], by (Meta) 38] d#*(/\x.star(X(x), Y(x)), Z) >= _|_ by (Bot) 39] d(/\x.X, Y) >= _|_ by (Bot) 40] d(/\x.x, X) >= _|_ by (Bot) 41] d(/\x.X(x), Y) >= d(/\x.X(x), Y) because d in Mul, [42] and [45], by (Fun) 42] /\y.X(y) >= /\y.X(y) because [43], by (Abs) 43] X(x) >= X(x) because [44], by (Meta) 44] x >= x by (Var) 45] Y >= Y by (Meta) 46] d(/\x.plus(X(x), Y(x)), Z) >= plus(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because [47], by (Star) 47] d*(/\x.plus(X(x), Y(x)), Z) >= plus(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because d > plus, [48] and [54], by (Copy) 48] d*(/\x.plus(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [49] and [11], by (Stat) 49] /\x.plus(X(x), Y(x)) > /\x.X(x) because [50], by definition 50] /\y.plus*(X(y), Y(y)) >= /\y.X(y) because [51], by (Abs) 51] plus*(X(x), Y(x)) >= X(x) because [52], by (Select) 52] X(x) >= X(x) because [53], by (Meta) 53] x >= x by (Var) 54] d*(/\y.plus(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because d in Mul, [14] and [11], by (Stat) 55] 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 [56], by (Star) 56] 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, [57] and [64], by (Copy) 57] d*(/\x.star(X(x), Y(x)), Z) >= star(d(/\x.X(x), Z), Y(Z)) because d > star, [58] and [59], by (Copy) 58] d*(/\x.star(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [21] and [26], by (Stat) 59] d*(/\x.star(X(x), Y(x)), Z) >= Y(Z) because [60], by (Select) 60] star(X(d*(/\x.star(X(x), Y(x)), Z)), Y(d*(/\y.star(X(y), Y(y)), Z))) >= Y(Z) because [61], by (Star) 61] star*(X(d*(/\x.star(X(x), Y(x)), Z)), Y(d*(/\y.star(X(y), Y(y)), Z))) >= Y(Z) because [62], by (Select) 62] Y(d*(/\x.star(X(x), Y(x)), Z)) >= Y(Z) because [63], by (Meta) 63] d*(/\x.star(X(x), Y(x)), Z) >= Z because [26], by (Select) 64] d*(/\x.star(X(x), Y(x)), Z) >= star(X(Z), d(/\x.Y(x), Z)) because d > star, [65] and [69], by (Copy) 65] d*(/\x.star(X(x), Y(x)), Z) >= X(Z) because [66], by (Select) 66] star(X(d*(/\x.star(X(x), Y(x)), Z)), Y(d*(/\y.star(X(y), Y(y)), Z))) >= X(Z) because [67], by (Star) 67] star*(X(d*(/\x.star(X(x), Y(x)), Z)), Y(d*(/\y.star(X(y), Y(y)), Z))) >= X(Z) because [68], by (Select) 68] X(d*(/\x.star(X(x), Y(x)), Z)) >= X(Z) because [63], by (Meta) 69] d*(/\x.star(X(x), Y(x)), Z) >= d(/\x.Y(x), Z) because d in Mul, [70] and [26], by (Stat) 70] /\x.star(X(x), Y(x)) > /\x.Y(x) because [71], by definition 71] /\y.star*(X(y), Y(y)) >= /\y.Y(y) because [72], by (Abs) 72] star*(X(x), Y(x)) >= Y(x) because [73], by (Select) 73] Y(x) >= Y(x) because [74], by (Meta) 74] x >= x by (Var) 75] d(/\x.sin(X(x)), Y) >= star(cos(Y), d(/\x.X(x), Y)) because [76], by (Star) 76] d*(/\x.sin(X(x)), Y) >= star(cos(Y), d(/\x.X(x), Y)) because d > star, [77] and [80], by (Copy) 77] d*(/\x.sin(X(x)), Y) >= cos(Y) because d > cos and [78], by (Copy) 78] d*(/\x.sin(X(x)), Y) >= Y because [79], by (Select) 79] Y >= Y by (Meta) 80] d*(/\x.sin(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [81] and [86], by (Stat) 81] /\x.sin(X(x)) > /\x.X(x) because [82], by definition 82] /\y.sin*(X(y)) >= /\y.X(y) because [83], by (Abs) 83] sin*(X(x)) >= X(x) because [84], by (Select) 84] X(x) >= X(x) because [85], by (Meta) 85] x >= x by (Var) 86] Y >= Y by (Meta) 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_3, R_0, minimal, all) by (P_4, R_0, minimal, all), where P_4 consists of: d#(/\x.minus(X(x)), Y) =#> X(y) d#(/\x.plus(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) d#(/\x.star(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) d#(/\x.star(X(x), Y(x)), Z) =#> 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) >? X(~c0) d#(/\x.plus(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) d#(/\x.star(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) d#(/\x.star(X(x), Y(x)), Z) >? Y(~c1) 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 = {} and Mul = {cos, d, 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) >= X(_|_) d#(/\x.plus(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) d#(/\x.star(X(x), Y(x)), Z) > d#(/\x.X(x), Z) d#(/\x.star(X(x), Y(x)), Z) >= 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) >= X(_|_) because [2], by (Star) 2] d#*(/\x.minus(X(x)), Y) >= X(_|_) because [3], by (Select) 3] minus(X(d#*(/\x.minus(X(x)), Y))) >= X(_|_) because [4], by (Star) 4] minus*(X(d#*(/\x.minus(X(x)), Y))) >= X(_|_) because [5], by (Select) 5] X(d#*(/\x.minus(X(x)), Y)) >= X(_|_) because [6], by (Meta) 6] d#*(/\x.minus(X(x)), Y) >= _|_ by (Bot) 7] d#(/\x.plus(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because d# in Mul, [8] and [13], by (Fun) 8] /\y.plus(X(y), Y(y)) >= /\y.X(y) because [9], by (Abs) 9] plus(X(x), Y(x)) >= X(x) because [10], by (Star) 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.star(X(x), Y(x)), Z) > d#(/\x.X(x), Z) because [15], by definition 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#(/\x.star(X(x), Y(x)), Z) >= Y(_|_) because [23], by (Star) 23] d#*(/\x.star(X(x), Y(x)), Z) >= Y(_|_) because [24], by (Select) 24] star(X(d#*(/\x.star(X(x), Y(x)), Z)), Y(d#*(/\y.star(X(y), Y(y)), Z))) >= Y(_|_) because [25], by (Star) 25] star*(X(d#*(/\x.star(X(x), Y(x)), Z)), Y(d#*(/\y.star(X(y), Y(y)), Z))) >= Y(_|_) because [26], by (Select) 26] Y(d#*(/\x.star(X(x), Y(x)), Z)) >= Y(_|_) because [27], by (Meta) 27] d#*(/\x.star(X(x), Y(x)), Z) >= _|_ by (Bot) 28] d(/\x.X, Y) >= _|_ by (Bot) 29] d(/\x.x, X) >= _|_ by (Bot) 30] d(/\x.minus(X(x)), Y) >= minus(d(/\x.X(x), Y)) because [31], by (Star) 31] d*(/\x.minus(X(x)), Y) >= minus(d(/\x.X(x), Y)) because d > minus and [32], by (Copy) 32] d*(/\x.minus(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [33] and [38], by (Stat) 33] /\x.minus(X(x)) > /\x.X(x) because [34], by definition 34] /\y.minus*(X(y)) >= /\y.X(y) because [35], by (Abs) 35] minus*(X(x)) >= X(x) because [36], by (Select) 36] X(x) >= X(x) because [37], by (Meta) 37] x >= x by (Var) 38] Y >= Y by (Meta) 39] d(/\x.plus(X(x), Y(x)), Z) >= plus(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because [40], by (Star) 40] d*(/\x.plus(X(x), Y(x)), Z) >= plus(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because d > plus, [41] and [47], by (Copy) 41] d*(/\x.plus(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [42] and [13], by (Stat) 42] /\x.plus(X(x), Y(x)) > /\x.X(x) because [43], by definition 43] /\y.plus*(X(y), Y(y)) >= /\y.X(y) because [44], by (Abs) 44] plus*(X(x), Y(x)) >= X(x) because [45], by (Select) 45] X(x) >= X(x) because [46], by (Meta) 46] x >= x by (Var) 47] d*(/\y.plus(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because d in Mul, [48] and [13], by (Stat) 48] /\y.plus(X(y), Y(y)) > /\y.Y(y) because [49], by definition 49] /\z.plus*(X(z), Y(z)) >= /\z.Y(z) because [50], by (Abs) 50] plus*(X(y), Y(y)) >= Y(y) because [51], by (Select) 51] Y(y) >= Y(y) because [52], by (Meta) 52] y >= y by (Var) 53] d(/\x.star(X(x), Y(x)), Z) >= plus(star(d(/\x.X(x), Z), Y(Z)), star(X(Z), d(/\y.Y(y), Z))) because [54], by (Star) 54] 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, [55] and [62], by (Copy) 55] d*(/\x.star(X(x), Y(x)), Z) >= star(d(/\x.X(x), Z), Y(Z)) because d > star, [56] and [57], by (Copy) 56] d*(/\x.star(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [16] and [21], by (Stat) 57] d*(/\x.star(X(x), Y(x)), Z) >= Y(Z) because [58], by (Select) 58] star(X(d*(/\x.star(X(x), Y(x)), Z)), Y(d*(/\y.star(X(y), Y(y)), Z))) >= Y(Z) because [59], by (Star) 59] star*(X(d*(/\x.star(X(x), Y(x)), Z)), Y(d*(/\y.star(X(y), Y(y)), Z))) >= Y(Z) because [60], by (Select) 60] Y(d*(/\x.star(X(x), Y(x)), Z)) >= Y(Z) because [61], by (Meta) 61] d*(/\x.star(X(x), Y(x)), Z) >= Z because [21], by (Select) 62] d*(/\x.star(X(x), Y(x)), Z) >= star(X(Z), d(/\x.Y(x), Z)) because d > star, [63] and [67], by (Copy) 63] d*(/\x.star(X(x), Y(x)), Z) >= X(Z) because [64], by (Select) 64] star(X(d*(/\x.star(X(x), Y(x)), Z)), Y(d*(/\y.star(X(y), Y(y)), Z))) >= X(Z) because [65], by (Star) 65] star*(X(d*(/\x.star(X(x), Y(x)), Z)), Y(d*(/\y.star(X(y), Y(y)), Z))) >= X(Z) because [66], by (Select) 66] X(d*(/\x.star(X(x), Y(x)), Z)) >= X(Z) because [61], by (Meta) 67] d*(/\x.star(X(x), Y(x)), Z) >= d(/\x.Y(x), Z) because d in Mul, [68] and [21], by (Stat) 68] /\x.star(X(x), Y(x)) > /\x.Y(x) because [69], by definition 69] /\y.star*(X(y), Y(y)) >= /\y.Y(y) because [70], by (Abs) 70] star*(X(x), Y(x)) >= Y(x) because [71], by (Select) 71] Y(x) >= Y(x) because [72], by (Meta) 72] x >= x by (Var) 73] d(/\x.sin(X(x)), Y) >= star(cos(Y), d(/\x.X(x), Y)) because [74], by (Star) 74] d*(/\x.sin(X(x)), Y) >= star(cos(Y), d(/\x.X(x), Y)) because d > star, [75] and [78], by (Copy) 75] d*(/\x.sin(X(x)), Y) >= cos(Y) because d > cos and [76], by (Copy) 76] d*(/\x.sin(X(x)), Y) >= Y because [77], by (Select) 77] Y >= Y by (Meta) 78] d*(/\x.sin(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [79] and [84], by (Stat) 79] /\x.sin(X(x)) > /\x.X(x) because [80], by definition 80] /\y.sin*(X(y)) >= /\y.X(y) because [81], by (Abs) 81] sin*(X(x)) >= X(x) because [82], by (Select) 82] X(x) >= X(x) because [83], by (Meta) 83] x >= x by (Var) 84] Y >= Y by (Meta) 85] d(/\x.cos(X(x)), Y) >= star(minus(sin(Y)), d(/\x.X(x), Y)) because [86], by (Star) 86] d*(/\x.cos(X(x)), Y) >= star(minus(sin(Y)), d(/\x.X(x), Y)) because d > star, [87] and [91], by (Copy) 87] d*(/\x.cos(X(x)), Y) >= minus(sin(Y)) because d > minus and [88], by (Copy) 88] d*(/\x.cos(X(x)), Y) >= sin(Y) because d > sin and [89], by (Copy) 89] d*(/\x.cos(X(x)), Y) >= Y because [90], by (Select) 90] Y >= Y by (Meta) 91] d*(/\x.cos(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [92] and [97], by (Stat) 92] /\x.cos(X(x)) > /\x.X(x) because [93], by definition 93] /\y.cos*(X(y)) >= /\y.X(y) because [94], by (Abs) 94] cos*(X(x)) >= X(x) because [95], by (Select) 95] X(x) >= X(x) because [96], by (Meta) 96] x >= x by (Var) 97] Y >= Y by (Meta) 98] minus(_|_) >= _|_ by (Bot) 99] star(_|_, X) >= _|_ by (Bot) 100] star(X, _|_) >= _|_ by (Bot) 101] plus(_|_, X) >= X because [102], by (Star) 102] plus*(_|_, X) >= X because [103], by (Select) 103] X >= X by (Meta) 104] d(F, X) >= d#(F, X) because [105], by (Star) 105] d*(F, X) >= d#(F, X) because d > d#, [106] and [108], by (Copy) 106] d*(F, X) >= F because [107], by (Select) 107] F >= F by (Meta) 108] d*(F, X) >= X because [109], by (Select) 109] 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) =#> X(y) d#(/\x.plus(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) d#(/\x.star(X(x), Y(x)), Z) =#> Y(y) 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) >? X(~c0) d#(/\x.plus(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) d#(/\x.star(X(x), Y(x)), Z) >? Y(~c1) 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 = {} and Mul = {cos, d, 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) > X(_|_) d#(/\x.plus(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) d#(/\x.star(X(x), Y(x)), Z) >= 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) > X(_|_) because [2], by definition 2] d#*(/\x.minus(X(x)), Y) >= X(_|_) because [3], by (Select) 3] minus(X(d#*(/\x.minus(X(x)), Y))) >= X(_|_) because [4], by (Star) 4] minus*(X(d#*(/\x.minus(X(x)), Y))) >= X(_|_) because [5], by (Select) 5] X(d#*(/\x.minus(X(x)), Y)) >= X(_|_) because [6], by (Meta) 6] d#*(/\x.minus(X(x)), Y) >= _|_ by (Bot) 7] d#(/\x.plus(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because [8], by (Star) 8] d#*(/\x.plus(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because d# in Mul, [9] and [14], by (Stat) 9] /\x.plus(X(x), Y(x)) > /\x.X(x) because [10], by definition 10] /\y.plus*(X(y), Y(y)) >= /\y.X(y) because [11], by (Abs) 11] plus*(X(x), Y(x)) >= X(x) because [12], by (Select) 12] X(x) >= X(x) because [13], by (Meta) 13] x >= x by (Var) 14] Z >= Z by (Meta) 15] d#(/\x.star(X(x), Y(x)), Z) >= Y(_|_) because [16], by (Star) 16] d#*(/\x.star(X(x), Y(x)), Z) >= Y(_|_) because [17], by (Select) 17] star(X(d#*(/\x.star(X(x), Y(x)), Z)), Y(d#*(/\y.star(X(y), Y(y)), Z))) >= Y(_|_) because [18], by (Star) 18] star*(X(d#*(/\x.star(X(x), Y(x)), Z)), Y(d#*(/\y.star(X(y), Y(y)), Z))) >= Y(_|_) because [19], by (Select) 19] Y(d#*(/\x.star(X(x), Y(x)), Z)) >= Y(_|_) because [20], by (Meta) 20] d#*(/\x.star(X(x), Y(x)), Z) >= _|_ by (Bot) 21] d(/\x.X, Y) >= _|_ by (Bot) 22] d(/\x.x, X) >= _|_ by (Bot) 23] d(/\x.minus(X(x)), Y) >= minus(d(/\x.X(x), Y)) because [24], by (Star) 24] d*(/\x.minus(X(x)), Y) >= minus(d(/\x.X(x), Y)) because d > minus and [25], by (Copy) 25] d*(/\x.minus(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [26] and [31], by (Stat) 26] /\x.minus(X(x)) > /\x.X(x) because [27], by definition 27] /\y.minus*(X(y)) >= /\y.X(y) because [28], by (Abs) 28] minus*(X(x)) >= X(x) because [29], by (Select) 29] X(x) >= X(x) because [30], by (Meta) 30] x >= x by (Var) 31] Y >= Y by (Meta) 32] d(/\x.plus(X(x), Y(x)), Z) >= plus(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because [33], by (Star) 33] d*(/\x.plus(X(x), Y(x)), Z) >= plus(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because d > plus, [34] and [35], by (Copy) 34] d*(/\x.plus(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [9] and [14], by (Stat) 35] d*(/\x.plus(X(x), Y(x)), Z) >= d(/\x.Y(x), Z) because d in Mul, [36] and [14], by (Stat) 36] /\x.plus(X(x), Y(x)) > /\x.Y(x) because [37], by definition 37] /\y.plus*(X(y), Y(y)) >= /\y.Y(y) because [38], by (Abs) 38] plus*(X(x), Y(x)) >= Y(x) because [39], by (Select) 39] Y(x) >= Y(x) because [40], by (Meta) 40] x >= x by (Var) 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 [42], by (Star) 42] 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, [43] and [56], by (Copy) 43] d*(/\x.star(X(x), Y(x)), Z) >= star(d(/\x.X(x), Z), Y(Z)) because d > star, [44] and [51], by (Copy) 44] d*(/\x.star(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [45] and [50], by (Stat) 45] /\x.star(X(x), Y(x)) > /\x.X(x) because [46], by definition 46] /\y.star*(X(y), Y(y)) >= /\y.X(y) because [47], by (Abs) 47] star*(X(x), Y(x)) >= X(x) because [48], by (Select) 48] X(x) >= X(x) because [49], by (Meta) 49] x >= x by (Var) 50] Z >= Z by (Meta) 51] d*(/\y.star(X(y), Y(y)), Z) >= Y(Z) because [52], by (Select) 52] star(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= Y(Z) because [53], by (Star) 53] star*(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= Y(Z) because [54], by (Select) 54] Y(d*(/\y.star(X(y), Y(y)), Z)) >= Y(Z) because [55], by (Meta) 55] d*(/\y.star(X(y), Y(y)), Z) >= Z because [50], by (Select) 56] d*(/\y.star(X(y), Y(y)), Z) >= star(X(Z), d(/\y.Y(y), Z)) because d > star, [57] and [61], by (Copy) 57] d*(/\y.star(X(y), Y(y)), Z) >= X(Z) because [58], by (Select) 58] star(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= X(Z) because [59], by (Star) 59] star*(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= X(Z) because [60], by (Select) 60] X(d*(/\y.star(X(y), Y(y)), Z)) >= X(Z) because [55], by (Meta) 61] d*(/\y.star(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because d in Mul, [62] and [50], by (Stat) 62] /\y.star(X(y), Y(y)) > /\y.Y(y) because [63], by definition 63] /\z.star*(X(z), Y(z)) >= /\z.Y(z) because [64], by (Abs) 64] star*(X(y), Y(y)) >= Y(y) because [65], by (Select) 65] Y(y) >= Y(y) because [66], by (Meta) 66] y >= y by (Var) 67] d(/\x.sin(X(x)), Y) >= star(cos(Y), d(/\x.X(x), Y)) because [68], by (Star) 68] d*(/\x.sin(X(x)), Y) >= star(cos(Y), d(/\x.X(x), Y)) because d > star, [69] and [72], by (Copy) 69] d*(/\x.sin(X(x)), Y) >= cos(Y) because d > cos and [70], by (Copy) 70] d*(/\x.sin(X(x)), Y) >= Y because [71], by (Select) 71] Y >= Y by (Meta) 72] d*(/\x.sin(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [73] and [78], by (Stat) 73] /\x.sin(X(x)) > /\x.X(x) because [74], by definition 74] /\y.sin*(X(y)) >= /\y.X(y) because [75], by (Abs) 75] sin*(X(x)) >= X(x) because [76], by (Select) 76] X(x) >= X(x) because [77], by (Meta) 77] x >= x by (Var) 78] Y >= Y by (Meta) 79] d(/\x.cos(X(x)), Y) >= star(minus(sin(Y)), d(/\x.X(x), Y)) because [80], by (Star) 80] d*(/\x.cos(X(x)), Y) >= star(minus(sin(Y)), d(/\x.X(x), Y)) because d > star, [81] and [85], by (Copy) 81] d*(/\x.cos(X(x)), Y) >= minus(sin(Y)) because d > minus and [82], by (Copy) 82] d*(/\x.cos(X(x)), Y) >= sin(Y) because d > sin and [83], by (Copy) 83] d*(/\x.cos(X(x)), Y) >= Y because [84], by (Select) 84] Y >= Y by (Meta) 85] d*(/\x.cos(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [86] and [91], by (Stat) 86] /\x.cos(X(x)) > /\x.X(x) because [87], by definition 87] /\y.cos*(X(y)) >= /\y.X(y) because [88], by (Abs) 88] cos*(X(x)) >= X(x) because [89], by (Select) 89] X(x) >= X(x) because [90], by (Meta) 90] x >= x by (Var) 91] Y >= Y by (Meta) 92] minus(_|_) >= _|_ by (Bot) 93] star(_|_, X) >= _|_ by (Bot) 94] star(X, _|_) >= _|_ by (Bot) 95] plus(_|_, X) >= X because [96], by (Star) 96] plus*(_|_, X) >= X because [97], by (Select) 97] X >= X by (Meta) 98] d(F, X) >= d#(F, X) because [99], by (Star) 99] d*(F, X) >= d#(F, X) because d > d#, [100] and [102], by (Copy) 100] d*(F, X) >= F because [101], by (Select) 101] F >= F by (Meta) 102] d*(F, X) >= X because [103], by (Select) 103] 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.plus(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) d#(/\x.star(X(x), Y(x)), Z) =#> Y(y) 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.plus(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) d#(/\x.star(X(x), Y(x)), Z) >? Y(~c0) 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 > d# > plus > cos > sin > star Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: d#(/\x.plus(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) d#(/\x.star(X(x), Y(x)), Z) > 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.plus(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because d# in Mul, [2] and [7], by (Fun) 2] /\y.plus(X(y), Y(y)) >= /\y.X(y) because [3], by (Abs) 3] plus(X(x), Y(x)) >= X(x) because [4], by (Star) 4] plus*(X(x), Y(x)) >= X(x) because [5], by (Select) 5] X(x) >= X(x) because [6], by (Meta) 6] x >= x by (Var) 7] Z >= Z by (Meta) 8] d#(/\x.star(X(x), Y(x)), Z) > Y(_|_) because [9], by definition 9] d#*(/\x.star(X(x), Y(x)), Z) >= Y(_|_) because [10], by (Select) 10] star(X(d#*(/\x.star(X(x), Y(x)), Z)), Y(d#*(/\y.star(X(y), Y(y)), Z))) >= Y(_|_) because [11], by (Star) 11] star*(X(d#*(/\x.star(X(x), Y(x)), Z)), Y(d#*(/\y.star(X(y), Y(y)), Z))) >= Y(_|_) because [12], by (Select) 12] Y(d#*(/\x.star(X(x), Y(x)), Z)) >= Y(_|_) because [13], by (Meta) 13] d#*(/\x.star(X(x), Y(x)), Z) >= _|_ by (Bot) 14] d(/\x.X, Y) >= _|_ by (Bot) 15] d(/\x.x, X) >= _|_ by (Bot) 16] d(/\x.X(x), Y) >= d(/\x.X(x), Y) because d in Mul, [17] and [20], by (Fun) 17] /\y.X(y) >= /\y.X(y) because [18], by (Abs) 18] X(x) >= X(x) because [19], by (Meta) 19] x >= x by (Var) 20] Y >= Y by (Meta) 21] d(/\x.plus(X(x), Y(x)), Z) >= plus(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because [22], by (Star) 22] d*(/\x.plus(X(x), Y(x)), Z) >= plus(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because d > plus, [23] and [29], by (Copy) 23] d*(/\x.plus(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [24] and [7], by (Stat) 24] /\x.plus(X(x), Y(x)) > /\x.X(x) because [25], by definition 25] /\y.plus*(X(y), Y(y)) >= /\y.X(y) because [26], by (Abs) 26] plus*(X(x), Y(x)) >= X(x) because [27], by (Select) 27] X(x) >= X(x) because [28], by (Meta) 28] x >= x by (Var) 29] d*(/\y.plus(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because d in Mul, [30] and [7], by (Stat) 30] /\y.plus(X(y), Y(y)) > /\y.Y(y) because [31], by definition 31] /\z.plus*(X(z), Y(z)) >= /\z.Y(z) because [32], by (Abs) 32] plus*(X(y), Y(y)) >= Y(y) because [33], by (Select) 33] Y(y) >= Y(y) because [34], by (Meta) 34] y >= y by (Var) 35] 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 [36], by (Star) 36] 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, [37] and [50], by (Copy) 37] d*(/\x.star(X(x), Y(x)), Z) >= star(d(/\x.X(x), Z), Y(Z)) because d > star, [38] and [45], by (Copy) 38] d*(/\x.star(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [39] and [44], by (Stat) 39] /\x.star(X(x), Y(x)) > /\x.X(x) because [40], by definition 40] /\y.star*(X(y), Y(y)) >= /\y.X(y) because [41], by (Abs) 41] star*(X(x), Y(x)) >= X(x) because [42], by (Select) 42] X(x) >= X(x) because [43], by (Meta) 43] x >= x by (Var) 44] Z >= Z by (Meta) 45] d*(/\y.star(X(y), Y(y)), Z) >= Y(Z) because [46], by (Select) 46] star(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= Y(Z) because [47], by (Star) 47] star*(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= Y(Z) because [48], by (Select) 48] Y(d*(/\y.star(X(y), Y(y)), Z)) >= Y(Z) because [49], by (Meta) 49] d*(/\y.star(X(y), Y(y)), Z) >= Z because [44], by (Select) 50] d*(/\y.star(X(y), Y(y)), Z) >= star(X(Z), d(/\y.Y(y), Z)) because d > star, [51] and [55], by (Copy) 51] d*(/\y.star(X(y), Y(y)), Z) >= X(Z) because [52], by (Select) 52] star(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= X(Z) because [53], by (Star) 53] star*(X(d*(/\y.star(X(y), Y(y)), Z)), Y(d*(/\z.star(X(z), Y(z)), Z))) >= X(Z) because [54], by (Select) 54] X(d*(/\y.star(X(y), Y(y)), Z)) >= X(Z) because [49], by (Meta) 55] d*(/\y.star(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because d in Mul, [56] and [44], by (Stat) 56] /\y.star(X(y), Y(y)) > /\y.Y(y) because [57], by definition 57] /\z.star*(X(z), Y(z)) >= /\z.Y(z) because [58], by (Abs) 58] star*(X(y), Y(y)) >= Y(y) because [59], by (Select) 59] Y(y) >= Y(y) because [60], by (Meta) 60] y >= y by (Var) 61] d(/\x.sin(X(x)), Y) >= star(cos(Y), d(/\x.X(x), Y)) because [62], by (Star) 62] d*(/\x.sin(X(x)), Y) >= star(cos(Y), d(/\x.X(x), Y)) because d > star, [63] and [66], by (Copy) 63] d*(/\x.sin(X(x)), Y) >= cos(Y) because d > cos and [64], by (Copy) 64] d*(/\x.sin(X(x)), Y) >= Y because [65], by (Select) 65] Y >= Y by (Meta) 66] d*(/\x.sin(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [67] and [72], by (Stat) 67] /\x.sin(X(x)) > /\x.X(x) because [68], by definition 68] /\y.sin*(X(y)) >= /\y.X(y) because [69], by (Abs) 69] sin*(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] d(/\x.cos(X(x)), Y) >= star(sin(Y), d(/\x.X(x), Y)) because [74], by (Star) 74] d*(/\x.cos(X(x)), Y) >= star(sin(Y), d(/\x.X(x), Y)) because d > star, [75] and [78], by (Copy) 75] d*(/\x.cos(X(x)), Y) >= sin(Y) because d > sin and [76], by (Copy) 76] d*(/\x.cos(X(x)), Y) >= Y because [77], by (Select) 77] Y >= Y by (Meta) 78] d*(/\x.cos(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [79] and [84], by (Stat) 79] /\x.cos(X(x)) > /\x.X(x) because [80], by definition 80] /\y.cos*(X(y)) >= /\y.X(y) because [81], by (Abs) 81] cos*(X(x)) >= X(x) because [82], by (Select) 82] X(x) >= X(x) because [83], by (Meta) 83] x >= x by (Var) 84] Y >= Y by (Meta) 85] _|_ >= _|_ by (Bot) 86] star(_|_, X) >= _|_ by (Bot) 87] star(X, _|_) >= _|_ by (Bot) 88] plus(_|_, X) >= X because [89], by (Star) 89] plus*(_|_, X) >= X because [90], by (Select) 90] X >= X by (Meta) 91] d(F, X) >= d#(F, X) because [92], by (Star) 92] d*(F, X) >= d#(F, X) because d > d#, [93] and [95], by (Copy) 93] d*(F, X) >= F because [94], by (Select) 94] F >= F by (Meta) 95] d*(F, X) >= X because [96], by (Select) 96] 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.plus(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 with usable rules [Kop12, Thm. 7.44]. (P_7, R_0) has no usable rules. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: d#(/\x.plus(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) plus = \y0y1.3 + 3y0 Using this interpretation, the requirements translate to: [[d#(/\x.plus(_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_7, 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.