We consider the system h16. Alphabet: 0 : [] --> R 1 : [] --> R cos : [] --> R -> R d : [] --> (R -> R) -> R -> R minus : [] --> R -> R mul : [] --> R -> R -> R pls : [] --> R -> R -> R sin : [] --> R -> R Rules: d (/\x.y) z => 0 d (/\x.x) y => 1 d (/\x.minus (f x)) y => minus (d (/\z.f z) y) d (/\x.pls (f x) (g x)) y => pls (d (/\z.f z) y) (d (/\u.g u) y) d (/\x.mul (f x) (g x)) y => pls (mul (d (/\z.f z) y) (g y)) (mul (f y) (d (/\u.g u) y)) d (/\x.sin (f x)) y => mul (cos y) (d (/\z.f z) y) d (/\x.cos (f x)) y => mul (minus (sin y)) (d (/\z.f z) y) minus 0 => 0 mul 0 x => 0 mul x 0 => 0 pls 0 x => x Using the transformations described in [Kop11], this system can be brought in a form without leading free variables in the left-hand side, and where the left-hand side of a variable is always a functional term or application headed by a functional term. We now transform the resulting AFS into an AFSM by replacing all free variables by meta-variables (with arity 0). This leads to the following AFSM: Alphabet: 0 : [] --> R 1 : [] --> R cos : [R] --> R d : [R -> R * R] --> R minus : [R] --> R mul : [R * R] --> R pls : [R * R] --> R sin : [R] --> R ~AP1 : [R -> R * R] --> R Rules: d(/\x.X, Y) => 0 d(/\x.x, X) => 1 d(/\x.minus(~AP1(F, x)), X) => minus(d(/\y.~AP1(F, y), X)) d(/\x.pls(~AP1(F, x), ~AP1(G, x)), X) => pls(d(/\y.~AP1(F, y), X), d(/\z.~AP1(G, z), X)) d(/\x.mul(~AP1(F, x), ~AP1(G, x)), X) => pls(mul(d(/\y.~AP1(F, y), X), ~AP1(G, X)), mul(~AP1(F, X), d(/\z.~AP1(G, z), X))) d(/\x.sin(~AP1(F, x)), X) => mul(cos(X), d(/\y.~AP1(F, y), X)) d(/\x.cos(~AP1(F, x)), X) => mul(minus(sin(X)), d(/\y.~AP1(F, y), X)) minus(0) => 0 mul(0, X) => 0 mul(X, 0) => 0 pls(0, X) => X d(/\x.minus(cos(x)), X) => minus(d(/\y.cos(y), X)) d(/\x.minus(d(F, x)), X) => minus(d(/\y.d(F, y), X)) d(/\x.minus(minus(x)), X) => minus(d(/\y.minus(y), X)) d(/\x.minus(mul(X, x)), Y) => minus(d(/\y.mul(X, y), Y)) d(/\x.minus(pls(X, x)), Y) => minus(d(/\y.pls(X, y), Y)) d(/\x.minus(sin(x)), X) => minus(d(/\y.sin(y), X)) d(/\x.pls(cos(x), ~AP1(F, x)), X) => pls(d(/\y.cos(y), X), d(/\z.~AP1(F, z), X)) d(/\x.pls(d(F, x), ~AP1(G, x)), X) => pls(d(/\y.d(F, y), X), d(/\z.~AP1(G, z), X)) d(/\x.pls(minus(x), ~AP1(F, x)), X) => pls(d(/\y.minus(y), X), d(/\z.~AP1(F, z), X)) d(/\x.pls(mul(X, x), ~AP1(F, x)), Y) => pls(d(/\y.mul(X, y), Y), d(/\z.~AP1(F, z), Y)) d(/\x.pls(pls(X, x), ~AP1(F, x)), Y) => pls(d(/\y.pls(X, y), Y), d(/\z.~AP1(F, z), Y)) d(/\x.pls(sin(x), ~AP1(F, x)), X) => pls(d(/\y.sin(y), X), d(/\z.~AP1(F, z), X)) d(/\x.pls(~AP1(F, x), cos(x)), X) => pls(d(/\y.~AP1(F, y), X), d(/\z.cos(z), X)) d(/\x.pls(~AP1(F, x), d(G, x)), X) => pls(d(/\y.~AP1(F, y), X), d(/\z.d(G, z), X)) d(/\x.pls(~AP1(F, x), minus(x)), X) => pls(d(/\y.~AP1(F, y), X), d(/\z.minus(z), X)) d(/\x.pls(~AP1(F, x), mul(X, x)), Y) => pls(d(/\y.~AP1(F, y), Y), d(/\z.mul(X, z), Y)) d(/\x.pls(~AP1(F, x), pls(X, x)), Y) => pls(d(/\y.~AP1(F, y), Y), d(/\z.pls(X, z), Y)) d(/\x.pls(~AP1(F, x), sin(x)), X) => pls(d(/\y.~AP1(F, y), X), d(/\z.sin(z), X)) d(/\x.mul(cos(x), ~AP1(F, x)), X) => pls(mul(d(/\y.cos(y), X), ~AP1(F, X)), mul(cos(X), d(/\z.~AP1(F, z), X))) d(/\x.mul(d(F, x), ~AP1(G, x)), X) => pls(mul(d(/\y.d(F, y), X), ~AP1(G, X)), mul(d(F, X), d(/\z.~AP1(G, z), X))) d(/\x.mul(minus(x), ~AP1(F, x)), X) => pls(mul(d(/\y.minus(y), X), ~AP1(F, X)), mul(minus(X), d(/\z.~AP1(F, z), X))) d(/\x.mul(mul(X, x), ~AP1(F, x)), Y) => pls(mul(d(/\y.mul(X, y), Y), ~AP1(F, Y)), mul(mul(X, Y), d(/\z.~AP1(F, z), Y))) d(/\x.mul(pls(X, x), ~AP1(F, x)), Y) => pls(mul(d(/\y.pls(X, y), Y), ~AP1(F, Y)), mul(pls(X, Y), d(/\z.~AP1(F, z), Y))) d(/\x.mul(sin(x), ~AP1(F, x)), X) => pls(mul(d(/\y.sin(y), X), ~AP1(F, X)), mul(sin(X), d(/\z.~AP1(F, z), X))) d(/\x.mul(~AP1(F, x), cos(x)), X) => pls(mul(d(/\y.~AP1(F, y), X), cos(X)), mul(~AP1(F, X), d(/\z.cos(z), X))) d(/\x.mul(~AP1(F, x), d(G, x)), X) => pls(mul(d(/\y.~AP1(F, y), X), d(G, X)), mul(~AP1(F, X), d(/\z.d(G, z), X))) d(/\x.mul(~AP1(F, x), minus(x)), X) => pls(mul(d(/\y.~AP1(F, y), X), minus(X)), mul(~AP1(F, X), d(/\z.minus(z), X))) d(/\x.mul(~AP1(F, x), mul(X, x)), Y) => pls(mul(d(/\y.~AP1(F, y), Y), mul(X, Y)), mul(~AP1(F, Y), d(/\z.mul(X, z), Y))) d(/\x.mul(~AP1(F, x), pls(X, x)), Y) => pls(mul(d(/\y.~AP1(F, y), Y), pls(X, Y)), mul(~AP1(F, Y), d(/\z.pls(X, z), Y))) d(/\x.mul(~AP1(F, x), sin(x)), X) => pls(mul(d(/\y.~AP1(F, y), X), sin(X)), mul(~AP1(F, X), d(/\z.sin(z), X))) d(/\x.sin(cos(x)), X) => mul(cos(X), d(/\y.cos(y), X)) d(/\x.sin(d(F, x)), X) => mul(cos(X), d(/\y.d(F, y), X)) d(/\x.sin(minus(x)), X) => mul(cos(X), d(/\y.minus(y), X)) d(/\x.sin(mul(X, x)), Y) => mul(cos(Y), d(/\y.mul(X, y), Y)) d(/\x.sin(pls(X, x)), Y) => mul(cos(Y), d(/\y.pls(X, y), Y)) d(/\x.sin(sin(x)), X) => mul(cos(X), d(/\y.sin(y), X)) d(/\x.cos(cos(x)), X) => mul(minus(sin(X)), d(/\y.cos(y), X)) d(/\x.cos(d(F, x)), X) => mul(minus(sin(X)), d(/\y.d(F, y), X)) d(/\x.cos(minus(x)), X) => mul(minus(sin(X)), d(/\y.minus(y), X)) d(/\x.cos(mul(X, x)), Y) => mul(minus(sin(Y)), d(/\y.mul(X, y), Y)) d(/\x.cos(pls(X, x)), Y) => mul(minus(sin(Y)), d(/\y.pls(X, y), Y)) d(/\x.cos(sin(x)), X) => mul(minus(sin(X)), d(/\y.sin(y), X)) d(/\x.pls(cos(x), cos(x)), X) => pls(d(/\y.cos(y), X), d(/\z.cos(z), X)) d(/\x.pls(cos(x), d(F, x)), X) => pls(d(/\y.cos(y), X), d(/\z.d(F, z), X)) d(/\x.pls(cos(x), minus(x)), X) => pls(d(/\y.cos(y), X), d(/\z.minus(z), X)) d(/\x.pls(cos(x), mul(X, x)), Y) => pls(d(/\y.cos(y), Y), d(/\z.mul(X, z), Y)) d(/\x.pls(cos(x), pls(X, x)), Y) => pls(d(/\y.cos(y), Y), d(/\z.pls(X, z), Y)) d(/\x.pls(cos(x), sin(x)), X) => pls(d(/\y.cos(y), X), d(/\z.sin(z), X)) d(/\x.pls(d(F, x), cos(x)), X) => pls(d(/\y.d(F, y), X), d(/\z.cos(z), X)) d(/\x.pls(d(F, x), d(G, x)), X) => pls(d(/\y.d(F, y), X), d(/\z.d(G, z), X)) d(/\x.pls(d(F, x), minus(x)), X) => pls(d(/\y.d(F, y), X), d(/\z.minus(z), X)) d(/\x.pls(d(F, x), mul(X, x)), Y) => pls(d(/\y.d(F, y), Y), d(/\z.mul(X, z), Y)) d(/\x.pls(d(F, x), pls(X, x)), Y) => pls(d(/\y.d(F, y), Y), d(/\z.pls(X, z), Y)) d(/\x.pls(d(F, x), sin(x)), X) => pls(d(/\y.d(F, y), X), d(/\z.sin(z), X)) d(/\x.pls(minus(x), cos(x)), X) => pls(d(/\y.minus(y), X), d(/\z.cos(z), X)) d(/\x.pls(minus(x), d(F, x)), X) => pls(d(/\y.minus(y), X), d(/\z.d(F, z), X)) d(/\x.pls(minus(x), minus(x)), X) => pls(d(/\y.minus(y), X), d(/\z.minus(z), X)) d(/\x.pls(minus(x), mul(X, x)), Y) => pls(d(/\y.minus(y), Y), d(/\z.mul(X, z), Y)) d(/\x.pls(minus(x), pls(X, x)), Y) => pls(d(/\y.minus(y), Y), d(/\z.pls(X, z), Y)) d(/\x.pls(minus(x), sin(x)), X) => pls(d(/\y.minus(y), X), d(/\z.sin(z), X)) d(/\x.pls(mul(X, x), cos(x)), Y) => pls(d(/\y.mul(X, y), Y), d(/\z.cos(z), Y)) d(/\x.pls(mul(X, x), d(F, x)), Y) => pls(d(/\y.mul(X, y), Y), d(/\z.d(F, z), Y)) d(/\x.pls(mul(X, x), minus(x)), Y) => pls(d(/\y.mul(X, y), Y), d(/\z.minus(z), Y)) d(/\x.pls(mul(X, x), mul(Y, x)), Z) => pls(d(/\y.mul(X, y), Z), d(/\z.mul(Y, z), Z)) d(/\x.pls(mul(X, x), pls(Y, x)), Z) => pls(d(/\y.mul(X, y), Z), d(/\z.pls(Y, z), Z)) d(/\x.pls(mul(X, x), sin(x)), Y) => pls(d(/\y.mul(X, y), Y), d(/\z.sin(z), Y)) d(/\x.pls(pls(X, x), cos(x)), Y) => pls(d(/\y.pls(X, y), Y), d(/\z.cos(z), Y)) d(/\x.pls(pls(X, x), d(F, x)), Y) => pls(d(/\y.pls(X, y), Y), d(/\z.d(F, z), Y)) d(/\x.pls(pls(X, x), minus(x)), Y) => pls(d(/\y.pls(X, y), Y), d(/\z.minus(z), Y)) d(/\x.pls(pls(X, x), mul(Y, x)), Z) => pls(d(/\y.pls(X, y), Z), d(/\z.mul(Y, z), Z)) d(/\x.pls(pls(X, x), pls(Y, x)), Z) => pls(d(/\y.pls(X, y), Z), d(/\z.pls(Y, z), Z)) d(/\x.pls(pls(X, x), sin(x)), Y) => pls(d(/\y.pls(X, y), Y), d(/\z.sin(z), Y)) d(/\x.pls(sin(x), cos(x)), X) => pls(d(/\y.sin(y), X), d(/\z.cos(z), X)) d(/\x.pls(sin(x), d(F, x)), X) => pls(d(/\y.sin(y), X), d(/\z.d(F, z), X)) d(/\x.pls(sin(x), minus(x)), X) => pls(d(/\y.sin(y), X), d(/\z.minus(z), X)) d(/\x.pls(sin(x), mul(X, x)), Y) => pls(d(/\y.sin(y), Y), d(/\z.mul(X, z), Y)) d(/\x.pls(sin(x), pls(X, x)), Y) => pls(d(/\y.sin(y), Y), d(/\z.pls(X, z), Y)) d(/\x.pls(sin(x), sin(x)), X) => pls(d(/\y.sin(y), X), d(/\z.sin(z), X)) d(/\x.mul(cos(x), cos(x)), X) => pls(mul(d(/\y.cos(y), X), cos(X)), mul(cos(X), d(/\z.cos(z), X))) d(/\x.mul(cos(x), d(F, x)), X) => pls(mul(d(/\y.cos(y), X), d(F, X)), mul(cos(X), d(/\z.d(F, z), X))) d(/\x.mul(cos(x), minus(x)), X) => pls(mul(d(/\y.cos(y), X), minus(X)), mul(cos(X), d(/\z.minus(z), X))) d(/\x.mul(cos(x), mul(X, x)), Y) => pls(mul(d(/\y.cos(y), Y), mul(X, Y)), mul(cos(Y), d(/\z.mul(X, z), Y))) d(/\x.mul(cos(x), pls(X, x)), Y) => pls(mul(d(/\y.cos(y), Y), pls(X, Y)), mul(cos(Y), d(/\z.pls(X, z), Y))) d(/\x.mul(cos(x), sin(x)), X) => pls(mul(d(/\y.cos(y), X), sin(X)), mul(cos(X), d(/\z.sin(z), X))) d(/\x.mul(d(F, x), cos(x)), X) => pls(mul(d(/\y.d(F, y), X), cos(X)), mul(d(F, X), d(/\z.cos(z), X))) d(/\x.mul(d(F, x), d(G, x)), X) => pls(mul(d(/\y.d(F, y), X), d(G, X)), mul(d(F, X), d(/\z.d(G, z), X))) d(/\x.mul(d(F, x), minus(x)), X) => pls(mul(d(/\y.d(F, y), X), minus(X)), mul(d(F, X), d(/\z.minus(z), X))) d(/\x.mul(d(F, x), mul(X, x)), Y) => pls(mul(d(/\y.d(F, y), Y), mul(X, Y)), mul(d(F, Y), d(/\z.mul(X, z), Y))) d(/\x.mul(d(F, x), pls(X, x)), Y) => pls(mul(d(/\y.d(F, y), Y), pls(X, Y)), mul(d(F, Y), d(/\z.pls(X, z), Y))) d(/\x.mul(d(F, x), sin(x)), X) => pls(mul(d(/\y.d(F, y), X), sin(X)), mul(d(F, X), d(/\z.sin(z), X))) d(/\x.mul(minus(x), cos(x)), X) => pls(mul(d(/\y.minus(y), X), cos(X)), mul(minus(X), d(/\z.cos(z), X))) d(/\x.mul(minus(x), d(F, x)), X) => pls(mul(d(/\y.minus(y), X), d(F, X)), mul(minus(X), d(/\z.d(F, z), X))) d(/\x.mul(minus(x), minus(x)), X) => pls(mul(d(/\y.minus(y), X), minus(X)), mul(minus(X), d(/\z.minus(z), X))) d(/\x.mul(minus(x), mul(X, x)), Y) => pls(mul(d(/\y.minus(y), Y), mul(X, Y)), mul(minus(Y), d(/\z.mul(X, z), Y))) d(/\x.mul(minus(x), pls(X, x)), Y) => pls(mul(d(/\y.minus(y), Y), pls(X, Y)), mul(minus(Y), d(/\z.pls(X, z), Y))) d(/\x.mul(minus(x), sin(x)), X) => pls(mul(d(/\y.minus(y), X), sin(X)), mul(minus(X), d(/\z.sin(z), X))) d(/\x.mul(mul(X, x), cos(x)), Y) => pls(mul(d(/\y.mul(X, y), Y), cos(Y)), mul(mul(X, Y), d(/\z.cos(z), Y))) d(/\x.mul(mul(X, x), d(F, x)), Y) => pls(mul(d(/\y.mul(X, y), Y), d(F, Y)), mul(mul(X, Y), d(/\z.d(F, z), Y))) d(/\x.mul(mul(X, x), minus(x)), Y) => pls(mul(d(/\y.mul(X, y), Y), minus(Y)), mul(mul(X, Y), d(/\z.minus(z), Y))) d(/\x.mul(mul(X, x), mul(Y, x)), Z) => pls(mul(d(/\y.mul(X, y), Z), mul(Y, Z)), mul(mul(X, Z), d(/\z.mul(Y, z), Z))) d(/\x.mul(mul(X, x), pls(Y, x)), Z) => pls(mul(d(/\y.mul(X, y), Z), pls(Y, Z)), mul(mul(X, Z), d(/\z.pls(Y, z), Z))) d(/\x.mul(mul(X, x), sin(x)), Y) => pls(mul(d(/\y.mul(X, y), Y), sin(Y)), mul(mul(X, Y), d(/\z.sin(z), Y))) d(/\x.mul(pls(X, x), cos(x)), Y) => pls(mul(d(/\y.pls(X, y), Y), cos(Y)), mul(pls(X, Y), d(/\z.cos(z), Y))) d(/\x.mul(pls(X, x), d(F, x)), Y) => pls(mul(d(/\y.pls(X, y), Y), d(F, Y)), mul(pls(X, Y), d(/\z.d(F, z), Y))) d(/\x.mul(pls(X, x), minus(x)), Y) => pls(mul(d(/\y.pls(X, y), Y), minus(Y)), mul(pls(X, Y), d(/\z.minus(z), Y))) d(/\x.mul(pls(X, x), mul(Y, x)), Z) => pls(mul(d(/\y.pls(X, y), Z), mul(Y, Z)), mul(pls(X, Z), d(/\z.mul(Y, z), Z))) d(/\x.mul(pls(X, x), pls(Y, x)), Z) => pls(mul(d(/\y.pls(X, y), Z), pls(Y, Z)), mul(pls(X, Z), d(/\z.pls(Y, z), Z))) d(/\x.mul(pls(X, x), sin(x)), Y) => pls(mul(d(/\y.pls(X, y), Y), sin(Y)), mul(pls(X, Y), d(/\z.sin(z), Y))) d(/\x.mul(sin(x), cos(x)), X) => pls(mul(d(/\y.sin(y), X), cos(X)), mul(sin(X), d(/\z.cos(z), X))) d(/\x.mul(sin(x), d(F, x)), X) => pls(mul(d(/\y.sin(y), X), d(F, X)), mul(sin(X), d(/\z.d(F, z), X))) d(/\x.mul(sin(x), minus(x)), X) => pls(mul(d(/\y.sin(y), X), minus(X)), mul(sin(X), d(/\z.minus(z), X))) d(/\x.mul(sin(x), mul(X, x)), Y) => pls(mul(d(/\y.sin(y), Y), mul(X, Y)), mul(sin(Y), d(/\z.mul(X, z), Y))) d(/\x.mul(sin(x), pls(X, x)), Y) => pls(mul(d(/\y.sin(y), Y), pls(X, Y)), mul(sin(Y), d(/\z.pls(X, z), Y))) d(/\x.mul(sin(x), sin(x)), X) => pls(mul(d(/\y.sin(y), X), sin(X)), mul(sin(X), d(/\z.sin(z), X))) ~AP1(F, X) => F X Symbol ~AP1 is an encoding for application that is only used in innocuous ways. We can simplify the program (without losing non-termination) by removing it. Additionally, we can remove some (now-)redundant rules. This gives: Alphabet: 0 : [] --> R 1 : [] --> R cos : [R] --> R d : [R -> R * R] --> R minus : [R] --> R mul : [R * R] --> R pls : [R * R] --> R sin : [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.pls(X(x), Y(x)), Z) => pls(d(/\y.X(y), Z), d(/\z.Y(z), Z)) d(/\x.mul(X(x), Y(x)), Z) => pls(mul(d(/\y.X(y), Z), Y(Z)), mul(X(Z), d(/\z.Y(z), Z))) d(/\x.sin(X(x)), Y) => mul(cos(Y), d(/\y.X(y), Y)) d(/\x.cos(X(x)), Y) => mul(minus(sin(Y)), d(/\y.X(y), Y)) minus(0) => 0 mul(0, X) => 0 mul(X, 0) => 0 pls(0, X) => X We observe that the rules contain a first-order subset: minus(0) => 0 mul(0, X) => 0 mul(X, 0) => 0 pls(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 || mul(0, %X) -> 0 || mul(%X, 0) -> 0 || pls(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(mul(x_1, x_2)) = 2 + 2*x_1 + 2*x_2 || POL(pls(x_1, x_2)) = 2 + x_1 + 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 || mul(0, %X) -> 0 || mul(%X, 0) -> 0 || pls(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.pls(X(x), Y(x)), Z) =#> pls#(d(/\y.X(y), Z), d(/\z.Y(z), Z)) 4] d#(/\x.pls(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) 5] d#(/\x.pls(X(x), Y(x)), Z) =#> X(y) 6] d#(/\x.pls(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z) 7] d#(/\x.pls(X(x), Y(x)), Z) =#> Y(y) 8] d#(/\x.mul(X(x), Y(x)), Z) =#> pls#(mul(d(/\y.X(y), Z), Y(Z)), mul(X(Z), d(/\z.Y(z), Z))) 9] d#(/\x.mul(X(x), Y(x)), Z) =#> mul#(d(/\y.X(y), Z), Y(Z)) 10] d#(/\x.mul(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) 11] d#(/\x.mul(X(x), Y(x)), Z) =#> X(y) 12] d#(/\x.mul(X(x), Y(x)), Z) =#> Y(Z) 13] d#(/\x.mul(X(x), Y(x)), Z) =#> mul#(X(Z), d(/\y.Y(y), Z)) 14] d#(/\x.mul(X(x), Y(x)), Z) =#> X(Z) 15] d#(/\x.mul(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z) 16] d#(/\x.mul(X(x), Y(x)), Z) =#> Y(y) 17] d#(/\x.sin(X(x)), Y) =#> mul#(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) =#> mul#(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.pls(X(x), Y(x)), Z) => pls(d(/\y.X(y), Z), d(/\z.Y(z), Z)) d(/\x.mul(X(x), Y(x)), Z) => pls(mul(d(/\y.X(y), Z), Y(Z)), mul(X(Z), d(/\z.Y(z), Z))) d(/\x.sin(X(x)), Y) => mul(cos(Y), d(/\y.X(y), Y)) d(/\x.cos(X(x)), Y) => mul(minus(sin(Y)), d(/\y.X(y), Y)) minus(0) => 0 mul(0, X) => 0 mul(X, 0) => 0 pls(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.pls(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) d#(/\x.pls(X(x), Y(x)), Z) =#> X(y) d#(/\x.pls(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z) d#(/\x.pls(X(x), Y(x)), Z) =#> Y(y) d#(/\x.mul(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) d#(/\x.mul(X(x), Y(x)), Z) =#> X(y) d#(/\x.mul(X(x), Y(x)), Z) =#> Y(Z) d#(/\x.mul(X(x), Y(x)), Z) =#> X(Z) d#(/\x.mul(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z) d#(/\x.mul(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.pls(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) d#(/\x.pls(X(x), Y(x)), Z) >? X(~c1) d#(/\x.pls(X(x), Y(x)), Z) >? d#(/\y.Y(y), Z) d#(/\x.pls(X(x), Y(x)), Z) >? Y(~c2) d#(/\x.mul(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) d#(/\x.mul(X(x), Y(x)), Z) >? X(~c3) d#(/\x.mul(X(x), Y(x)), Z) >? Y(Z) d#(/\x.mul(X(x), Y(x)), Z) >? X(Z) d#(/\x.mul(X(x), Y(x)), Z) >? d#(/\y.Y(y), Z) d#(/\x.mul(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.pls(X(x), Y(x)), Z) >= pls(d(/\y.X(y), Z), d(/\z.Y(z), Z)) d(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\y.X(y), Z), Y(Z)), mul(X(Z), d(/\z.Y(z), Z))) d(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\y.X(y), Y)) d(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\y.X(y), Y)) minus(0) >= 0 mul(0, X) >= 0 mul(X, 0) >= 0 pls(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]] = _|_ [[~c5]] = _|_ [[~c6]] = _|_ We choose Lex = {d#} and Mul = {cos, d, mul, pls, sin}, and the following precedence: cos = d > d# > mul > pls > sin Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: d#(/\x.X(x), Y) >= d#(/\x.X(x), Y) d#(/\x.X(x), Y) >= X(_|_) d#(/\x.pls(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) d#(/\x.pls(X(x), Y(x)), Z) > X(_|_) d#(/\x.pls(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) d#(/\x.pls(X(x), Y(x)), Z) >= Y(_|_) d#(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) d#(/\x.mul(X(x), Y(x)), Z) >= X(_|_) d#(/\x.mul(X(x), Y(x)), Z) >= Y(Z) d#(/\x.mul(X(x), Y(x)), Z) >= X(Z) d#(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) d#(/\x.mul(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.pls(X(x), Y(x)), Z) >= pls(d(/\x.X(x), Z), d(/\y.Y(y), Z)) d(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\x.X(x), Z), Y(Z)), mul(X(Z), d(/\y.Y(y), Z))) d(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\x.X(x), Y)) d(/\x.cos(X(x)), Y) >= mul(sin(Y), d(/\x.X(x), Y)) _|_ >= _|_ mul(_|_, X) >= _|_ mul(X, _|_) >= _|_ pls(_|_, 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 [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.pls(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because [11] and [16], by (Fun) 11] /\y.pls(X(y), Y(y)) >= /\y.X(y) because [12], by (Abs) 12] pls(X(x), Y(x)) >= X(x) because [13], by (Star) 13] pls*(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.pls(X(x), Y(x)), Z) > X(_|_) because [18], by definition 18] d#*(/\x.pls(X(x), Y(x)), Z) >= X(_|_) because [19], by (Select) 19] pls(X(d#*(/\x.pls(X(x), Y(x)), Z)), Y(d#*(/\y.pls(X(y), Y(y)), Z))) >= X(_|_) because [20], by (Star) 20] pls*(X(d#*(/\x.pls(X(x), Y(x)), Z)), Y(d#*(/\y.pls(X(y), Y(y)), Z))) >= X(_|_) because [21], by (Select) 21] X(d#*(/\x.pls(X(x), Y(x)), Z)) >= X(_|_) because [22], by (Meta) 22] d#*(/\x.pls(X(x), Y(x)), Z) >= _|_ by (Bot) 23] d#(/\x.pls(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) because [24] and [16], by (Fun) 24] /\y.pls(X(y), Y(y)) >= /\y.Y(y) because [25], by (Abs) 25] pls(X(x), Y(x)) >= Y(x) because [26], by (Star) 26] pls*(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.pls(X(x), Y(x)), Z) >= Y(_|_) because [30], by (Star) 30] d#*(/\x.pls(X(x), Y(x)), Z) >= Y(_|_) because [31], by (Select) 31] pls(X(d#*(/\x.pls(X(x), Y(x)), Z)), Y(d#*(/\y.pls(X(y), Y(y)), Z))) >= Y(_|_) because [32], by (Star) 32] pls*(X(d#*(/\x.pls(X(x), Y(x)), Z)), Y(d#*(/\y.pls(X(y), Y(y)), Z))) >= Y(_|_) because [33], by (Select) 33] Y(d#*(/\x.pls(X(x), Y(x)), Z)) >= Y(_|_) because [34], by (Meta) 34] d#*(/\x.pls(X(x), Y(x)), Z) >= _|_ by (Bot) 35] d#(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because [36] and [41], by (Fun) 36] /\y.mul(X(y), Y(y)) >= /\y.X(y) because [37], by (Abs) 37] mul(X(x), Y(x)) >= X(x) because [38], by (Star) 38] mul*(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.mul(X(x), Y(x)), Z) >= X(_|_) because [43], by (Star) 43] d#*(/\x.mul(X(x), Y(x)), Z) >= X(_|_) because [44], by (Select) 44] mul(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= X(_|_) because [45], by (Star) 45] mul*(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= X(_|_) because [46], by (Select) 46] X(d#*(/\x.mul(X(x), Y(x)), Z)) >= X(_|_) because [47], by (Meta) 47] d#*(/\x.mul(X(x), Y(x)), Z) >= _|_ by (Bot) 48] d#(/\x.mul(X(x), Y(x)), Z) >= Y(Z) because [49], by (Star) 49] d#*(/\x.mul(X(x), Y(x)), Z) >= Y(Z) because [50], by (Select) 50] mul(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= Y(Z) because [51], by (Star) 51] mul*(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= Y(Z) because [52], by (Select) 52] Y(d#*(/\x.mul(X(x), Y(x)), Z)) >= Y(Z) because [53], by (Meta) 53] d#*(/\x.mul(X(x), Y(x)), Z) >= Z because [41], by (Select) 54] d#(/\x.mul(X(x), Y(x)), Z) >= X(Z) because [55], by (Star) 55] d#*(/\x.mul(X(x), Y(x)), Z) >= X(Z) because [56], by (Select) 56] mul(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= X(Z) because [57], by (Star) 57] mul*(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= X(Z) because [58], by (Select) 58] X(d#*(/\x.mul(X(x), Y(x)), Z)) >= X(Z) because [53], by (Meta) 59] d#(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) because [60] and [41], by (Fun) 60] /\y.mul(X(y), Y(y)) >= /\y.Y(y) because [61], by (Abs) 61] mul(X(x), Y(x)) >= Y(x) because [62], by (Star) 62] mul*(X(x), Y(x)) >= Y(x) because [63], by (Select) 63] Y(x) >= Y(x) because [64], by (Meta) 64] x >= x by (Var) 65] d#(/\x.mul(X(x), Y(x)), Z) >= Y(_|_) because [66], by (Star) 66] d#*(/\x.mul(X(x), Y(x)), Z) >= Y(_|_) because [67], by (Select) 67] mul(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= Y(_|_) because [68], by (Star) 68] mul*(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= Y(_|_) because [69], by (Select) 69] Y(d#*(/\x.mul(X(x), Y(x)), Z)) >= Y(_|_) because [70], by (Meta) 70] d#*(/\x.mul(X(x), Y(x)), Z) >= _|_ by (Bot) 71] d#(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y) because [72] and [77], by (Fun) 72] /\y.sin(X(y)) >= /\y.X(y) because [73], by (Abs) 73] sin(X(x)) >= X(x) because [74], by (Star) 74] sin*(X(x)) >= X(x) because [75], by (Select) 75] X(x) >= X(x) because [76], by (Meta) 76] x >= x by (Var) 77] Y >= Y by (Meta) 78] d#(/\x.sin(X(x)), Y) >= X(_|_) because [79], by (Star) 79] d#*(/\x.sin(X(x)), Y) >= X(_|_) because [80], by (Select) 80] sin(X(d#*(/\x.sin(X(x)), Y))) >= X(_|_) because [81], by (Star) 81] sin*(X(d#*(/\x.sin(X(x)), Y))) >= X(_|_) because [82], by (Select) 82] X(d#*(/\x.sin(X(x)), Y)) >= X(_|_) because [83], by (Meta) 83] d#*(/\x.sin(X(x)), Y) >= _|_ by (Bot) 84] d#(/\x.cos(X(x)), Y) > d#(/\x.X(x), Y) because [85], by definition 85] d#*(/\x.cos(X(x)), Y) >= d#(/\x.X(x), Y) because [86], [91] and [98], 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] d#*(/\y.cos(X(y)), Y) >= /\y.X(y) because [92], by (F-Abs) 92] d#*(/\y.cos(X(y)), Y, z) >= X(z) because [93], by (Select) 93] cos(X(d#*(/\y.cos(X(y)), Y, z))) >= X(z) because [94], by (Star) 94] cos*(X(d#*(/\y.cos(X(y)), Y, z))) >= X(z) because [95], by (Select) 95] X(d#*(/\y.cos(X(y)), Y, z)) >= X(z) because [96], by (Meta) 96] d#*(/\y.cos(X(y)), Y, z) >= z because [97], by (Select) 97] z >= z by (Var) 98] d#*(/\y.cos(X(y)), Y) >= Y because [99], by (Select) 99] Y >= Y by (Meta) 100] d#(/\x.cos(X(x)), Y) > X(_|_) because [101], by definition 101] d#*(/\x.cos(X(x)), Y) >= X(_|_) because [102], by (Select) 102] cos(X(d#*(/\x.cos(X(x)), Y))) >= X(_|_) because [103], by (Star) 103] cos*(X(d#*(/\x.cos(X(x)), Y))) >= X(_|_) because [104], by (Select) 104] X(d#*(/\x.cos(X(x)), Y)) >= X(_|_) because [105], by (Meta) 105] d#*(/\x.cos(X(x)), Y) >= _|_ by (Bot) 106] d(/\x.X, Y) >= _|_ by (Bot) 107] d(/\x.x, X) >= _|_ by (Bot) 108] d(/\x.X(x), Y) >= d(/\x.X(x), Y) because d in Mul, [2] and [5], by (Fun) 109] d(/\x.pls(X(x), Y(x)), Z) >= pls(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because [110], by (Star) 110] d*(/\x.pls(X(x), Y(x)), Z) >= pls(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because d > pls, [111] and [117], by (Copy) 111] d*(/\x.pls(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [112] and [16], by (Stat) 112] /\x.pls(X(x), Y(x)) > /\x.X(x) because [113], by definition 113] /\y.pls*(X(y), Y(y)) >= /\y.X(y) because [114], by (Abs) 114] pls*(X(x), Y(x)) >= X(x) because [115], by (Select) 115] X(x) >= X(x) because [116], by (Meta) 116] x >= x by (Var) 117] d*(/\y.pls(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because d in Mul, [118] and [16], by (Stat) 118] /\y.pls(X(y), Y(y)) > /\y.Y(y) because [119], by definition 119] /\z.pls*(X(z), Y(z)) >= /\z.Y(z) because [120], by (Abs) 120] pls*(X(y), Y(y)) >= Y(y) because [121], by (Select) 121] Y(y) >= Y(y) because [122], by (Meta) 122] y >= y by (Var) 123] d(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\x.X(x), Z), Y(Z)), mul(X(Z), d(/\y.Y(y), Z))) because [124], by (Star) 124] d*(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\x.X(x), Z), Y(Z)), mul(X(Z), d(/\y.Y(y), Z))) because d > pls, [125] and [137], by (Copy) 125] d*(/\x.mul(X(x), Y(x)), Z) >= mul(d(/\x.X(x), Z), Y(Z)) because d > mul, [126] and [132], by (Copy) 126] d*(/\x.mul(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [127] and [41], by (Stat) 127] /\x.mul(X(x), Y(x)) > /\x.X(x) because [128], by definition 128] /\y.mul*(X(y), Y(y)) >= /\y.X(y) because [129], by (Abs) 129] mul*(X(x), Y(x)) >= X(x) because [130], by (Select) 130] X(x) >= X(x) because [131], by (Meta) 131] x >= x by (Var) 132] d*(/\y.mul(X(y), Y(y)), Z) >= Y(Z) because [133], by (Select) 133] mul(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [134], by (Star) 134] mul*(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [135], by (Select) 135] Y(d*(/\y.mul(X(y), Y(y)), Z)) >= Y(Z) because [136], by (Meta) 136] d*(/\y.mul(X(y), Y(y)), Z) >= Z because [41], by (Select) 137] d*(/\y.mul(X(y), Y(y)), Z) >= mul(X(Z), d(/\y.Y(y), Z)) because d > mul, [138] and [142], by (Copy) 138] d*(/\y.mul(X(y), Y(y)), Z) >= X(Z) because [139], by (Select) 139] mul(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [140], by (Star) 140] mul*(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [141], by (Select) 141] X(d*(/\y.mul(X(y), Y(y)), Z)) >= X(Z) because [136], by (Meta) 142] d*(/\y.mul(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because d in Mul, [143] and [41], by (Stat) 143] /\y.mul(X(y), Y(y)) > /\y.Y(y) because [144], by definition 144] /\z.mul*(X(z), Y(z)) >= /\z.Y(z) because [145], by (Abs) 145] mul*(X(y), Y(y)) >= Y(y) because [146], by (Select) 146] Y(y) >= Y(y) because [147], by (Meta) 147] y >= y by (Var) 148] d(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\x.X(x), Y)) because [149], by (Star) 149] d*(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\x.X(x), Y)) because d > mul, [150] and [151], by (Copy) 150] d*(/\x.sin(X(x)), Y) >= cos(Y) because d = cos, d in Mul and [77], by (Stat) 151] d*(/\x.sin(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [152] and [77], by (Stat) 152] /\x.sin(X(x)) > /\x.X(x) because [153], by definition 153] /\y.sin*(X(y)) >= /\y.X(y) because [154], by (Abs) 154] sin*(X(x)) >= X(x) because [155], by (Select) 155] X(x) >= X(x) because [156], by (Meta) 156] x >= x by (Var) 157] d(/\x.cos(X(x)), Y) >= mul(sin(Y), d(/\x.X(x), Y)) because [158], by (Star) 158] d*(/\x.cos(X(x)), Y) >= mul(sin(Y), d(/\x.X(x), Y)) because d > mul, [159] and [161], 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 [99], by (Select) 161] d*(/\x.cos(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [86] and [162], by (Stat) 162] Y >= Y by (Meta) 163] _|_ >= _|_ by (Bot) 164] mul(_|_, X) >= _|_ by (Bot) 165] mul(X, _|_) >= _|_ by (Bot) 166] pls(_|_, X) >= X because [167], by (Star) 167] pls*(_|_, X) >= X because [168], by (Select) 168] X >= X by (Meta) 169] d(F, X) >= d#(F, X) because [170], by (Star) 170] d*(F, X) >= d#(F, X) because d > d#, [171] and [173], by (Copy) 171] d*(F, X) >= F because [172], by (Select) 172] F >= F by (Meta) 173] d*(F, X) >= X because [174], by (Select) 174] 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.pls(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) d#(/\x.pls(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z) d#(/\x.pls(X(x), Y(x)), Z) =#> Y(y) d#(/\x.mul(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) d#(/\x.mul(X(x), Y(x)), Z) =#> X(y) d#(/\x.mul(X(x), Y(x)), Z) =#> Y(Z) d#(/\x.mul(X(x), Y(x)), Z) =#> X(Z) d#(/\x.mul(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z) d#(/\x.mul(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) 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.pls(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) d#(/\x.pls(X(x), Y(x)), Z) >? d#(/\y.Y(y), Z) d#(/\x.pls(X(x), Y(x)), Z) >? Y(~c1) d#(/\x.mul(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) d#(/\x.mul(X(x), Y(x)), Z) >? X(~c2) d#(/\x.mul(X(x), Y(x)), Z) >? Y(Z) d#(/\x.mul(X(x), Y(x)), Z) >? X(Z) d#(/\x.mul(X(x), Y(x)), Z) >? d#(/\y.Y(y), Z) d#(/\x.mul(X(x), Y(x)), Z) >? Y(~c3) d#(/\x.sin(X(x)), Y) >? d#(/\y.X(y), Y) d#(/\x.sin(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.pls(X(x), Y(x)), Z) >= pls(d(/\y.X(y), Z), d(/\z.Y(z), Z)) d(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\y.X(y), Z), Y(Z)), mul(X(Z), d(/\z.Y(z), Z))) d(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\y.X(y), Y)) d(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\y.X(y), Y)) minus(0) >= 0 mul(0, X) >= 0 mul(X, 0) >= 0 pls(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]] = _|_ We choose Lex = {} and Mul = {cos, d, d#, minus, mul, pls, sin}, and the following precedence: d > d# > minus > cos > sin > mul > pls 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.pls(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) d#(/\x.pls(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) d#(/\x.pls(X(x), Y(x)), Z) >= Y(_|_) d#(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) d#(/\x.mul(X(x), Y(x)), Z) >= X(_|_) d#(/\x.mul(X(x), Y(x)), Z) > Y(Z) d#(/\x.mul(X(x), Y(x)), Z) > X(Z) d#(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) d#(/\x.mul(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.X, Y) >= _|_ d(/\x.x, X) >= _|_ d(/\x.minus(X(x)), Y) >= minus(d(/\x.X(x), Y)) d(/\x.pls(X(x), Y(x)), Z) >= pls(d(/\x.X(x), Z), d(/\y.Y(y), Z)) d(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\x.X(x), Z), Y(Z)), mul(X(Z), d(/\y.Y(y), Z))) d(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\x.X(x), Y)) d(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\x.X(x), Y)) minus(_|_) >= _|_ mul(_|_, X) >= _|_ mul(X, _|_) >= _|_ pls(_|_, 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.pls(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because d# in Mul, [15] and [20], by (Fun) 15] /\y.pls(X(y), Y(y)) >= /\y.X(y) because [16], by (Abs) 16] pls(X(x), Y(x)) >= X(x) because [17], by (Star) 17] pls*(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.pls(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) because d# in Mul, [22] and [20], by (Fun) 22] /\y.pls(X(y), Y(y)) >= /\y.Y(y) because [23], by (Abs) 23] pls(X(x), Y(x)) >= Y(x) because [24], by (Star) 24] pls*(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.pls(X(x), Y(x)), Z) >= Y(_|_) because [28], by (Star) 28] d#*(/\x.pls(X(x), Y(x)), Z) >= Y(_|_) because [29], by (Select) 29] pls(X(d#*(/\x.pls(X(x), Y(x)), Z)), Y(d#*(/\y.pls(X(y), Y(y)), Z))) >= Y(_|_) because [30], by (Star) 30] pls*(X(d#*(/\x.pls(X(x), Y(x)), Z)), Y(d#*(/\y.pls(X(y), Y(y)), Z))) >= Y(_|_) because [31], by (Select) 31] Y(d#*(/\x.pls(X(x), Y(x)), Z)) >= Y(_|_) because [32], by (Meta) 32] d#*(/\x.pls(X(x), Y(x)), Z) >= _|_ by (Bot) 33] d#(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because d# in Mul, [34] and [39], by (Fun) 34] /\y.mul(X(y), Y(y)) >= /\y.X(y) because [35], by (Abs) 35] mul(X(x), Y(x)) >= X(x) because [36], by (Star) 36] mul*(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.mul(X(x), Y(x)), Z) >= X(_|_) because [41], by (Star) 41] d#*(/\x.mul(X(x), Y(x)), Z) >= X(_|_) because [42], by (Select) 42] mul(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= X(_|_) because [43], by (Star) 43] mul*(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= X(_|_) because [44], by (Select) 44] X(d#*(/\x.mul(X(x), Y(x)), Z)) >= X(_|_) because [45], by (Meta) 45] d#*(/\x.mul(X(x), Y(x)), Z) >= _|_ by (Bot) 46] d#(/\x.mul(X(x), Y(x)), Z) > Y(Z) because [47], by definition 47] d#*(/\x.mul(X(x), Y(x)), Z) >= Y(Z) because [48], by (Select) 48] mul(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= Y(Z) because [49], by (Star) 49] mul*(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= Y(Z) because [50], by (Select) 50] Y(d#*(/\x.mul(X(x), Y(x)), Z)) >= Y(Z) because [51], by (Meta) 51] d#*(/\x.mul(X(x), Y(x)), Z) >= Z because [39], by (Select) 52] d#(/\x.mul(X(x), Y(x)), Z) > X(Z) because [53], by definition 53] d#*(/\x.mul(X(x), Y(x)), Z) >= X(Z) because [54], by (Select) 54] mul(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= X(Z) because [55], by (Star) 55] mul*(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= X(Z) because [56], by (Select) 56] X(d#*(/\x.mul(X(x), Y(x)), Z)) >= X(Z) because [51], by (Meta) 57] d#(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) because d# in Mul, [58] and [39], by (Fun) 58] /\y.mul(X(y), Y(y)) >= /\y.Y(y) because [59], by (Abs) 59] mul(X(x), Y(x)) >= Y(x) because [60], by (Star) 60] mul*(X(x), Y(x)) >= Y(x) because [61], by (Select) 61] Y(x) >= Y(x) because [62], by (Meta) 62] x >= x by (Var) 63] d#(/\x.mul(X(x), Y(x)), Z) > Y(_|_) because [64], by definition 64] d#*(/\x.mul(X(x), Y(x)), Z) >= Y(_|_) because [65], by (Select) 65] mul(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= Y(_|_) because [66], by (Star) 66] mul*(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= Y(_|_) because [67], by (Select) 67] Y(d#*(/\x.mul(X(x), Y(x)), Z)) >= Y(_|_) because [68], by (Meta) 68] d#*(/\x.mul(X(x), Y(x)), Z) >= _|_ by (Bot) 69] d#(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y) because d# in Mul, [70] and [75], by (Fun) 70] /\y.sin(X(y)) >= /\y.X(y) because [71], by (Abs) 71] sin(X(x)) >= X(x) because [72], by (Star) 72] sin*(X(x)) >= X(x) because [73], by (Select) 73] X(x) >= X(x) because [74], by (Meta) 74] x >= x by (Var) 75] Y >= Y by (Meta) 76] d#(/\x.sin(X(x)), Y) >= X(_|_) because [77], by (Star) 77] d#*(/\x.sin(X(x)), Y) >= X(_|_) because [78], by (Select) 78] sin(X(d#*(/\x.sin(X(x)), Y))) >= X(_|_) because [79], by (Star) 79] sin*(X(d#*(/\x.sin(X(x)), Y))) >= X(_|_) because [80], by (Select) 80] X(d#*(/\x.sin(X(x)), Y)) >= X(_|_) because [81], by (Meta) 81] d#*(/\x.sin(X(x)), Y) >= _|_ by (Bot) 82] d(/\x.X, Y) >= _|_ by (Bot) 83] d(/\x.x, X) >= _|_ by (Bot) 84] d(/\x.minus(X(x)), Y) >= minus(d(/\x.X(x), Y)) because [85], by (Star) 85] d*(/\x.minus(X(x)), Y) >= minus(d(/\x.X(x), Y)) because d > minus and [86], by (Copy) 86] d*(/\x.minus(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [87] and [7], by (Stat) 87] /\x.minus(X(x)) > /\x.X(x) because [88], by definition 88] /\y.minus*(X(y)) >= /\y.X(y) because [89], by (Abs) 89] minus*(X(x)) >= X(x) because [90], by (Select) 90] X(x) >= X(x) because [91], by (Meta) 91] x >= x by (Var) 92] d(/\x.pls(X(x), Y(x)), Z) >= pls(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because [93], by (Star) 93] d*(/\x.pls(X(x), Y(x)), Z) >= pls(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because d > pls, [94] and [100], by (Copy) 94] d*(/\x.pls(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [95] and [20], by (Stat) 95] /\x.pls(X(x), Y(x)) > /\x.X(x) because [96], by definition 96] /\y.pls*(X(y), Y(y)) >= /\y.X(y) because [97], by (Abs) 97] pls*(X(x), Y(x)) >= X(x) because [98], by (Select) 98] X(x) >= X(x) because [99], by (Meta) 99] x >= x by (Var) 100] d*(/\y.pls(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because d in Mul, [101] and [20], by (Stat) 101] /\y.pls(X(y), Y(y)) > /\y.Y(y) because [102], by definition 102] /\z.pls*(X(z), Y(z)) >= /\z.Y(z) because [103], by (Abs) 103] pls*(X(y), Y(y)) >= Y(y) because [104], by (Select) 104] Y(y) >= Y(y) because [105], by (Meta) 105] y >= y by (Var) 106] d(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\x.X(x), Z), Y(Z)), mul(X(Z), d(/\y.Y(y), Z))) because [107], by (Star) 107] d*(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\x.X(x), Z), Y(Z)), mul(X(Z), d(/\y.Y(y), Z))) because d > pls, [108] and [120], by (Copy) 108] d*(/\x.mul(X(x), Y(x)), Z) >= mul(d(/\x.X(x), Z), Y(Z)) because d > mul, [109] and [115], by (Copy) 109] d*(/\x.mul(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [110] and [39], by (Stat) 110] /\x.mul(X(x), Y(x)) > /\x.X(x) because [111], by definition 111] /\y.mul*(X(y), Y(y)) >= /\y.X(y) because [112], by (Abs) 112] mul*(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.mul(X(y), Y(y)), Z) >= Y(Z) because [116], by (Select) 116] mul(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [117], by (Star) 117] mul*(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [118], by (Select) 118] Y(d*(/\y.mul(X(y), Y(y)), Z)) >= Y(Z) because [119], by (Meta) 119] d*(/\y.mul(X(y), Y(y)), Z) >= Z because [39], by (Select) 120] d*(/\y.mul(X(y), Y(y)), Z) >= mul(X(Z), d(/\y.Y(y), Z)) because d > mul, [121] and [125], by (Copy) 121] d*(/\y.mul(X(y), Y(y)), Z) >= X(Z) because [122], by (Select) 122] mul(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [123], by (Star) 123] mul*(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [124], by (Select) 124] X(d*(/\y.mul(X(y), Y(y)), Z)) >= X(Z) because [119], by (Meta) 125] d*(/\y.mul(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because d in Mul, [126] and [39], by (Stat) 126] /\y.mul(X(y), Y(y)) > /\y.Y(y) because [127], by definition 127] /\z.mul*(X(z), Y(z)) >= /\z.Y(z) because [128], by (Abs) 128] mul*(X(y), Y(y)) >= Y(y) because [129], by (Select) 129] Y(y) >= Y(y) because [130], by (Meta) 130] y >= y by (Var) 131] d(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\x.X(x), Y)) because [132], by (Star) 132] d*(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\x.X(x), Y)) because d > mul, [133] and [135], by (Copy) 133] d*(/\x.sin(X(x)), Y) >= cos(Y) because d > cos and [134], by (Copy) 134] d*(/\x.sin(X(x)), Y) >= Y because [75], by (Select) 135] d*(/\x.sin(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [136] and [75], by (Stat) 136] /\x.sin(X(x)) > /\x.X(x) because [137], by definition 137] /\y.sin*(X(y)) >= /\y.X(y) because [138], by (Abs) 138] sin*(X(x)) >= X(x) because [139], by (Select) 139] X(x) >= X(x) because [140], by (Meta) 140] x >= x by (Var) 141] d(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\x.X(x), Y)) because [142], by (Star) 142] d*(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\x.X(x), Y)) because d > mul, [143] and [147], by (Copy) 143] d*(/\x.cos(X(x)), Y) >= minus(sin(Y)) because d > minus and [144], by (Copy) 144] d*(/\x.cos(X(x)), Y) >= sin(Y) because d > sin and [145], by (Copy) 145] d*(/\x.cos(X(x)), Y) >= Y because [146], by (Select) 146] Y >= Y by (Meta) 147] d*(/\x.cos(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [148] and [153], by (Stat) 148] /\x.cos(X(x)) > /\x.X(x) because [149], by definition 149] /\y.cos*(X(y)) >= /\y.X(y) because [150], by (Abs) 150] cos*(X(x)) >= X(x) because [151], by (Select) 151] X(x) >= X(x) because [152], by (Meta) 152] x >= x by (Var) 153] Y >= Y by (Meta) 154] minus(_|_) >= _|_ by (Bot) 155] mul(_|_, X) >= _|_ by (Bot) 156] mul(X, _|_) >= _|_ by (Bot) 157] pls(_|_, X) >= X because [158], by (Star) 158] pls*(_|_, X) >= X because [159], by (Select) 159] X >= X by (Meta) 160] d(F, X) >= d#(F, X) because [161], by (Star) 161] d*(F, X) >= d#(F, X) because d > d#, [162] and [164], by (Copy) 162] d*(F, X) >= F because [163], by (Select) 163] F >= F by (Meta) 164] d*(F, X) >= X because [165], by (Select) 165] 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.pls(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) d#(/\x.pls(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z) d#(/\x.pls(X(x), Y(x)), Z) =#> Y(y) d#(/\x.mul(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) d#(/\x.mul(X(x), Y(x)), Z) =#> X(y) d#(/\x.mul(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z) d#(/\x.sin(X(x)), Y) =#> d#(/\y.X(y), Y) d#(/\x.sin(X(x)), Y) =#> X(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.pls(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) d#(/\x.pls(X(x), Y(x)), Z) >? d#(/\y.Y(y), Z) d#(/\x.pls(X(x), Y(x)), Z) >? Y(~c1) d#(/\x.mul(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) d#(/\x.mul(X(x), Y(x)), Z) >? X(~c2) d#(/\x.mul(X(x), Y(x)), Z) >? d#(/\y.Y(y), Z) d#(/\x.sin(X(x)), Y) >? d#(/\y.X(y), Y) d#(/\x.sin(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.pls(X(x), Y(x)), Z) >= pls(d(/\y.X(y), Z), d(/\z.Y(z), Z)) d(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\y.X(y), Z), Y(Z)), mul(X(Z), d(/\z.Y(z), Z))) d(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\y.X(y), Y)) d(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\y.X(y), Y)) minus(0) >= 0 mul(0, X) >= 0 mul(X, 0) >= 0 pls(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]] = _|_ We choose Lex = {} and Mul = {cos, d, d#, minus, mul, pls, sin}, and the following precedence: d > cos > d# > minus > mul > pls > 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.pls(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) d#(/\x.pls(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) d#(/\x.pls(X(x), Y(x)), Z) > Y(_|_) d#(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) d#(/\x.mul(X(x), Y(x)), Z) >= X(_|_) d#(/\x.mul(X(x), Y(x)), Z) > d#(/\x.Y(x), Z) d#(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y) d#(/\x.sin(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.pls(X(x), Y(x)), Z) >= pls(d(/\x.X(x), Z), d(/\y.Y(y), Z)) d(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\x.X(x), Z), Y(Z)), mul(X(Z), d(/\y.Y(y), Z))) d(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\x.X(x), Y)) d(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\x.X(x), Y)) minus(_|_) >= _|_ mul(_|_, X) >= _|_ mul(X, _|_) >= _|_ pls(_|_, 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 definition 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.pls(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because d# in Mul, [15] and [20], by (Fun) 15] /\y.pls(X(y), Y(y)) >= /\y.X(y) because [16], by (Abs) 16] pls(X(x), Y(x)) >= X(x) because [17], by (Star) 17] pls*(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.pls(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) because d# in Mul, [22] and [20], by (Fun) 22] /\y.pls(X(y), Y(y)) >= /\y.Y(y) because [23], by (Abs) 23] pls(X(x), Y(x)) >= Y(x) because [24], by (Star) 24] pls*(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.pls(X(x), Y(x)), Z) > Y(_|_) because [28], by definition 28] d#*(/\x.pls(X(x), Y(x)), Z) >= Y(_|_) because [29], by (Select) 29] pls(X(d#*(/\x.pls(X(x), Y(x)), Z)), Y(d#*(/\y.pls(X(y), Y(y)), Z))) >= Y(_|_) because [30], by (Star) 30] pls*(X(d#*(/\x.pls(X(x), Y(x)), Z)), Y(d#*(/\y.pls(X(y), Y(y)), Z))) >= Y(_|_) because [31], by (Select) 31] Y(d#*(/\x.pls(X(x), Y(x)), Z)) >= Y(_|_) because [32], by (Meta) 32] d#*(/\x.pls(X(x), Y(x)), Z) >= _|_ by (Bot) 33] d#(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because d# in Mul, [34] and [39], by (Fun) 34] /\y.mul(X(y), Y(y)) >= /\y.X(y) because [35], by (Abs) 35] mul(X(x), Y(x)) >= X(x) because [36], by (Star) 36] mul*(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.mul(X(x), Y(x)), Z) >= X(_|_) because [41], by (Star) 41] d#*(/\x.mul(X(x), Y(x)), Z) >= X(_|_) because [42], by (Select) 42] mul(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= X(_|_) because [43], by (Star) 43] mul*(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= X(_|_) because [44], by (Select) 44] X(d#*(/\x.mul(X(x), Y(x)), Z)) >= X(_|_) because [45], by (Meta) 45] d#*(/\x.mul(X(x), Y(x)), Z) >= _|_ by (Bot) 46] d#(/\x.mul(X(x), Y(x)), Z) > d#(/\x.Y(x), Z) because [47], by definition 47] d#*(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) because d# in Mul, [48] and [39], by (Stat) 48] /\x.mul(X(x), Y(x)) > /\x.Y(x) because [49], by definition 49] /\y.mul*(X(y), Y(y)) >= /\y.Y(y) because [50], by (Abs) 50] mul*(X(x), Y(x)) >= Y(x) because [51], by (Select) 51] Y(x) >= Y(x) because [52], by (Meta) 52] x >= x by (Var) 53] d#(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y) because [54], by (Star) 54] d#*(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y) because d# in Mul, [55] and [60], by (Stat) 55] /\x.sin(X(x)) > /\x.X(x) because [56], by definition 56] /\y.sin*(X(y)) >= /\y.X(y) because [57], by (Abs) 57] sin*(X(x)) >= X(x) because [58], by (Select) 58] X(x) >= X(x) because [59], by (Meta) 59] x >= x by (Var) 60] Y >= Y by (Meta) 61] d#(/\x.sin(X(x)), Y) >= X(_|_) because [62], by (Star) 62] d#*(/\x.sin(X(x)), Y) >= X(_|_) because [63], by (Select) 63] sin(X(d#*(/\x.sin(X(x)), Y))) >= X(_|_) because [64], by (Star) 64] sin*(X(d#*(/\x.sin(X(x)), Y))) >= X(_|_) because [65], by (Select) 65] X(d#*(/\x.sin(X(x)), Y)) >= X(_|_) because [66], by (Meta) 66] d#*(/\x.sin(X(x)), Y) >= _|_ by (Bot) 67] d(/\x.X, Y) >= _|_ by (Bot) 68] d(/\x.x, X) >= _|_ by (Bot) 69] d(/\x.minus(X(x)), Y) >= minus(d(/\x.X(x), Y)) because [70], by (Star) 70] d*(/\x.minus(X(x)), Y) >= minus(d(/\x.X(x), Y)) because d > minus and [71], by (Copy) 71] d*(/\x.minus(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [72] and [7], by (Stat) 72] /\x.minus(X(x)) > /\x.X(x) because [73], by definition 73] /\y.minus*(X(y)) >= /\y.X(y) because [74], by (Abs) 74] minus*(X(x)) >= X(x) because [75], by (Select) 75] X(x) >= X(x) because [76], by (Meta) 76] x >= x by (Var) 77] d(/\x.pls(X(x), Y(x)), Z) >= pls(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because [78], by (Star) 78] d*(/\x.pls(X(x), Y(x)), Z) >= pls(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because d > pls, [79] and [85], by (Copy) 79] d*(/\x.pls(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [80] and [20], by (Stat) 80] /\x.pls(X(x), Y(x)) > /\x.X(x) because [81], by definition 81] /\y.pls*(X(y), Y(y)) >= /\y.X(y) because [82], by (Abs) 82] pls*(X(x), Y(x)) >= X(x) because [83], by (Select) 83] X(x) >= X(x) because [84], by (Meta) 84] x >= x by (Var) 85] d*(/\y.pls(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because d in Mul, [86] and [20], by (Stat) 86] /\y.pls(X(y), Y(y)) > /\y.Y(y) because [87], by definition 87] /\z.pls*(X(z), Y(z)) >= /\z.Y(z) because [88], by (Abs) 88] pls*(X(y), Y(y)) >= Y(y) because [89], by (Select) 89] Y(y) >= Y(y) because [90], by (Meta) 90] y >= y by (Var) 91] d(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\x.X(x), Z), Y(Z)), mul(X(Z), d(/\y.Y(y), Z))) because [92], by (Star) 92] d*(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\x.X(x), Z), Y(Z)), mul(X(Z), d(/\y.Y(y), Z))) because d > pls, [93] and [105], by (Copy) 93] d*(/\x.mul(X(x), Y(x)), Z) >= mul(d(/\x.X(x), Z), Y(Z)) because d > mul, [94] and [100], by (Copy) 94] d*(/\x.mul(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [95] and [39], by (Stat) 95] /\x.mul(X(x), Y(x)) > /\x.X(x) because [96], by definition 96] /\y.mul*(X(y), Y(y)) >= /\y.X(y) because [97], by (Abs) 97] mul*(X(x), Y(x)) >= X(x) because [98], by (Select) 98] X(x) >= X(x) because [99], by (Meta) 99] x >= x by (Var) 100] d*(/\y.mul(X(y), Y(y)), Z) >= Y(Z) because [101], by (Select) 101] mul(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [102], by (Star) 102] mul*(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [103], by (Select) 103] Y(d*(/\y.mul(X(y), Y(y)), Z)) >= Y(Z) because [104], by (Meta) 104] d*(/\y.mul(X(y), Y(y)), Z) >= Z because [39], by (Select) 105] d*(/\y.mul(X(y), Y(y)), Z) >= mul(X(Z), d(/\y.Y(y), Z)) because d > mul, [106] and [110], by (Copy) 106] d*(/\y.mul(X(y), Y(y)), Z) >= X(Z) because [107], by (Select) 107] mul(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [108], by (Star) 108] mul*(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [109], by (Select) 109] X(d*(/\y.mul(X(y), Y(y)), Z)) >= X(Z) because [104], by (Meta) 110] d*(/\y.mul(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because d in Mul, [48] and [39], by (Stat) 111] d(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\x.X(x), Y)) because [112], by (Star) 112] d*(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\x.X(x), Y)) because d > mul, [113] and [115], by (Copy) 113] d*(/\x.sin(X(x)), Y) >= cos(Y) because d > cos and [114], by (Copy) 114] d*(/\x.sin(X(x)), Y) >= Y because [60], by (Select) 115] d*(/\x.sin(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [55] and [60], by (Stat) 116] d(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\x.X(x), Y)) because [117], by (Star) 117] d*(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\x.X(x), Y)) because d > mul, [118] and [122], by (Copy) 118] d*(/\x.cos(X(x)), Y) >= minus(sin(Y)) because d > minus and [119], by (Copy) 119] d*(/\x.cos(X(x)), Y) >= sin(Y) because d > sin and [120], by (Copy) 120] d*(/\x.cos(X(x)), Y) >= Y because [121], by (Select) 121] Y >= Y by (Meta) 122] d*(/\x.cos(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [123] and [128], by (Stat) 123] /\x.cos(X(x)) > /\x.X(x) because [124], by definition 124] /\y.cos*(X(y)) >= /\y.X(y) because [125], by (Abs) 125] cos*(X(x)) >= X(x) because [126], by (Select) 126] X(x) >= X(x) because [127], by (Meta) 127] x >= x by (Var) 128] Y >= Y by (Meta) 129] minus(_|_) >= _|_ by (Bot) 130] mul(_|_, X) >= _|_ by (Bot) 131] mul(X, _|_) >= _|_ by (Bot) 132] pls(_|_, X) >= X because [133], by (Star) 133] pls*(_|_, X) >= X because [134], by (Select) 134] X >= X by (Meta) 135] d(F, X) >= d#(F, X) because [136], by (Star) 136] d*(F, X) >= d#(F, X) because d > d#, [137] and [139], by (Copy) 137] d*(F, X) >= F because [138], by (Select) 138] F >= F by (Meta) 139] d*(F, X) >= X because [140], by (Select) 140] 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.pls(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) d#(/\x.pls(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z) d#(/\x.mul(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) d#(/\x.mul(X(x), Y(x)), Z) =#> X(y) d#(/\x.sin(X(x)), Y) =#> d#(/\y.X(y), Y) d#(/\x.sin(X(x)), Y) =#> X(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.pls(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) d#(/\x.pls(X(x), Y(x)), Z) >? d#(/\y.Y(y), Z) d#(/\x.mul(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) d#(/\x.mul(X(x), Y(x)), Z) >? X(~c0) d#(/\x.sin(X(x)), Y) >? d#(/\y.X(y), Y) d#(/\x.sin(X(x)), Y) >? X(~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.pls(X(x), Y(x)), Z) >= pls(d(/\y.X(y), Z), d(/\z.Y(z), Z)) d(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\y.X(y), Z), Y(Z)), mul(X(Z), d(/\z.Y(z), Z))) d(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\y.X(y), Y)) d(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\y.X(y), Y)) minus(0) >= 0 mul(0, X) >= 0 mul(X, 0) >= 0 pls(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, mul, pls, sin}, and the following precedence: d > d# > minus > cos > pls > mul > 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.pls(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) d#(/\x.pls(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) d#(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) d#(/\x.mul(X(x), Y(x)), Z) > X(_|_) d#(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y) d#(/\x.sin(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.pls(X(x), Y(x)), Z) >= pls(d(/\x.X(x), Z), d(/\y.Y(y), Z)) d(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\x.X(x), Z), Y(Z)), mul(X(Z), d(/\y.Y(y), Z))) d(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\x.X(x), Y)) d(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\x.X(x), Y)) minus(_|_) >= _|_ mul(_|_, X) >= _|_ mul(X, _|_) >= _|_ pls(_|_, 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.pls(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because d# in Mul, [9] and [14], by (Fun) 9] /\y.pls(X(y), Y(y)) >= /\y.X(y) because [10], by (Abs) 10] pls(X(x), Y(x)) >= X(x) because [11], by (Star) 11] pls*(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.pls(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) because d# in Mul, [16] and [14], by (Fun) 16] /\y.pls(X(y), Y(y)) >= /\y.Y(y) because [17], by (Abs) 17] pls(X(x), Y(x)) >= Y(x) because [18], by (Star) 18] pls*(X(x), Y(x)) >= Y(x) because [19], by (Select) 19] Y(x) >= Y(x) because [20], by (Meta) 20] x >= x by (Var) 21] d#(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because [22], by (Star) 22] d#*(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because d# in Mul, [23] and [28], by (Stat) 23] /\x.mul(X(x), Y(x)) > /\x.X(x) because [24], by definition 24] /\y.mul*(X(y), Y(y)) >= /\y.X(y) because [25], by (Abs) 25] mul*(X(x), Y(x)) >= X(x) because [26], by (Select) 26] X(x) >= X(x) because [27], by (Meta) 27] x >= x by (Var) 28] Z >= Z by (Meta) 29] d#(/\x.mul(X(x), Y(x)), Z) > X(_|_) because [30], by definition 30] d#*(/\x.mul(X(x), Y(x)), Z) >= X(_|_) because [31], by (Select) 31] mul(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= X(_|_) because [32], by (Star) 32] mul*(X(d#*(/\x.mul(X(x), Y(x)), Z)), Y(d#*(/\y.mul(X(y), Y(y)), Z))) >= X(_|_) because [33], by (Select) 33] X(d#*(/\x.mul(X(x), Y(x)), Z)) >= X(_|_) because [34], by (Meta) 34] d#*(/\x.mul(X(x), Y(x)), Z) >= _|_ by (Bot) 35] d#(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y) because [36], by (Star) 36] d#*(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y) because d# in Mul, [37] and [42], by (Stat) 37] /\x.sin(X(x)) > /\x.X(x) because [38], by definition 38] /\y.sin*(X(y)) >= /\y.X(y) because [39], by (Abs) 39] sin*(X(x)) >= X(x) because [40], by (Select) 40] X(x) >= X(x) because [41], by (Meta) 41] x >= x by (Var) 42] Y >= Y by (Meta) 43] d#(/\x.sin(X(x)), Y) >= X(_|_) because [44], by (Star) 44] d#*(/\x.sin(X(x)), Y) >= X(_|_) because [45], by (Select) 45] sin(X(d#*(/\x.sin(X(x)), Y))) >= X(_|_) because [46], by (Star) 46] sin*(X(d#*(/\x.sin(X(x)), Y))) >= X(_|_) because [47], by (Select) 47] X(d#*(/\x.sin(X(x)), Y)) >= X(_|_) because [48], by (Meta) 48] d#*(/\x.sin(X(x)), Y) >= _|_ by (Bot) 49] d(/\x.X, Y) >= _|_ by (Bot) 50] d(/\x.x, X) >= _|_ by (Bot) 51] d(/\x.minus(X(x)), Y) >= minus(d(/\x.X(x), Y)) because [52], by (Star) 52] d*(/\x.minus(X(x)), Y) >= minus(d(/\x.X(x), Y)) because d > minus and [53], by (Copy) 53] d*(/\x.minus(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [54] and [7], by (Stat) 54] /\x.minus(X(x)) > /\x.X(x) because [55], by definition 55] /\y.minus*(X(y)) >= /\y.X(y) because [56], by (Abs) 56] minus*(X(x)) >= X(x) because [57], by (Select) 57] X(x) >= X(x) because [58], by (Meta) 58] x >= x by (Var) 59] d(/\x.pls(X(x), Y(x)), Z) >= pls(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because [60], by (Star) 60] d*(/\x.pls(X(x), Y(x)), Z) >= pls(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because d > pls, [61] and [67], by (Copy) 61] d*(/\x.pls(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [62] and [14], by (Stat) 62] /\x.pls(X(x), Y(x)) > /\x.X(x) because [63], by definition 63] /\y.pls*(X(y), Y(y)) >= /\y.X(y) because [64], by (Abs) 64] pls*(X(x), Y(x)) >= X(x) because [65], by (Select) 65] X(x) >= X(x) because [66], by (Meta) 66] x >= x by (Var) 67] d*(/\y.pls(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because d in Mul, [68] and [14], by (Stat) 68] /\y.pls(X(y), Y(y)) > /\y.Y(y) because [69], by definition 69] /\z.pls*(X(z), Y(z)) >= /\z.Y(z) because [70], by (Abs) 70] pls*(X(y), Y(y)) >= Y(y) because [71], by (Select) 71] Y(y) >= Y(y) because [72], by (Meta) 72] y >= y by (Var) 73] d(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\x.X(x), Z), Y(Z)), mul(X(Z), d(/\y.Y(y), Z))) because [74], by (Star) 74] d*(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\x.X(x), Z), Y(Z)), mul(X(Z), d(/\y.Y(y), Z))) because d > pls, [75] and [82], by (Copy) 75] d*(/\x.mul(X(x), Y(x)), Z) >= mul(d(/\x.X(x), Z), Y(Z)) because d > mul, [76] and [77], by (Copy) 76] d*(/\x.mul(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [23] and [28], by (Stat) 77] d*(/\x.mul(X(x), Y(x)), Z) >= Y(Z) because [78], by (Select) 78] mul(X(d*(/\x.mul(X(x), Y(x)), Z)), Y(d*(/\y.mul(X(y), Y(y)), Z))) >= Y(Z) because [79], by (Star) 79] mul*(X(d*(/\x.mul(X(x), Y(x)), Z)), Y(d*(/\y.mul(X(y), Y(y)), Z))) >= Y(Z) because [80], by (Select) 80] Y(d*(/\x.mul(X(x), Y(x)), Z)) >= Y(Z) because [81], by (Meta) 81] d*(/\x.mul(X(x), Y(x)), Z) >= Z because [28], by (Select) 82] d*(/\x.mul(X(x), Y(x)), Z) >= mul(X(Z), d(/\x.Y(x), Z)) because d > mul, [83] and [87], by (Copy) 83] d*(/\x.mul(X(x), Y(x)), Z) >= X(Z) because [84], by (Select) 84] mul(X(d*(/\x.mul(X(x), Y(x)), Z)), Y(d*(/\y.mul(X(y), Y(y)), Z))) >= X(Z) because [85], by (Star) 85] mul*(X(d*(/\x.mul(X(x), Y(x)), Z)), Y(d*(/\y.mul(X(y), Y(y)), Z))) >= X(Z) because [86], by (Select) 86] X(d*(/\x.mul(X(x), Y(x)), Z)) >= X(Z) because [81], by (Meta) 87] d*(/\x.mul(X(x), Y(x)), Z) >= d(/\x.Y(x), Z) because d in Mul, [88] and [28], by (Stat) 88] /\x.mul(X(x), Y(x)) > /\x.Y(x) because [89], by definition 89] /\y.mul*(X(y), Y(y)) >= /\y.Y(y) because [90], by (Abs) 90] mul*(X(x), Y(x)) >= Y(x) because [91], by (Select) 91] Y(x) >= Y(x) because [92], by (Meta) 92] x >= x by (Var) 93] d(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\x.X(x), Y)) because [94], by (Star) 94] d*(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\x.X(x), Y)) because d > mul, [95] and [97], by (Copy) 95] d*(/\x.sin(X(x)), Y) >= cos(Y) because d > cos and [96], by (Copy) 96] d*(/\x.sin(X(x)), Y) >= Y because [42], by (Select) 97] d*(/\x.sin(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [37] and [42], by (Stat) 98] d(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\x.X(x), Y)) because [99], by (Star) 99] d*(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\x.X(x), Y)) because d > mul, [100] and [104], by (Copy) 100] d*(/\x.cos(X(x)), Y) >= minus(sin(Y)) because d > minus and [101], by (Copy) 101] d*(/\x.cos(X(x)), Y) >= sin(Y) because d > sin and [102], by (Copy) 102] d*(/\x.cos(X(x)), Y) >= Y because [103], by (Select) 103] Y >= Y by (Meta) 104] d*(/\x.cos(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [105] and [110], by (Stat) 105] /\x.cos(X(x)) > /\x.X(x) because [106], by definition 106] /\y.cos*(X(y)) >= /\y.X(y) because [107], by (Abs) 107] cos*(X(x)) >= X(x) because [108], by (Select) 108] X(x) >= X(x) because [109], by (Meta) 109] x >= x by (Var) 110] Y >= Y by (Meta) 111] minus(_|_) >= _|_ by (Bot) 112] mul(_|_, X) >= _|_ by (Bot) 113] mul(X, _|_) >= _|_ by (Bot) 114] pls(_|_, X) >= X because [115], by (Star) 115] pls*(_|_, X) >= X because [116], by (Select) 116] X >= X by (Meta) 117] d(F, X) >= d#(F, X) because [118], by (Star) 118] d*(F, X) >= d#(F, X) because d > d#, [119] and [121], by (Copy) 119] d*(F, X) >= F because [120], by (Select) 120] F >= F by (Meta) 121] d*(F, X) >= X because [122], by (Select) 122] 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.pls(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) d#(/\x.pls(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z) d#(/\x.mul(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) d#(/\x.sin(X(x)), Y) =#> d#(/\y.X(y), Y) d#(/\x.sin(X(x)), Y) =#> X(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) >? d#(/\y.X(y), Y) d#(/\x.pls(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) d#(/\x.pls(X(x), Y(x)), Z) >? d#(/\y.Y(y), Z) d#(/\x.mul(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) d#(/\x.sin(X(x)), Y) >? d#(/\y.X(y), Y) d#(/\x.sin(X(x)), Y) >? X(~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.pls(X(x), Y(x)), Z) >= pls(d(/\y.X(y), Z), d(/\z.Y(z), Z)) d(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\y.X(y), Z), Y(Z)), mul(X(Z), d(/\z.Y(z), Z))) d(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\y.X(y), Y)) d(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\y.X(y), Y)) minus(0) >= 0 mul(0, X) >= 0 mul(X, 0) >= 0 pls(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) [[~c0]] = _|_ We choose Lex = {d#} and Mul = {cos, d, minus, mul, pls, sin}, and the following precedence: d > cos > d# > minus > mul > pls > 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.pls(X(x), Y(x)), Z) > d#(/\x.X(x), Z) d#(/\x.pls(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) d#(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) d#(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y) d#(/\x.sin(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.pls(X(x), Y(x)), Z) >= pls(d(/\x.X(x), Z), d(/\y.Y(y), Z)) d(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\x.X(x), Z), Y(Z)), mul(X(Z), d(/\y.Y(y), Z))) d(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\x.X(x), Y)) d(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\x.X(x), Y)) minus(_|_) >= _|_ mul(_|_, X) >= _|_ mul(X, _|_) >= _|_ pls(_|_, 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] 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.pls(X(x), Y(x)), Z) > d#(/\x.X(x), Z) because [9], by definition 9] d#*(/\x.pls(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because [10], [15], [16] and [22], by (Stat) 10] /\x.pls(X(x), Y(x)) > /\x.X(x) because [11], by definition 11] /\y.pls*(X(y), Y(y)) >= /\y.X(y) because [12], by (Abs) 12] pls*(X(x), Y(x)) >= X(x) because [13], by (Select) 13] X(x) >= X(x) because [14], by (Meta) 14] x >= x by (Var) 15] Z >= Z by (Meta) 16] d#*(/\y.pls(X(y), Y(y)), Z) >= /\y.X(y) because [17], by (Select) 17] /\z.pls(X(z), Y(z)) >= /\z.X(z) because [18], by (Abs) 18] pls(X(y), Y(y)) >= X(y) because [19], by (Star) 19] pls*(X(y), Y(y)) >= X(y) because [20], by (Select) 20] X(y) >= X(y) because [21], by (Meta) 21] y >= y by (Var) 22] d#*(/\z.pls(X(z), Y(z)), Z) >= Z because [15], by (Select) 23] d#(/\x.pls(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) because [24] and [15], by (Fun) 24] /\y.pls(X(y), Y(y)) >= /\y.Y(y) because [25], by (Abs) 25] pls(X(x), Y(x)) >= Y(x) because [26], by (Star) 26] pls*(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.mul(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because [30] and [35], by (Fun) 30] /\y.mul(X(y), Y(y)) >= /\y.X(y) because [31], by (Abs) 31] mul(X(x), Y(x)) >= X(x) because [32], by (Star) 32] mul*(X(x), Y(x)) >= X(x) because [33], by (Select) 33] X(x) >= X(x) because [34], by (Meta) 34] x >= x by (Var) 35] Z >= Z by (Meta) 36] d#(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y) because [37] and [42], by (Fun) 37] /\y.sin(X(y)) >= /\y.X(y) because [38], by (Abs) 38] sin(X(x)) >= X(x) because [39], by (Star) 39] sin*(X(x)) >= X(x) because [40], by (Select) 40] X(x) >= X(x) because [41], by (Meta) 41] x >= x by (Var) 42] Y >= Y by (Meta) 43] d#(/\x.sin(X(x)), Y) >= X(_|_) because [44], by (Star) 44] d#*(/\x.sin(X(x)), Y) >= X(_|_) because [45], by (Select) 45] sin(X(d#*(/\x.sin(X(x)), Y))) >= X(_|_) because [46], by (Star) 46] sin*(X(d#*(/\x.sin(X(x)), Y))) >= X(_|_) because [47], by (Select) 47] X(d#*(/\x.sin(X(x)), Y)) >= X(_|_) because [48], by (Meta) 48] d#*(/\x.sin(X(x)), Y) >= _|_ by (Bot) 49] d(/\x.X, Y) >= _|_ by (Bot) 50] d(/\x.x, X) >= _|_ by (Bot) 51] d(/\x.minus(X(x)), Y) >= minus(d(/\x.X(x), Y)) because [52], by (Star) 52] d*(/\x.minus(X(x)), Y) >= minus(d(/\x.X(x), Y)) because d > minus and [53], by (Copy) 53] d*(/\x.minus(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [54] and [7], by (Stat) 54] /\x.minus(X(x)) > /\x.X(x) because [55], by definition 55] /\y.minus*(X(y)) >= /\y.X(y) because [56], by (Abs) 56] minus*(X(x)) >= X(x) because [57], by (Select) 57] X(x) >= X(x) because [58], by (Meta) 58] x >= x by (Var) 59] d(/\x.pls(X(x), Y(x)), Z) >= pls(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because [60], by (Star) 60] d*(/\x.pls(X(x), Y(x)), Z) >= pls(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because d > pls, [61] and [62], by (Copy) 61] d*(/\x.pls(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [10] and [15], by (Stat) 62] d*(/\x.pls(X(x), Y(x)), Z) >= d(/\x.Y(x), Z) because d in Mul, [63] and [15], by (Stat) 63] /\x.pls(X(x), Y(x)) > /\x.Y(x) because [64], by definition 64] /\y.pls*(X(y), Y(y)) >= /\y.Y(y) because [65], by (Abs) 65] pls*(X(x), Y(x)) >= Y(x) because [66], by (Select) 66] Y(x) >= Y(x) because [67], by (Meta) 67] x >= x by (Var) 68] d(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\x.X(x), Z), Y(Z)), mul(X(Z), d(/\y.Y(y), Z))) because [69], by (Star) 69] d*(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\x.X(x), Z), Y(Z)), mul(X(Z), d(/\y.Y(y), Z))) because d > pls, [70] and [82], by (Copy) 70] d*(/\x.mul(X(x), Y(x)), Z) >= mul(d(/\x.X(x), Z), Y(Z)) because d > mul, [71] and [77], by (Copy) 71] d*(/\x.mul(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [72] and [35], by (Stat) 72] /\x.mul(X(x), Y(x)) > /\x.X(x) because [73], by definition 73] /\y.mul*(X(y), Y(y)) >= /\y.X(y) because [74], by (Abs) 74] mul*(X(x), Y(x)) >= X(x) because [75], by (Select) 75] X(x) >= X(x) because [76], by (Meta) 76] x >= x by (Var) 77] d*(/\y.mul(X(y), Y(y)), Z) >= Y(Z) because [78], by (Select) 78] mul(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [79], by (Star) 79] mul*(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [80], by (Select) 80] Y(d*(/\y.mul(X(y), Y(y)), Z)) >= Y(Z) because [81], by (Meta) 81] d*(/\y.mul(X(y), Y(y)), Z) >= Z because [35], by (Select) 82] d*(/\y.mul(X(y), Y(y)), Z) >= mul(X(Z), d(/\y.Y(y), Z)) because d > mul, [83] and [87], by (Copy) 83] d*(/\y.mul(X(y), Y(y)), Z) >= X(Z) because [84], by (Select) 84] mul(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [85], by (Star) 85] mul*(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [86], by (Select) 86] X(d*(/\y.mul(X(y), Y(y)), Z)) >= X(Z) because [81], by (Meta) 87] d*(/\y.mul(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because d in Mul, [88] and [35], by (Stat) 88] /\y.mul(X(y), Y(y)) > /\y.Y(y) because [89], by definition 89] /\z.mul*(X(z), Y(z)) >= /\z.Y(z) because [90], by (Abs) 90] mul*(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.sin(X(x)), Y) >= mul(cos(Y), d(/\x.X(x), Y)) because [94], by (Star) 94] d*(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\x.X(x), Y)) because d > mul, [95] and [97], by (Copy) 95] d*(/\x.sin(X(x)), Y) >= cos(Y) because d > cos and [96], by (Copy) 96] d*(/\x.sin(X(x)), Y) >= Y because [42], by (Select) 97] d*(/\x.sin(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [98] and [42], by (Stat) 98] /\x.sin(X(x)) > /\x.X(x) because [99], by definition 99] /\y.sin*(X(y)) >= /\y.X(y) because [100], by (Abs) 100] sin*(X(x)) >= X(x) because [101], by (Select) 101] X(x) >= X(x) because [102], by (Meta) 102] x >= x by (Var) 103] d(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\x.X(x), Y)) because [104], by (Star) 104] d*(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\x.X(x), Y)) because d > mul, [105] and [109], by (Copy) 105] d*(/\x.cos(X(x)), Y) >= minus(sin(Y)) because d > minus and [106], by (Copy) 106] d*(/\x.cos(X(x)), Y) >= sin(Y) because d > sin and [107], by (Copy) 107] d*(/\x.cos(X(x)), Y) >= Y because [108], by (Select) 108] Y >= Y by (Meta) 109] d*(/\x.cos(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [110] and [115], by (Stat) 110] /\x.cos(X(x)) > /\x.X(x) because [111], by definition 111] /\y.cos*(X(y)) >= /\y.X(y) because [112], by (Abs) 112] cos*(X(x)) >= X(x) because [113], by (Select) 113] X(x) >= X(x) because [114], by (Meta) 114] x >= x by (Var) 115] Y >= Y by (Meta) 116] minus(_|_) >= _|_ by (Bot) 117] mul(_|_, X) >= _|_ by (Bot) 118] mul(X, _|_) >= _|_ by (Bot) 119] pls(_|_, X) >= X because [120], by (Star) 120] pls*(_|_, X) >= X because [121], by (Select) 121] X >= X by (Meta) 122] d(F, X) >= d#(F, X) because [123], by (Star) 123] d*(F, X) >= d#(F, X) because d > d#, [124] and [126], by (Copy) 124] d*(F, X) >= F because [125], by (Select) 125] F >= F by (Meta) 126] d*(F, X) >= X because [127], by (Select) 127] 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.pls(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z) d#(/\x.mul(X(x), Y(x)), Z) =#> d#(/\y.X(y), Z) d#(/\x.sin(X(x)), Y) =#> d#(/\y.X(y), Y) d#(/\x.sin(X(x)), Y) =#> X(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.minus(X(x)), Y) >? d#(/\y.X(y), Y) d#(/\x.pls(X(x), Y(x)), Z) >? d#(/\y.Y(y), Z) d#(/\x.mul(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) d#(/\x.sin(X(x)), Y) >? d#(/\y.X(y), Y) d#(/\x.sin(X(x)), Y) >? X(~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.pls(X(x), Y(x)), Z) >= pls(d(/\y.X(y), Z), d(/\z.Y(z), Z)) d(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\y.X(y), Z), Y(Z)), mul(X(Z), d(/\z.Y(z), Z))) d(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\y.X(y), Y)) d(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\y.X(y), Y)) minus(0) >= 0 mul(0, X) >= 0 mul(X, 0) >= 0 pls(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]] = _|_ We choose Lex = {} and Mul = {cos, d, d#, minus, mul, pls, sin}, and the following precedence: d > cos > d# > minus > pls > mul > 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.pls(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) d#(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) d#(/\x.sin(X(x)), Y) >= d#(/\x.X(x), Y) d#(/\x.sin(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.pls(X(x), Y(x)), Z) >= pls(d(/\x.X(x), Z), d(/\y.Y(y), Z)) d(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\x.X(x), Z), Y(Z)), mul(X(Z), d(/\y.Y(y), Z))) d(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\x.X(x), Y)) d(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\x.X(x), Y)) minus(_|_) >= _|_ mul(_|_, X) >= _|_ mul(X, _|_) >= _|_ pls(_|_, 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.pls(X(x), Y(x)), Z) >= d#(/\x.Y(x), Z) because d# in Mul, [9] and [14], by (Fun) 9] /\y.pls(X(y), Y(y)) >= /\y.Y(y) because [10], by (Abs) 10] pls(X(x), Y(x)) >= Y(x) because [11], by (Star) 11] pls*(X(x), Y(x)) >= Y(x) because [12], by (Select) 12] Y(x) >= Y(x) because [13], by (Meta) 13] x >= x by (Var) 14] Z >= Z by (Meta) 15] d#(/\x.mul(X(x), Y(x)), Z) >= d#(/\x.X(x), Z) because d# in Mul, [16] and [21], by (Fun) 16] /\y.mul(X(y), Y(y)) >= /\y.X(y) because [17], by (Abs) 17] mul(X(x), Y(x)) >= X(x) because [18], by (Star) 18] mul*(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.sin(X(x)), Y) >= d#(/\x.X(x), Y) because d# in Mul, [23] and [28], by (Fun) 23] /\y.sin(X(y)) >= /\y.X(y) because [24], by (Abs) 24] sin(X(x)) >= X(x) because [25], by (Star) 25] sin*(X(x)) >= X(x) because [26], by (Select) 26] X(x) >= X(x) because [27], by (Meta) 27] x >= x by (Var) 28] Y >= Y by (Meta) 29] d#(/\x.sin(X(x)), Y) > X(_|_) because [30], by definition 30] d#*(/\x.sin(X(x)), Y) >= X(_|_) because [31], by (Select) 31] sin(X(d#*(/\x.sin(X(x)), Y))) >= X(_|_) because [32], by (Star) 32] sin*(X(d#*(/\x.sin(X(x)), Y))) >= X(_|_) because [33], by (Select) 33] X(d#*(/\x.sin(X(x)), Y)) >= X(_|_) because [34], by (Meta) 34] d#*(/\x.sin(X(x)), Y) >= _|_ by (Bot) 35] d(/\x.X, Y) >= _|_ by (Bot) 36] d(/\x.x, X) >= _|_ by (Bot) 37] d(/\x.minus(X(x)), Y) >= minus(d(/\x.X(x), Y)) because [38], by (Star) 38] d*(/\x.minus(X(x)), Y) >= minus(d(/\x.X(x), Y)) because d > minus and [39], by (Copy) 39] d*(/\x.minus(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [40] and [7], by (Stat) 40] /\x.minus(X(x)) > /\x.X(x) because [41], by definition 41] /\y.minus*(X(y)) >= /\y.X(y) because [42], by (Abs) 42] minus*(X(x)) >= X(x) because [43], by (Select) 43] X(x) >= X(x) because [44], by (Meta) 44] x >= x by (Var) 45] d(/\x.pls(X(x), Y(x)), Z) >= pls(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because [46], by (Star) 46] d*(/\x.pls(X(x), Y(x)), Z) >= pls(d(/\x.X(x), Z), d(/\y.Y(y), Z)) because d > pls, [47] and [53], by (Copy) 47] d*(/\x.pls(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [48] and [14], by (Stat) 48] /\x.pls(X(x), Y(x)) > /\x.X(x) because [49], by definition 49] /\y.pls*(X(y), Y(y)) >= /\y.X(y) because [50], by (Abs) 50] pls*(X(x), Y(x)) >= X(x) because [51], by (Select) 51] X(x) >= X(x) because [52], by (Meta) 52] x >= x by (Var) 53] d*(/\y.pls(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because d in Mul, [54] and [14], by (Stat) 54] /\y.pls(X(y), Y(y)) > /\y.Y(y) because [55], by definition 55] /\z.pls*(X(z), Y(z)) >= /\z.Y(z) because [56], by (Abs) 56] pls*(X(y), Y(y)) >= Y(y) because [57], by (Select) 57] Y(y) >= Y(y) because [58], by (Meta) 58] y >= y by (Var) 59] d(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\x.X(x), Z), Y(Z)), mul(X(Z), d(/\y.Y(y), Z))) because [60], by (Star) 60] d*(/\x.mul(X(x), Y(x)), Z) >= pls(mul(d(/\x.X(x), Z), Y(Z)), mul(X(Z), d(/\y.Y(y), Z))) because d > pls, [61] and [73], by (Copy) 61] d*(/\x.mul(X(x), Y(x)), Z) >= mul(d(/\x.X(x), Z), Y(Z)) because d > mul, [62] and [68], by (Copy) 62] d*(/\x.mul(X(x), Y(x)), Z) >= d(/\x.X(x), Z) because d in Mul, [63] and [21], by (Stat) 63] /\x.mul(X(x), Y(x)) > /\x.X(x) because [64], by definition 64] /\y.mul*(X(y), Y(y)) >= /\y.X(y) because [65], by (Abs) 65] mul*(X(x), Y(x)) >= X(x) because [66], by (Select) 66] X(x) >= X(x) because [67], by (Meta) 67] x >= x by (Var) 68] d*(/\y.mul(X(y), Y(y)), Z) >= Y(Z) because [69], by (Select) 69] mul(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [70], by (Star) 70] mul*(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= Y(Z) because [71], by (Select) 71] Y(d*(/\y.mul(X(y), Y(y)), Z)) >= Y(Z) because [72], by (Meta) 72] d*(/\y.mul(X(y), Y(y)), Z) >= Z because [21], by (Select) 73] d*(/\y.mul(X(y), Y(y)), Z) >= mul(X(Z), d(/\y.Y(y), Z)) because d > mul, [74] and [78], by (Copy) 74] d*(/\y.mul(X(y), Y(y)), Z) >= X(Z) because [75], by (Select) 75] mul(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [76], by (Star) 76] mul*(X(d*(/\y.mul(X(y), Y(y)), Z)), Y(d*(/\z.mul(X(z), Y(z)), Z))) >= X(Z) because [77], by (Select) 77] X(d*(/\y.mul(X(y), Y(y)), Z)) >= X(Z) because [72], by (Meta) 78] d*(/\y.mul(X(y), Y(y)), Z) >= d(/\y.Y(y), Z) because d in Mul, [79] and [21], by (Stat) 79] /\y.mul(X(y), Y(y)) > /\y.Y(y) because [80], by definition 80] /\z.mul*(X(z), Y(z)) >= /\z.Y(z) because [81], by (Abs) 81] mul*(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(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\x.X(x), Y)) because [85], by (Star) 85] d*(/\x.sin(X(x)), Y) >= mul(cos(Y), d(/\x.X(x), Y)) because d > mul, [86] and [88], by (Copy) 86] d*(/\x.sin(X(x)), Y) >= cos(Y) because d > cos and [87], by (Copy) 87] d*(/\x.sin(X(x)), Y) >= Y because [28], by (Select) 88] d*(/\x.sin(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [89] and [28], by (Stat) 89] /\x.sin(X(x)) > /\x.X(x) because [90], by definition 90] /\y.sin*(X(y)) >= /\y.X(y) because [91], by (Abs) 91] sin*(X(x)) >= X(x) because [92], by (Select) 92] X(x) >= X(x) because [93], by (Meta) 93] x >= x by (Var) 94] d(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\x.X(x), Y)) because [95], by (Star) 95] d*(/\x.cos(X(x)), Y) >= mul(minus(sin(Y)), d(/\x.X(x), Y)) because d > mul, [96] and [100], by (Copy) 96] d*(/\x.cos(X(x)), Y) >= minus(sin(Y)) because d > minus and [97], by (Copy) 97] d*(/\x.cos(X(x)), Y) >= sin(Y) because d > sin and [98], by (Copy) 98] d*(/\x.cos(X(x)), Y) >= Y because [99], by (Select) 99] Y >= Y by (Meta) 100] d*(/\x.cos(X(x)), Y) >= d(/\x.X(x), Y) because d in Mul, [101] and [106], by (Stat) 101] /\x.cos(X(x)) > /\x.X(x) because [102], by definition 102] /\y.cos*(X(y)) >= /\y.X(y) because [103], by (Abs) 103] cos*(X(x)) >= X(x) because [104], by (Select) 104] X(x) >= X(x) because [105], by (Meta) 105] x >= x by (Var) 106] Y >= Y by (Meta) 107] minus(_|_) >= _|_ by (Bot) 108] mul(_|_, X) >= _|_ by (Bot) 109] mul(X, _|_) >= _|_ by (Bot) 110] pls(_|_, X) >= X because [111], by (Star) 111] pls*(_|_, X) >= X because [112], by (Select) 112] X >= X by (Meta) 113] d(F, X) >= d#(F, X) because [114], by (Star) 114] d*(F, X) >= d#(F, X) because d > d#, [115] and [117], by (Copy) 115] d*(F, X) >= F because [116], by (Select) 116] F >= F by (Meta) 117] d*(F, X) >= X because [118], by (Select) 118] 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.pls(X(x), Y(x)), Z) =#> d#(/\y.Y(y), Z) d#(/\x.mul(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_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.minus(X(x)), Y) >? d#(/\y.X(y), Y) d#(/\x.pls(X(x), Y(x)), Z) >? d#(/\y.Y(y), Z) d#(/\x.mul(X(x), Y(x)), Z) >? d#(/\y.X(y), Z) d#(/\x.sin(X(x)), Y) >? d#(/\y.X(y), Y) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: d# = \G0y1.2y1G0(y1) + 3G0(0) + 3G0(y1) minus = \y0.3 + 3y0 mul = \y0y1.3 + 3y0 pls = \y0y1.3 + 3y1 sin = \y0.3 + 3y0 Using this interpretation, the requirements translate to: [[d#(/\x.minus(_x0(x)), _x1)]] = 18 + 6x1 + 6x1F0(x1) + 9F0(0) + 9F0(x1) > 2x1F0(x1) + 3F0(0) + 3F0(x1) = [[d#(/\x._x0(x), _x1)]] [[d#(/\x.pls(_x0(x), _x1(x)), _x2)]] = 18 + 6x2 + 6x2F1(x2) + 9F1(0) + 9F1(x2) > 2x2F1(x2) + 3F1(0) + 3F1(x2) = [[d#(/\x._x1(x), _x2)]] [[d#(/\x.mul(_x0(x), _x1(x)), _x2)]] = 18 + 6x2 + 6x2F0(x2) + 9F0(0) + 9F0(x2) > 2x2F0(x2) + 3F0(0) + 3F0(x2) = [[d#(/\x._x0(x), _x2)]] [[d#(/\x.sin(_x0(x)), _x1)]] = 18 + 6x1 + 6x1F0(x1) + 9F0(0) + 9F0(x1) > 2x1F0(x1) + 3F0(0) + 3F0(x1) = [[d#(/\x._x0(x), _x1)]] 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 +++ [Kop11] C. Kop. Simplifying Algebraic Functional Systems. In Proceedings of CAI 2011, volume 6742 of LNCS. 201--215, Springer, 2011. [Kop12] C. Kop. Higher Order Termination. PhD Thesis, 2012.