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