We consider the system Applicative_first_order_05__11. Alphabet: !facminus : [a * a] --> a !facplus : [a * a] --> a !factimes : [a * a] --> a 0 : [] --> a 1 : [] --> a 2 : [] --> a D : [a] --> a cons : [c * d] --> d constant : [] --> a div : [a * a] --> a false : [] --> b filter : [c -> b * d] --> d filter2 : [b * c -> b * c * d] --> d ln : [a] --> a map : [c -> c * d] --> d minus : [a] --> a nil : [] --> d pow : [a * a] --> a t : [] --> a true : [] --> b Rules: D(t) => 1 D(constant) => 0 D(!facplus(x, y)) => !facplus(D(x), D(y)) D(!factimes(x, y)) => !facplus(!factimes(y, D(x)), !factimes(x, D(y))) D(!facminus(x, y)) => !facminus(D(x), D(y)) D(minus(x)) => minus(D(x)) D(div(x, y)) => !facminus(div(D(x), y), div(!factimes(x, D(y)), pow(y, 2))) D(ln(x)) => div(D(x), x) D(pow(x, y)) => !facplus(!factimes(!factimes(y, pow(x, !facminus(y, 1))), D(x)), !factimes(!factimes(pow(x, y), ln(x)), D(y))) map(f, nil) => nil map(f, cons(x, y)) => cons(f x, map(f, y)) filter(f, nil) => nil filter(f, cons(x, y)) => filter2(f x, f, x, y) filter2(true, f, x, y) => cons(x, filter(f, y)) filter2(false, f, x, y) => filter(f, y) This AFS is converted to an AFSM simply by replacing all free variables by meta-variables (with arity 0). We use the dependency pair framework as described in [Kop12, Ch. 6/7], with static dependency pairs (see [KusIsoSakBla09] and the adaptation for AFSMs and accessible arguments in [Kop13]). We thus obtain the following dependency pair problem (P_0, R_0, static, formative): Dependency Pairs P_0: 0] D#(!facplus(X, Y)) =#> D#(X) 1] D#(!facplus(X, Y)) =#> D#(Y) 2] D#(!factimes(X, Y)) =#> D#(X) 3] D#(!factimes(X, Y)) =#> D#(Y) 4] D#(!facminus(X, Y)) =#> D#(X) 5] D#(!facminus(X, Y)) =#> D#(Y) 6] D#(minus(X)) =#> D#(X) 7] D#(div(X, Y)) =#> D#(X) 8] D#(div(X, Y)) =#> D#(Y) 9] D#(ln(X)) =#> D#(X) 10] D#(pow(X, Y)) =#> D#(X) 11] D#(pow(X, Y)) =#> D#(Y) 12] map#(F, cons(X, Y)) =#> map#(F, Y) 13] filter#(F, cons(X, Y)) =#> filter2#(F X, F, X, Y) 14] filter2#(true, F, X, Y) =#> filter#(F, Y) 15] filter2#(false, F, X, Y) =#> filter#(F, Y) Rules R_0: D(t) => 1 D(constant) => 0 D(!facplus(X, Y)) => !facplus(D(X), D(Y)) D(!factimes(X, Y)) => !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X, Y)) => !facminus(D(X), D(Y)) D(minus(X)) => minus(D(X)) D(div(X, Y)) => !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) D(ln(X)) => div(D(X), X) D(pow(X, Y)) => !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) map(F, nil) => nil map(F, cons(X, Y)) => cons(F X, map(F, Y)) filter(F, nil) => nil filter(F, cons(X, Y)) => filter2(F X, F, X, Y) filter2(true, F, X, Y) => cons(X, filter(F, Y)) filter2(false, F, X, Y) => filter(F, Y) Thus, the original system is terminating if (P_0, R_0, static, formative) is finite. We consider the dependency pair problem (P_0, R_0, static, formative). The formative rules of (P_0, R_0) are R_1 ::= D(!facplus(X, Y)) => !facplus(D(X), D(Y)) D(!factimes(X, Y)) => !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X, Y)) => !facminus(D(X), D(Y)) D(minus(X)) => minus(D(X)) D(div(X, Y)) => !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) D(ln(X)) => div(D(X), X) D(pow(X, Y)) => !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) map(F, cons(X, Y)) => cons(F X, map(F, Y)) filter(F, cons(X, Y)) => filter2(F X, F, X, Y) filter2(true, F, X, Y) => cons(X, filter(F, Y)) filter2(false, F, X, Y) => filter(F, Y) By [Kop12, Thm. 7.17], we may replace the dependency pair problem (P_0, R_0, static, formative) by (P_0, R_1, static, formative). Thus, the original system is terminating if (P_0, R_1, static, formative) is finite. We consider the dependency pair problem (P_0, R_1, static, formative). 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#(!facplus(X, Y)) >? D#(X) D#(!facplus(X, Y)) >? D#(Y) D#(!factimes(X, Y)) >? D#(X) D#(!factimes(X, Y)) >? D#(Y) D#(!facminus(X, Y)) >? D#(X) D#(!facminus(X, Y)) >? D#(Y) D#(minus(X)) >? D#(X) D#(div(X, Y)) >? D#(X) D#(div(X, Y)) >? D#(Y) D#(ln(X)) >? D#(X) D#(pow(X, Y)) >? D#(X) D#(pow(X, Y)) >? D#(Y) map#(F, cons(X, Y)) >? map#(F, Y) filter#(F, cons(X, Y)) >? filter2#(F X, F, X, Y) filter2#(true, F, X, Y) >? filter#(F, Y) filter2#(false, F, X, Y) >? filter#(F, Y) D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) D(minus(X)) >= minus(D(X)) D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) D(ln(X)) >= div(D(X), X) D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) map(F, cons(X, Y)) >= cons(F X, map(F, Y)) filter(F, cons(X, Y)) >= filter2(F X, F, X, Y) filter2(true, F, X, Y) >= cons(X, filter(F, Y)) filter2(false, F, X, Y) >= filter(F, Y) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: !facminus = \y0y1.0 !facplus = \y0y1.0 !factimes = \y0y1.0 1 = 0 2 = 0 D = \y0.0 D# = \y0.0 cons = \y0y1.1 + 2y1 div = \y0y1.0 false = 3 filter = \G0y1.y1 filter2 = \y0G1y2y3.1 + 2y3 filter2# = \y0G1y2y3.1 + 2y3 + 2y3G1(y3) filter# = \G0y1.y1 + 2y1G0(y1) ln = \y0.0 map = \G0y1.y1 map# = \G0y1.0 minus = \y0.0 pow = \y0y1.0 true = 3 Using this interpretation, the requirements translate to: [[D#(!facplus(_x0, _x1))]] = 0 >= 0 = [[D#(_x0)]] [[D#(!facplus(_x0, _x1))]] = 0 >= 0 = [[D#(_x1)]] [[D#(!factimes(_x0, _x1))]] = 0 >= 0 = [[D#(_x0)]] [[D#(!factimes(_x0, _x1))]] = 0 >= 0 = [[D#(_x1)]] [[D#(!facminus(_x0, _x1))]] = 0 >= 0 = [[D#(_x0)]] [[D#(!facminus(_x0, _x1))]] = 0 >= 0 = [[D#(_x1)]] [[D#(minus(_x0))]] = 0 >= 0 = [[D#(_x0)]] [[D#(div(_x0, _x1))]] = 0 >= 0 = [[D#(_x0)]] [[D#(div(_x0, _x1))]] = 0 >= 0 = [[D#(_x1)]] [[D#(ln(_x0))]] = 0 >= 0 = [[D#(_x0)]] [[D#(pow(_x0, _x1))]] = 0 >= 0 = [[D#(_x0)]] [[D#(pow(_x0, _x1))]] = 0 >= 0 = [[D#(_x1)]] [[map#(_F0, cons(_x1, _x2))]] = 0 >= 0 = [[map#(_F0, _x2)]] [[filter#(_F0, cons(_x1, _x2))]] = 1 + 2x2 + 2F0(1 + 2x2) + 4x2F0(1 + 2x2) >= 1 + 2x2 + 2x2F0(x2) = [[filter2#(_F0 _x1, _F0, _x1, _x2)]] [[filter2#(true, _F0, _x1, _x2)]] = 1 + 2x2 + 2x2F0(x2) > x2 + 2x2F0(x2) = [[filter#(_F0, _x2)]] [[filter2#(false, _F0, _x1, _x2)]] = 1 + 2x2 + 2x2F0(x2) > x2 + 2x2F0(x2) = [[filter#(_F0, _x2)]] [[D(!facplus(_x0, _x1))]] = 0 >= 0 = [[!facplus(D(_x0), D(_x1))]] [[D(!factimes(_x0, _x1))]] = 0 >= 0 = [[!facplus(!factimes(_x1, D(_x0)), !factimes(_x0, D(_x1)))]] [[D(!facminus(_x0, _x1))]] = 0 >= 0 = [[!facminus(D(_x0), D(_x1))]] [[D(minus(_x0))]] = 0 >= 0 = [[minus(D(_x0))]] [[D(div(_x0, _x1))]] = 0 >= 0 = [[!facminus(div(D(_x0), _x1), div(!factimes(_x0, D(_x1)), pow(_x1, 2)))]] [[D(ln(_x0))]] = 0 >= 0 = [[div(D(_x0), _x0)]] [[D(pow(_x0, _x1))]] = 0 >= 0 = [[!facplus(!factimes(!factimes(_x1, pow(_x0, !facminus(_x1, 1))), D(_x0)), !factimes(!factimes(pow(_x0, _x1), ln(_x0)), D(_x1)))]] [[map(_F0, cons(_x1, _x2))]] = 1 + 2x2 >= 1 + 2x2 = [[cons(_F0 _x1, map(_F0, _x2))]] [[filter(_F0, cons(_x1, _x2))]] = 1 + 2x2 >= 1 + 2x2 = [[filter2(_F0 _x1, _F0, _x1, _x2)]] [[filter2(true, _F0, _x1, _x2)]] = 1 + 2x2 >= 1 + 2x2 = [[cons(_x1, filter(_F0, _x2))]] [[filter2(false, _F0, _x1, _x2)]] = 1 + 2x2 >= x2 = [[filter(_F0, _x2)]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_0, R_1, static, formative) by (P_1, R_1, static, formative), where P_1 consists of: D#(!facplus(X, Y)) =#> D#(X) D#(!facplus(X, Y)) =#> D#(Y) D#(!factimes(X, Y)) =#> D#(X) D#(!factimes(X, Y)) =#> D#(Y) D#(!facminus(X, Y)) =#> D#(X) D#(!facminus(X, Y)) =#> D#(Y) D#(minus(X)) =#> D#(X) D#(div(X, Y)) =#> D#(X) D#(div(X, Y)) =#> D#(Y) D#(ln(X)) =#> D#(X) D#(pow(X, Y)) =#> D#(X) D#(pow(X, Y)) =#> D#(Y) map#(F, cons(X, Y)) =#> map#(F, Y) filter#(F, cons(X, Y)) =#> filter2#(F X, F, X, Y) Thus, the original system is terminating if (P_1, R_1, static, formative) is finite. We consider the dependency pair problem (P_1, R_1, static, formative). 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#(!facplus(X, Y)) >? D#(X) D#(!facplus(X, Y)) >? D#(Y) D#(!factimes(X, Y)) >? D#(X) D#(!factimes(X, Y)) >? D#(Y) D#(!facminus(X, Y)) >? D#(X) D#(!facminus(X, Y)) >? D#(Y) D#(minus(X)) >? D#(X) D#(div(X, Y)) >? D#(X) D#(div(X, Y)) >? D#(Y) D#(ln(X)) >? D#(X) D#(pow(X, Y)) >? D#(X) D#(pow(X, Y)) >? D#(Y) map#(F, cons(X, Y)) >? map#(F, Y) filter#(F, cons(X, Y)) >? filter2#(F X, F, X, Y) D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) D(minus(X)) >= minus(D(X)) D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) D(ln(X)) >= div(D(X), X) D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) map(F, cons(X, Y)) >= cons(F X, map(F, Y)) filter(F, cons(X, Y)) >= filter2(F X, F, X, Y) filter2(true, F, X, Y) >= cons(X, filter(F, Y)) filter2(false, F, X, Y) >= filter(F, Y) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: !facminus = \y0y1.0 !facplus = \y0y1.3 !factimes = \y0y1.0 1 = 0 2 = 0 D = \y0.3 + 2y0 D# = \y0.0 cons = \y0y1.0 div = \y0y1.0 false = 3 filter = \G0y1.0 filter2 = \y0G1y2y3.0 filter2# = \y0G1y2y3.0 filter# = \G0y1.3 ln = \y0.0 map = \G0y1.2G0(0) map# = \G0y1.0 minus = \y0.0 pow = \y0y1.0 true = 3 Using this interpretation, the requirements translate to: [[D#(!facplus(_x0, _x1))]] = 0 >= 0 = [[D#(_x0)]] [[D#(!facplus(_x0, _x1))]] = 0 >= 0 = [[D#(_x1)]] [[D#(!factimes(_x0, _x1))]] = 0 >= 0 = [[D#(_x0)]] [[D#(!factimes(_x0, _x1))]] = 0 >= 0 = [[D#(_x1)]] [[D#(!facminus(_x0, _x1))]] = 0 >= 0 = [[D#(_x0)]] [[D#(!facminus(_x0, _x1))]] = 0 >= 0 = [[D#(_x1)]] [[D#(minus(_x0))]] = 0 >= 0 = [[D#(_x0)]] [[D#(div(_x0, _x1))]] = 0 >= 0 = [[D#(_x0)]] [[D#(div(_x0, _x1))]] = 0 >= 0 = [[D#(_x1)]] [[D#(ln(_x0))]] = 0 >= 0 = [[D#(_x0)]] [[D#(pow(_x0, _x1))]] = 0 >= 0 = [[D#(_x0)]] [[D#(pow(_x0, _x1))]] = 0 >= 0 = [[D#(_x1)]] [[map#(_F0, cons(_x1, _x2))]] = 0 >= 0 = [[map#(_F0, _x2)]] [[filter#(_F0, cons(_x1, _x2))]] = 3 > 0 = [[filter2#(_F0 _x1, _F0, _x1, _x2)]] [[D(!facplus(_x0, _x1))]] = 9 >= 3 = [[!facplus(D(_x0), D(_x1))]] [[D(!factimes(_x0, _x1))]] = 3 >= 3 = [[!facplus(!factimes(_x1, D(_x0)), !factimes(_x0, D(_x1)))]] [[D(!facminus(_x0, _x1))]] = 3 >= 0 = [[!facminus(D(_x0), D(_x1))]] [[D(minus(_x0))]] = 3 >= 0 = [[minus(D(_x0))]] [[D(div(_x0, _x1))]] = 3 >= 0 = [[!facminus(div(D(_x0), _x1), div(!factimes(_x0, D(_x1)), pow(_x1, 2)))]] [[D(ln(_x0))]] = 3 >= 0 = [[div(D(_x0), _x0)]] [[D(pow(_x0, _x1))]] = 3 >= 3 = [[!facplus(!factimes(!factimes(_x1, pow(_x0, !facminus(_x1, 1))), D(_x0)), !factimes(!factimes(pow(_x0, _x1), ln(_x0)), D(_x1)))]] [[map(_F0, cons(_x1, _x2))]] = 2F0(0) >= 0 = [[cons(_F0 _x1, map(_F0, _x2))]] [[filter(_F0, cons(_x1, _x2))]] = 0 >= 0 = [[filter2(_F0 _x1, _F0, _x1, _x2)]] [[filter2(true, _F0, _x1, _x2)]] = 0 >= 0 = [[cons(_x1, filter(_F0, _x2))]] [[filter2(false, _F0, _x1, _x2)]] = 0 >= 0 = [[filter(_F0, _x2)]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_1, R_1, static, formative) by (P_2, R_1, static, formative), where P_2 consists of: D#(!facplus(X, Y)) =#> D#(X) D#(!facplus(X, Y)) =#> D#(Y) D#(!factimes(X, Y)) =#> D#(X) D#(!factimes(X, Y)) =#> D#(Y) D#(!facminus(X, Y)) =#> D#(X) D#(!facminus(X, Y)) =#> D#(Y) D#(minus(X)) =#> D#(X) D#(div(X, Y)) =#> D#(X) D#(div(X, Y)) =#> D#(Y) D#(ln(X)) =#> D#(X) D#(pow(X, Y)) =#> D#(X) D#(pow(X, Y)) =#> D#(Y) map#(F, cons(X, Y)) =#> map#(F, Y) Thus, the original system is terminating if (P_2, R_1, static, formative) is finite. We consider the dependency pair problem (P_2, R_1, static, formative). 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#(!facplus(X, Y)) >? D#(X) D#(!facplus(X, Y)) >? D#(Y) D#(!factimes(X, Y)) >? D#(X) D#(!factimes(X, Y)) >? D#(Y) D#(!facminus(X, Y)) >? D#(X) D#(!facminus(X, Y)) >? D#(Y) D#(minus(X)) >? D#(X) D#(div(X, Y)) >? D#(X) D#(div(X, Y)) >? D#(Y) D#(ln(X)) >? D#(X) D#(pow(X, Y)) >? D#(X) D#(pow(X, Y)) >? D#(Y) map#(F, cons(X, Y)) >? map#(F, Y) D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) D(minus(X)) >= minus(D(X)) D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) D(ln(X)) >= div(D(X), X) D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) map(F, cons(X, Y)) >= cons(F X, map(F, Y)) filter(F, cons(X, Y)) >= filter2(F X, F, X, Y) filter2(true, F, X, Y) >= cons(X, filter(F, Y)) filter2(false, F, X, Y) >= filter(F, Y) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: !facminus = \y0y1.0 !facplus = \y0y1.0 !factimes = \y0y1.0 1 = 0 2 = 0 D = \y0.0 D# = \y0.0 cons = \y0y1.2 + y0 + y1 div = \y0y1.0 false = 3 filter = \G0y1.y1 filter2 = \y0G1y2y3.2 + y2 + y3 ln = \y0.0 map = \G0y1.y1 + y1G0(y1) map# = \G0y1.y1 minus = \y0.0 pow = \y0y1.0 true = 3 Using this interpretation, the requirements translate to: [[D#(!facplus(_x0, _x1))]] = 0 >= 0 = [[D#(_x0)]] [[D#(!facplus(_x0, _x1))]] = 0 >= 0 = [[D#(_x1)]] [[D#(!factimes(_x0, _x1))]] = 0 >= 0 = [[D#(_x0)]] [[D#(!factimes(_x0, _x1))]] = 0 >= 0 = [[D#(_x1)]] [[D#(!facminus(_x0, _x1))]] = 0 >= 0 = [[D#(_x0)]] [[D#(!facminus(_x0, _x1))]] = 0 >= 0 = [[D#(_x1)]] [[D#(minus(_x0))]] = 0 >= 0 = [[D#(_x0)]] [[D#(div(_x0, _x1))]] = 0 >= 0 = [[D#(_x0)]] [[D#(div(_x0, _x1))]] = 0 >= 0 = [[D#(_x1)]] [[D#(ln(_x0))]] = 0 >= 0 = [[D#(_x0)]] [[D#(pow(_x0, _x1))]] = 0 >= 0 = [[D#(_x0)]] [[D#(pow(_x0, _x1))]] = 0 >= 0 = [[D#(_x1)]] [[map#(_F0, cons(_x1, _x2))]] = 2 + x1 + x2 > x2 = [[map#(_F0, _x2)]] [[D(!facplus(_x0, _x1))]] = 0 >= 0 = [[!facplus(D(_x0), D(_x1))]] [[D(!factimes(_x0, _x1))]] = 0 >= 0 = [[!facplus(!factimes(_x1, D(_x0)), !factimes(_x0, D(_x1)))]] [[D(!facminus(_x0, _x1))]] = 0 >= 0 = [[!facminus(D(_x0), D(_x1))]] [[D(minus(_x0))]] = 0 >= 0 = [[minus(D(_x0))]] [[D(div(_x0, _x1))]] = 0 >= 0 = [[!facminus(div(D(_x0), _x1), div(!factimes(_x0, D(_x1)), pow(_x1, 2)))]] [[D(ln(_x0))]] = 0 >= 0 = [[div(D(_x0), _x0)]] [[D(pow(_x0, _x1))]] = 0 >= 0 = [[!facplus(!factimes(!factimes(_x1, pow(_x0, !facminus(_x1, 1))), D(_x0)), !factimes(!factimes(pow(_x0, _x1), ln(_x0)), D(_x1)))]] [[map(_F0, cons(_x1, _x2))]] = 2 + x1 + x2 + 2F0(2 + x1 + x2) + x1F0(2 + x1 + x2) + x2F0(2 + x1 + x2) >= 2 + x2 + F0(x1) + x2F0(x2) = [[cons(_F0 _x1, map(_F0, _x2))]] [[filter(_F0, cons(_x1, _x2))]] = 2 + x1 + x2 >= 2 + x1 + x2 = [[filter2(_F0 _x1, _F0, _x1, _x2)]] [[filter2(true, _F0, _x1, _x2)]] = 2 + x1 + x2 >= 2 + x1 + x2 = [[cons(_x1, filter(_F0, _x2))]] [[filter2(false, _F0, _x1, _x2)]] = 2 + x1 + x2 >= x2 = [[filter(_F0, _x2)]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_2, R_1, static, formative) by (P_3, R_1, static, formative), where P_3 consists of: D#(!facplus(X, Y)) =#> D#(X) D#(!facplus(X, Y)) =#> D#(Y) D#(!factimes(X, Y)) =#> D#(X) D#(!factimes(X, Y)) =#> D#(Y) D#(!facminus(X, Y)) =#> D#(X) D#(!facminus(X, Y)) =#> D#(Y) D#(minus(X)) =#> D#(X) D#(div(X, Y)) =#> D#(X) D#(div(X, Y)) =#> D#(Y) D#(ln(X)) =#> D#(X) D#(pow(X, Y)) =#> D#(X) D#(pow(X, Y)) =#> D#(Y) Thus, the original system is terminating if (P_3, R_1, static, formative) is finite. We consider the dependency pair problem (P_3, R_1, static, formative). The formative rules of (P_3, R_1) are R_2 ::= D(!facplus(X, Y)) => !facplus(D(X), D(Y)) D(!factimes(X, Y)) => !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X, Y)) => !facminus(D(X), D(Y)) D(minus(X)) => minus(D(X)) D(div(X, Y)) => !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) D(ln(X)) => div(D(X), X) D(pow(X, Y)) => !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) By [Kop12, Thm. 7.17], we may replace the dependency pair problem (P_3, R_1, static, formative) by (P_3, R_2, static, formative). Thus, the original system is terminating if (P_3, R_2, static, formative) is finite. We consider the dependency pair problem (P_3, R_2, static, formative). 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#(!facplus(X, Y)) >? D#(X) D#(!facplus(X, Y)) >? D#(Y) D#(!factimes(X, Y)) >? D#(X) D#(!factimes(X, Y)) >? D#(Y) D#(!facminus(X, Y)) >? D#(X) D#(!facminus(X, Y)) >? D#(Y) D#(minus(X)) >? D#(X) D#(div(X, Y)) >? D#(X) D#(div(X, Y)) >? D#(Y) D#(ln(X)) >? D#(X) D#(pow(X, Y)) >? D#(X) D#(pow(X, Y)) >? D#(Y) D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) D(minus(X)) >= minus(D(X)) D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) D(ln(X)) >= div(D(X), X) D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) 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: [[1]] = _|_ [[2]] = _|_ We choose Lex = {} and Mul = {!facminus, !facplus, !factimes, D, D#, div, ln, minus, pow}, and the following precedence: D# > D = minus > !facminus > !facplus > !factimes > pow > div > ln Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: D#(!facplus(X, Y)) >= D#(X) D#(!facplus(X, Y)) >= D#(Y) D#(!factimes(X, Y)) >= D#(X) D#(!factimes(X, Y)) >= D#(Y) D#(!facminus(X, Y)) >= D#(X) D#(!facminus(X, Y)) >= D#(Y) D#(minus(X)) >= D#(X) D#(div(X, Y)) >= D#(X) D#(div(X, Y)) >= D#(Y) D#(ln(X)) >= D#(X) D#(pow(X, Y)) >= D#(X) D#(pow(X, Y)) > D#(Y) D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) D(minus(X)) >= minus(D(X)) D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, _|_))) D(ln(X)) >= div(D(X), X) D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, _|_))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) With these choices, we have: 1] D#(!facplus(X, Y)) >= D#(X) because D# in Mul and [2], by (Fun) 2] !facplus(X, Y) >= X because [3], by (Star) 3] !facplus*(X, Y) >= X because [4], by (Select) 4] X >= X by (Meta) 5] D#(!facplus(X, Y)) >= D#(Y) because D# in Mul and [6], by (Fun) 6] !facplus(X, Y) >= Y because [7], by (Star) 7] !facplus*(X, Y) >= Y because [8], by (Select) 8] Y >= Y by (Meta) 9] D#(!factimes(X, Y)) >= D#(X) because D# in Mul and [10], by (Fun) 10] !factimes(X, Y) >= X because [11], by (Star) 11] !factimes*(X, Y) >= X because [12], by (Select) 12] X >= X by (Meta) 13] D#(!factimes(X, Y)) >= D#(Y) because D# in Mul and [14], by (Fun) 14] !factimes(X, Y) >= Y because [15], by (Star) 15] !factimes*(X, Y) >= Y because [16], by (Select) 16] Y >= Y by (Meta) 17] D#(!facminus(X, Y)) >= D#(X) because D# in Mul and [18], by (Fun) 18] !facminus(X, Y) >= X because [19], by (Star) 19] !facminus*(X, Y) >= X because [20], by (Select) 20] X >= X by (Meta) 21] D#(!facminus(X, Y)) >= D#(Y) because [22], by (Star) 22] D#*(!facminus(X, Y)) >= D#(Y) because D# in Mul and [23], by (Stat) 23] !facminus(X, Y) > Y because [24], by definition 24] !facminus*(X, Y) >= Y because [25], by (Select) 25] Y >= Y by (Meta) 26] D#(minus(X)) >= D#(X) because D# in Mul and [27], by (Fun) 27] minus(X) >= X because [28], by (Star) 28] minus*(X) >= X because [29], by (Select) 29] X >= X by (Meta) 30] D#(div(X, Y)) >= D#(X) because D# in Mul and [31], by (Fun) 31] div(X, Y) >= X because [32], by (Star) 32] div*(X, Y) >= X because [33], by (Select) 33] X >= X by (Meta) 34] D#(div(X, Y)) >= D#(Y) because D# in Mul and [35], by (Fun) 35] div(X, Y) >= Y because [36], by (Star) 36] div*(X, Y) >= Y because [37], by (Select) 37] Y >= Y by (Meta) 38] D#(ln(X)) >= D#(X) because D# in Mul and [39], by (Fun) 39] ln(X) >= X because [40], by (Star) 40] ln*(X) >= X because [41], by (Select) 41] X >= X by (Meta) 42] D#(pow(X, Y)) >= D#(X) because D# in Mul and [43], by (Fun) 43] pow(X, Y) >= X because [44], by (Star) 44] pow*(X, Y) >= X because [45], by (Select) 45] X >= X by (Meta) 46] D#(pow(X, Y)) > D#(Y) because [47], by definition 47] D#*(pow(X, Y)) >= D#(Y) because D# in Mul and [48], by (Stat) 48] pow(X, Y) > Y because [49], by definition 49] pow*(X, Y) >= Y because [50], by (Select) 50] Y >= Y by (Meta) 51] D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) because [52], by (Star) 52] D*(!facplus(X, Y)) >= !facplus(D(X), D(Y)) because D > !facplus, [53] and [56], by (Copy) 53] D*(!facplus(X, Y)) >= D(X) because D in Mul and [54], by (Stat) 54] !facplus(X, Y) > X because [55], by definition 55] !facplus*(X, Y) >= X because [4], by (Select) 56] D*(!facplus(X, Y)) >= D(Y) because D in Mul and [57], by (Stat) 57] !facplus(X, Y) > Y because [58], by definition 58] !facplus*(X, Y) >= Y because [8], by (Select) 59] D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) because [60], by (Star) 60] D*(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) because D > !facplus, [61] and [66], by (Copy) 61] D*(!factimes(X, Y)) >= !factimes(Y, D(X)) because D > !factimes, [62] and [63], by (Copy) 62] D*(!factimes(X, Y)) >= Y because [14], by (Select) 63] D*(!factimes(X, Y)) >= D(X) because D in Mul and [64], by (Stat) 64] !factimes(X, Y) > X because [65], by definition 65] !factimes*(X, Y) >= X because [12], by (Select) 66] D*(!factimes(X, Y)) >= !factimes(X, D(Y)) because D > !factimes, [67] and [68], by (Copy) 67] D*(!factimes(X, Y)) >= X because [10], by (Select) 68] D*(!factimes(X, Y)) >= D(Y) because D in Mul and [69], by (Stat) 69] !factimes(X, Y) > Y because [70], by definition 70] !factimes*(X, Y) >= Y because [16], by (Select) 71] D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) because [72], by (Star) 72] D*(!facminus(X, Y)) >= !facminus(D(X), D(Y)) because D > !facminus, [73] and [76], by (Copy) 73] D*(!facminus(X, Y)) >= D(X) because D in Mul and [74], by (Stat) 74] !facminus(X, Y) > X because [75], by definition 75] !facminus*(X, Y) >= X because [20], by (Select) 76] D*(!facminus(X, Y)) >= D(Y) because D in Mul and [23], by (Stat) 77] D(minus(X)) >= minus(D(X)) because D = minus, D in Mul and [78], by (Fun) 78] minus(X) >= D(X) because minus = D, minus in Mul and [79], by (Fun) 79] X >= X by (Meta) 80] D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, _|_))) because [81], by (Star) 81] D*(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, _|_))) because D > !facminus, [82] and [87], by (Copy) 82] D*(div(X, Y)) >= div(D(X), Y) because D > div, [83] and [86], by (Copy) 83] D*(div(X, Y)) >= D(X) because D in Mul and [84], by (Stat) 84] div(X, Y) > X because [85], by definition 85] div*(X, Y) >= X because [33], by (Select) 86] D*(div(X, Y)) >= Y because [35], by (Select) 87] D*(div(X, Y)) >= div(!factimes(X, D(Y)), pow(Y, _|_)) because D > div, [88] and [93], by (Copy) 88] D*(div(X, Y)) >= !factimes(X, D(Y)) because D > !factimes, [89] and [90], by (Copy) 89] D*(div(X, Y)) >= X because [31], by (Select) 90] D*(div(X, Y)) >= D(Y) because D in Mul and [91], by (Stat) 91] div(X, Y) > Y because [92], by definition 92] div*(X, Y) >= Y because [37], by (Select) 93] D*(div(X, Y)) >= pow(Y, _|_) because D > pow, [86] and [94], by (Copy) 94] D*(div(X, Y)) >= _|_ by (Bot) 95] D(ln(X)) >= div(D(X), X) because [96], by (Star) 96] D*(ln(X)) >= div(D(X), X) because D > div, [97] and [100], by (Copy) 97] D*(ln(X)) >= D(X) because D in Mul and [98], by (Stat) 98] ln(X) > X because [99], by definition 99] ln*(X) >= X because [41], by (Select) 100] D*(ln(X)) >= X because [39], by (Select) 101] D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, _|_))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) because [102], by (Star) 102] D*(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, _|_))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) because D > !facplus, [103] and [114], by (Copy) 103] D*(pow(X, Y)) >= !factimes(!factimes(Y, pow(X, !facminus(Y, _|_))), D(X)) because D > !factimes, [104] and [111], by (Copy) 104] D*(pow(X, Y)) >= !factimes(Y, pow(X, !facminus(Y, _|_))) because D > !factimes, [105] and [107], by (Copy) 105] D*(pow(X, Y)) >= Y because [106], by (Select) 106] pow(X, Y) >= Y because [49], by (Star) 107] D*(pow(X, Y)) >= pow(X, !facminus(Y, _|_)) because D > pow, [108] and [109], by (Copy) 108] D*(pow(X, Y)) >= X because [43], by (Select) 109] D*(pow(X, Y)) >= !facminus(Y, _|_) because D > !facminus, [105] and [110], by (Copy) 110] D*(pow(X, Y)) >= _|_ by (Bot) 111] D*(pow(X, Y)) >= D(X) because D in Mul and [112], by (Stat) 112] pow(X, Y) > X because [113], by definition 113] pow*(X, Y) >= X because [45], by (Select) 114] D*(pow(X, Y)) >= !factimes(!factimes(pow(X, Y), ln(X)), D(Y)) because D > !factimes, [115] and [120], by (Copy) 115] D*(pow(X, Y)) >= !factimes(pow(X, Y), ln(X)) because D > !factimes, [116] and [117], by (Copy) 116] D*(pow(X, Y)) >= pow(X, Y) because D > pow, [108] and [105], by (Copy) 117] D*(pow(X, Y)) >= ln(X) because [118], by (Select) 118] pow(X, Y) >= ln(X) because [119], by (Star) 119] pow*(X, Y) >= ln(X) because pow > ln and [113], by (Copy) 120] D*(pow(X, Y)) >= D(Y) because D in Mul and [48], by (Stat) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_3, R_2, static, formative) by (P_4, R_2, static, formative), where P_4 consists of: D#(!facplus(X, Y)) =#> D#(X) D#(!facplus(X, Y)) =#> D#(Y) D#(!factimes(X, Y)) =#> D#(X) D#(!factimes(X, Y)) =#> D#(Y) D#(!facminus(X, Y)) =#> D#(X) D#(!facminus(X, Y)) =#> D#(Y) D#(minus(X)) =#> D#(X) D#(div(X, Y)) =#> D#(X) D#(div(X, Y)) =#> D#(Y) D#(ln(X)) =#> D#(X) D#(pow(X, Y)) =#> D#(X) Thus, the original system is terminating if (P_4, R_2, static, formative) is finite. We consider the dependency pair problem (P_4, R_2, static, formative). 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#(!facplus(X, Y)) >? D#(X) D#(!facplus(X, Y)) >? D#(Y) D#(!factimes(X, Y)) >? D#(X) D#(!factimes(X, Y)) >? D#(Y) D#(!facminus(X, Y)) >? D#(X) D#(!facminus(X, Y)) >? D#(Y) D#(minus(X)) >? D#(X) D#(div(X, Y)) >? D#(X) D#(div(X, Y)) >? D#(Y) D#(ln(X)) >? D#(X) D#(pow(X, Y)) >? D#(X) D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) D(minus(X)) >= minus(D(X)) D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) D(ln(X)) >= div(D(X), X) D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) 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: [[1]] = _|_ [[2]] = _|_ We choose Lex = {} and Mul = {!facminus, !facplus, !factimes, D, D#, div, ln, minus, pow}, and the following precedence: D = ln > !facminus > !facplus = D# > pow > !factimes > div > minus Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: D#(!facplus(X, Y)) >= D#(X) D#(!facplus(X, Y)) >= D#(Y) D#(!factimes(X, Y)) >= D#(X) D#(!factimes(X, Y)) >= D#(Y) D#(!facminus(X, Y)) >= D#(X) D#(!facminus(X, Y)) > D#(Y) D#(minus(X)) >= D#(X) D#(div(X, Y)) >= D#(X) D#(div(X, Y)) >= D#(Y) D#(ln(X)) >= D#(X) D#(pow(X, Y)) >= D#(X) D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) D(minus(X)) >= minus(D(X)) D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, _|_))) D(ln(X)) >= div(D(X), X) D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, _|_))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) With these choices, we have: 1] D#(!facplus(X, Y)) >= D#(X) because D# in Mul and [2], by (Fun) 2] !facplus(X, Y) >= X because [3], by (Star) 3] !facplus*(X, Y) >= X because [4], by (Select) 4] X >= X by (Meta) 5] D#(!facplus(X, Y)) >= D#(Y) because [6], by (Star) 6] D#*(!facplus(X, Y)) >= D#(Y) because [7], by (Select) 7] !facplus(X, Y) >= D#(Y) because [8], by (Star) 8] !facplus*(X, Y) >= D#(Y) because !facplus = D#, !facplus in Mul and [9], by (Stat) 9] Y >= Y by (Meta) 10] D#(!factimes(X, Y)) >= D#(X) because [11], by (Star) 11] D#*(!factimes(X, Y)) >= D#(X) because D# in Mul and [12], by (Stat) 12] !factimes(X, Y) > X because [13], by definition 13] !factimes*(X, Y) >= X because [14], by (Select) 14] X >= X by (Meta) 15] D#(!factimes(X, Y)) >= D#(Y) because [16], by (Star) 16] D#*(!factimes(X, Y)) >= D#(Y) because D# in Mul and [17], by (Stat) 17] !factimes(X, Y) > Y because [18], by definition 18] !factimes*(X, Y) >= Y because [19], by (Select) 19] Y >= Y by (Meta) 20] D#(!facminus(X, Y)) >= D#(X) because [21], by (Star) 21] D#*(!facminus(X, Y)) >= D#(X) because [22], by (Select) 22] !facminus(X, Y) >= D#(X) because [23], by (Star) 23] !facminus*(X, Y) >= D#(X) because !facminus > D# and [24], by (Copy) 24] !facminus*(X, Y) >= X because [25], by (Select) 25] X >= X by (Meta) 26] D#(!facminus(X, Y)) > D#(Y) because [27], by definition 27] D#*(!facminus(X, Y)) >= D#(Y) because D# in Mul and [28], by (Stat) 28] !facminus(X, Y) > Y because [29], by definition 29] !facminus*(X, Y) >= Y because [30], by (Select) 30] Y >= Y by (Meta) 31] D#(minus(X)) >= D#(X) because D# in Mul and [32], by (Fun) 32] minus(X) >= X because [33], by (Star) 33] minus*(X) >= X because [34], by (Select) 34] X >= X by (Meta) 35] D#(div(X, Y)) >= D#(X) because D# in Mul and [36], by (Fun) 36] div(X, Y) >= X because [37], by (Star) 37] div*(X, Y) >= X because [38], by (Select) 38] X >= X by (Meta) 39] D#(div(X, Y)) >= D#(Y) because D# in Mul and [40], by (Fun) 40] div(X, Y) >= Y because [41], by (Star) 41] div*(X, Y) >= Y because [42], by (Select) 42] Y >= Y by (Meta) 43] D#(ln(X)) >= D#(X) because D# in Mul and [44], by (Fun) 44] ln(X) >= X because [45], by (Star) 45] ln*(X) >= X because [46], by (Select) 46] X >= X by (Meta) 47] D#(pow(X, Y)) >= D#(X) because D# in Mul and [48], by (Fun) 48] pow(X, Y) >= X because [49], by (Star) 49] pow*(X, Y) >= X because [50], by (Select) 50] X >= X by (Meta) 51] D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) because [52], by (Star) 52] D*(!facplus(X, Y)) >= !facplus(D(X), D(Y)) because D > !facplus, [53] and [56], by (Copy) 53] D*(!facplus(X, Y)) >= D(X) because D in Mul and [54], by (Stat) 54] !facplus(X, Y) > X because [55], by definition 55] !facplus*(X, Y) >= X because [4], by (Select) 56] D*(!facplus(X, Y)) >= D(Y) because D in Mul and [57], by (Stat) 57] !facplus(X, Y) > Y because [58], by definition 58] !facplus*(X, Y) >= Y because [9], by (Select) 59] D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) because [60], by (Star) 60] D*(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) because D > !facplus, [61] and [65], by (Copy) 61] D*(!factimes(X, Y)) >= !factimes(Y, D(X)) because D > !factimes, [62] and [64], by (Copy) 62] D*(!factimes(X, Y)) >= Y because [63], by (Select) 63] !factimes(X, Y) >= Y because [18], by (Star) 64] D*(!factimes(X, Y)) >= D(X) because D in Mul and [12], by (Stat) 65] D*(!factimes(X, Y)) >= !factimes(X, D(Y)) because D > !factimes, [66] and [68], by (Copy) 66] D*(!factimes(X, Y)) >= X because [67], by (Select) 67] !factimes(X, Y) >= X because [13], by (Star) 68] D*(!factimes(X, Y)) >= D(Y) because D in Mul and [17], by (Stat) 69] D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) because [70], by (Star) 70] D*(!facminus(X, Y)) >= !facminus(D(X), D(Y)) because D > !facminus, [71] and [73], by (Copy) 71] D*(!facminus(X, Y)) >= D(X) because D in Mul and [72], by (Stat) 72] !facminus(X, Y) > X because [24], by definition 73] D*(!facminus(X, Y)) >= D(Y) because D in Mul and [28], by (Stat) 74] D(minus(X)) >= minus(D(X)) because [75], by (Star) 75] D*(minus(X)) >= minus(D(X)) because D > minus and [76], by (Copy) 76] D*(minus(X)) >= D(X) because D in Mul and [77], by (Stat) 77] minus(X) > X because [78], by definition 78] minus*(X) >= X because [34], by (Select) 79] D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, _|_))) because [80], by (Star) 80] D*(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, _|_))) because D > !facminus, [81] and [86], by (Copy) 81] D*(div(X, Y)) >= div(D(X), Y) because D > div, [82] and [85], by (Copy) 82] D*(div(X, Y)) >= D(X) because D in Mul and [83], by (Stat) 83] div(X, Y) > X because [84], by definition 84] div*(X, Y) >= X because [38], by (Select) 85] D*(div(X, Y)) >= Y because [40], by (Select) 86] D*(div(X, Y)) >= div(!factimes(X, D(Y)), pow(Y, _|_)) because D > div, [87] and [92], by (Copy) 87] D*(div(X, Y)) >= !factimes(X, D(Y)) because D > !factimes, [88] and [89], by (Copy) 88] D*(div(X, Y)) >= X because [36], by (Select) 89] D*(div(X, Y)) >= D(Y) because D in Mul and [90], by (Stat) 90] div(X, Y) > Y because [91], by definition 91] div*(X, Y) >= Y because [42], by (Select) 92] D*(div(X, Y)) >= pow(Y, _|_) because D > pow, [85] and [93], by (Copy) 93] D*(div(X, Y)) >= _|_ by (Bot) 94] D(ln(X)) >= div(D(X), X) because [95], by (Star) 95] D*(ln(X)) >= div(D(X), X) because D > div, [96] and [99], by (Copy) 96] D*(ln(X)) >= D(X) because [97], by (Select) 97] ln(X) >= D(X) because ln = D, ln in Mul and [98], by (Fun) 98] X >= X by (Meta) 99] D*(ln(X)) >= X because [44], by (Select) 100] D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, _|_))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) because [101], by (Star) 101] D*(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, _|_))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) because D > !facplus, [102] and [115], by (Copy) 102] D*(pow(X, Y)) >= !factimes(!factimes(Y, pow(X, !facminus(Y, _|_))), D(X)) because D > !factimes, [103] and [112], by (Copy) 103] D*(pow(X, Y)) >= !factimes(Y, pow(X, !facminus(Y, _|_))) because D > !factimes, [104] and [108], by (Copy) 104] D*(pow(X, Y)) >= Y because [105], by (Select) 105] pow(X, Y) >= Y because [106], by (Star) 106] pow*(X, Y) >= Y because [107], by (Select) 107] Y >= Y by (Meta) 108] D*(pow(X, Y)) >= pow(X, !facminus(Y, _|_)) because D > pow, [109] and [110], by (Copy) 109] D*(pow(X, Y)) >= X because [48], by (Select) 110] D*(pow(X, Y)) >= !facminus(Y, _|_) because D > !facminus, [104] and [111], by (Copy) 111] D*(pow(X, Y)) >= _|_ by (Bot) 112] D*(pow(X, Y)) >= D(X) because D in Mul and [113], by (Stat) 113] pow(X, Y) > X because [114], by definition 114] pow*(X, Y) >= X because [50], by (Select) 115] D*(pow(X, Y)) >= !factimes(!factimes(pow(X, Y), ln(X)), D(Y)) because D > !factimes, [116] and [122], by (Copy) 116] D*(pow(X, Y)) >= !factimes(pow(X, Y), ln(X)) because D > !factimes, [117] and [121], by (Copy) 117] D*(pow(X, Y)) >= pow(X, Y) because [118], by (Select) 118] pow(X, Y) >= pow(X, Y) because pow in Mul, [119] and [120], by (Fun) 119] X >= X by (Meta) 120] Y >= Y by (Meta) 121] D*(pow(X, Y)) >= ln(X) because D = ln, D in Mul and [113], by (Stat) 122] D*(pow(X, Y)) >= D(Y) because D in Mul and [123], by (Stat) 123] pow(X, Y) > Y because [124], by definition 124] pow*(X, Y) >= Y because [120], by (Select) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_4, R_2, static, formative) by (P_5, R_2, static, formative), where P_5 consists of: D#(!facplus(X, Y)) =#> D#(X) D#(!facplus(X, Y)) =#> D#(Y) D#(!factimes(X, Y)) =#> D#(X) D#(!factimes(X, Y)) =#> D#(Y) D#(!facminus(X, Y)) =#> D#(X) D#(minus(X)) =#> D#(X) D#(div(X, Y)) =#> D#(X) D#(div(X, Y)) =#> D#(Y) D#(ln(X)) =#> D#(X) D#(pow(X, Y)) =#> D#(X) Thus, the original system is terminating if (P_5, R_2, static, formative) is finite. We consider the dependency pair problem (P_5, R_2, static, formative). 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#(!facplus(X, Y)) >? D#(X) D#(!facplus(X, Y)) >? D#(Y) D#(!factimes(X, Y)) >? D#(X) D#(!factimes(X, Y)) >? D#(Y) D#(!facminus(X, Y)) >? D#(X) D#(minus(X)) >? D#(X) D#(div(X, Y)) >? D#(X) D#(div(X, Y)) >? D#(Y) D#(ln(X)) >? D#(X) D#(pow(X, Y)) >? D#(X) D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) D(minus(X)) >= minus(D(X)) D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) D(ln(X)) >= div(D(X), X) D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) 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: [[!facminus(x_1, x_2)]] = x_1 [[1]] = _|_ [[2]] = _|_ We choose Lex = {} and Mul = {!facplus, !factimes, D, D#, div, ln, minus, pow}, and the following precedence: pow > D# > ln > D = minus > div > !factimes > !facplus Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: D#(!facplus(X, Y)) >= D#(X) D#(!facplus(X, Y)) >= D#(Y) D#(!factimes(X, Y)) > D#(X) D#(!factimes(X, Y)) >= D#(Y) D#(X) >= D#(X) D#(minus(X)) >= D#(X) D#(div(X, Y)) >= D#(X) D#(div(X, Y)) >= D#(Y) D#(ln(X)) >= D#(X) D#(pow(X, Y)) >= D#(X) D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(X) >= D(X) D(minus(X)) >= minus(D(X)) D(div(X, Y)) >= div(D(X), Y) D(ln(X)) >= div(D(X), X) D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, Y)), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) With these choices, we have: 1] D#(!facplus(X, Y)) >= D#(X) because D# in Mul and [2], by (Fun) 2] !facplus(X, Y) >= X because [3], by (Star) 3] !facplus*(X, Y) >= X because [4], by (Select) 4] X >= X by (Meta) 5] D#(!facplus(X, Y)) >= D#(Y) because D# in Mul and [6], by (Fun) 6] !facplus(X, Y) >= Y because [7], by (Star) 7] !facplus*(X, Y) >= Y because [8], by (Select) 8] Y >= Y by (Meta) 9] D#(!factimes(X, Y)) > D#(X) because [10], by definition 10] D#*(!factimes(X, Y)) >= D#(X) because D# in Mul and [11], by (Stat) 11] !factimes(X, Y) > X because [12], by definition 12] !factimes*(X, Y) >= X because [13], by (Select) 13] X >= X by (Meta) 14] D#(!factimes(X, Y)) >= D#(Y) because D# in Mul and [15], by (Fun) 15] !factimes(X, Y) >= Y because [16], by (Star) 16] !factimes*(X, Y) >= Y because [17], by (Select) 17] Y >= Y by (Meta) 18] D#(X) >= D#(X) because D# in Mul and [19], by (Fun) 19] X >= X by (Meta) 20] D#(minus(X)) >= D#(X) because D# in Mul and [21], by (Fun) 21] minus(X) >= X because [22], by (Star) 22] minus*(X) >= X because [23], by (Select) 23] X >= X by (Meta) 24] D#(div(X, Y)) >= D#(X) because D# in Mul and [25], by (Fun) 25] div(X, Y) >= X because [26], by (Star) 26] div*(X, Y) >= X because [27], by (Select) 27] X >= X by (Meta) 28] D#(div(X, Y)) >= D#(Y) because D# in Mul and [29], by (Fun) 29] div(X, Y) >= Y because [30], by (Star) 30] div*(X, Y) >= Y because [31], by (Select) 31] Y >= Y by (Meta) 32] D#(ln(X)) >= D#(X) because D# in Mul and [33], by (Fun) 33] ln(X) >= X because [34], by (Star) 34] ln*(X) >= X because [35], by (Select) 35] X >= X by (Meta) 36] D#(pow(X, Y)) >= D#(X) because D# in Mul and [37], by (Fun) 37] pow(X, Y) >= X because [38], by (Star) 38] pow*(X, Y) >= X because [39], by (Select) 39] X >= X by (Meta) 40] D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) because [41], by (Star) 41] D*(!facplus(X, Y)) >= !facplus(D(X), D(Y)) because D > !facplus, [42] and [45], by (Copy) 42] D*(!facplus(X, Y)) >= D(X) because D in Mul and [43], by (Stat) 43] !facplus(X, Y) > X because [44], by definition 44] !facplus*(X, Y) >= X because [4], by (Select) 45] D*(!facplus(X, Y)) >= D(Y) because D in Mul and [46], by (Stat) 46] !facplus(X, Y) > Y because [47], by definition 47] !facplus*(X, Y) >= Y because [8], by (Select) 48] D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) because [49], by (Star) 49] D*(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) because D > !facplus, [50] and [53], by (Copy) 50] D*(!factimes(X, Y)) >= !factimes(Y, D(X)) because D > !factimes, [51] and [52], by (Copy) 51] D*(!factimes(X, Y)) >= Y because [15], by (Select) 52] D*(!factimes(X, Y)) >= D(X) because D in Mul and [11], by (Stat) 53] D*(!factimes(X, Y)) >= !factimes(X, D(Y)) because D > !factimes, [54] and [56], by (Copy) 54] D*(!factimes(X, Y)) >= X because [55], by (Select) 55] !factimes(X, Y) >= X because [12], by (Star) 56] D*(!factimes(X, Y)) >= D(Y) because D in Mul and [57], by (Stat) 57] !factimes(X, Y) > Y because [58], by definition 58] !factimes*(X, Y) >= Y because [17], by (Select) 59] D(X) >= D(X) because D in Mul and [19], by (Fun) 60] D(minus(X)) >= minus(D(X)) because D = minus, D in Mul and [61], by (Fun) 61] minus(X) >= D(X) because minus = D, minus in Mul and [62], by (Fun) 62] X >= X by (Meta) 63] D(div(X, Y)) >= div(D(X), Y) because [64], by (Star) 64] D*(div(X, Y)) >= div(D(X), Y) because D > div, [65] and [68], by (Copy) 65] D*(div(X, Y)) >= D(X) because D in Mul and [66], by (Stat) 66] div(X, Y) > X because [67], by definition 67] div*(X, Y) >= X because [27], by (Select) 68] D*(div(X, Y)) >= Y because [29], by (Select) 69] D(ln(X)) >= div(D(X), X) because [70], by (Star) 70] D*(ln(X)) >= div(D(X), X) because D > div, [71] and [74], by (Copy) 71] D*(ln(X)) >= D(X) because D in Mul and [72], by (Stat) 72] ln(X) > X because [73], by definition 73] ln*(X) >= X because [35], by (Select) 74] D*(ln(X)) >= X because [33], by (Select) 75] D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, Y)), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) because [76], by (Star) 76] D*(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, Y)), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) because D > !facplus, [77] and [90], by (Copy) 77] D*(pow(X, Y)) >= !factimes(!factimes(Y, pow(X, Y)), D(X)) because D > !factimes, [78] and [87], by (Copy) 78] D*(pow(X, Y)) >= !factimes(Y, pow(X, Y)) because D > !factimes, [79] and [83], by (Copy) 79] D*(pow(X, Y)) >= Y because [80], by (Select) 80] pow(X, Y) >= Y because [81], by (Star) 81] pow*(X, Y) >= Y because [82], by (Select) 82] Y >= Y by (Meta) 83] D*(pow(X, Y)) >= pow(X, Y) because [84], by (Select) 84] pow(X, Y) >= pow(X, Y) because pow in Mul, [85] and [86], by (Fun) 85] X >= X by (Meta) 86] Y >= Y by (Meta) 87] D*(pow(X, Y)) >= D(X) because D in Mul and [88], by (Stat) 88] pow(X, Y) > X because [89], by definition 89] pow*(X, Y) >= X because [85], by (Select) 90] D*(pow(X, Y)) >= !factimes(!factimes(pow(X, Y), ln(X)), D(Y)) because D > !factimes, [91] and [97], by (Copy) 91] D*(pow(X, Y)) >= !factimes(pow(X, Y), ln(X)) because D > !factimes, [92] and [94], by (Copy) 92] D*(pow(X, Y)) >= pow(X, Y) because [93], by (Select) 93] pow(X, Y) >= pow(X, Y) because pow in Mul, [85] and [86], by (Fun) 94] D*(pow(X, Y)) >= ln(X) because [95], by (Select) 95] pow(X, Y) >= ln(X) because [96], by (Star) 96] pow*(X, Y) >= ln(X) because pow > ln and [89], by (Copy) 97] D*(pow(X, Y)) >= D(Y) because [98], by (Select) 98] pow(X, Y) >= D(Y) because [99], by (Star) 99] pow*(X, Y) >= D(Y) because pow > D and [100], by (Copy) 100] pow*(X, Y) >= Y because [86], by (Select) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_5, R_2, static, formative) by (P_6, R_2, static, formative), where P_6 consists of: D#(!facplus(X, Y)) =#> D#(X) D#(!facplus(X, Y)) =#> D#(Y) D#(!factimes(X, Y)) =#> D#(Y) D#(!facminus(X, Y)) =#> D#(X) D#(minus(X)) =#> D#(X) D#(div(X, Y)) =#> D#(X) D#(div(X, Y)) =#> D#(Y) D#(ln(X)) =#> D#(X) D#(pow(X, Y)) =#> D#(X) Thus, the original system is terminating if (P_6, R_2, static, formative) is finite. We consider the dependency pair problem (P_6, R_2, static, formative). 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#(!facplus(X, Y)) >? D#(X) D#(!facplus(X, Y)) >? D#(Y) D#(!factimes(X, Y)) >? D#(Y) D#(!facminus(X, Y)) >? D#(X) D#(minus(X)) >? D#(X) D#(div(X, Y)) >? D#(X) D#(div(X, Y)) >? D#(Y) D#(ln(X)) >? D#(X) D#(pow(X, Y)) >? D#(X) D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) D(minus(X)) >= minus(D(X)) D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) D(ln(X)) >= div(D(X), X) D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) 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: [[1]] = _|_ [[2]] = _|_ [[minus(x_1)]] = x_1 We choose Lex = {} and Mul = {!facminus, !facplus, !factimes, D, D#, div, ln, pow}, and the following precedence: D > !facplus > !factimes > div > ln > pow > !facminus > D# Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: D#(!facplus(X, Y)) >= D#(X) D#(!facplus(X, Y)) >= D#(Y) D#(!factimes(X, Y)) >= D#(Y) D#(!facminus(X, Y)) >= D#(X) D#(X) >= D#(X) D#(div(X, Y)) >= D#(X) D#(div(X, Y)) >= D#(Y) D#(ln(X)) >= D#(X) D#(pow(X, Y)) > D#(X) D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) D(X) >= D(X) D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, _|_))) D(ln(X)) >= div(D(X), X) D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, _|_))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) With these choices, we have: 1] D#(!facplus(X, Y)) >= D#(X) because D# in Mul and [2], by (Fun) 2] !facplus(X, Y) >= X because [3], by (Star) 3] !facplus*(X, Y) >= X because [4], by (Select) 4] X >= X by (Meta) 5] D#(!facplus(X, Y)) >= D#(Y) because [6], by (Star) 6] D#*(!facplus(X, Y)) >= D#(Y) because [7], by (Select) 7] !facplus(X, Y) >= D#(Y) because [8], by (Star) 8] !facplus*(X, Y) >= D#(Y) because !facplus > D# and [9], by (Copy) 9] !facplus*(X, Y) >= Y because [10], by (Select) 10] Y >= Y by (Meta) 11] D#(!factimes(X, Y)) >= D#(Y) because D# in Mul and [12], by (Fun) 12] !factimes(X, Y) >= Y because [13], by (Star) 13] !factimes*(X, Y) >= Y because [14], by (Select) 14] Y >= Y by (Meta) 15] D#(!facminus(X, Y)) >= D#(X) because [16], by (Star) 16] D#*(!facminus(X, Y)) >= D#(X) because D# in Mul and [17], by (Stat) 17] !facminus(X, Y) > X because [18], by definition 18] !facminus*(X, Y) >= X because [19], by (Select) 19] X >= X by (Meta) 20] D#(X) >= D#(X) because D# in Mul and [21], by (Fun) 21] X >= X by (Meta) 22] D#(div(X, Y)) >= D#(X) because D# in Mul and [23], by (Fun) 23] div(X, Y) >= X because [24], by (Star) 24] div*(X, Y) >= X because [25], by (Select) 25] X >= X by (Meta) 26] D#(div(X, Y)) >= D#(Y) because D# in Mul and [27], by (Fun) 27] div(X, Y) >= Y because [28], by (Star) 28] div*(X, Y) >= Y because [29], by (Select) 29] Y >= Y by (Meta) 30] D#(ln(X)) >= D#(X) because D# in Mul and [31], by (Fun) 31] ln(X) >= X because [32], by (Star) 32] ln*(X) >= X because [33], by (Select) 33] X >= X by (Meta) 34] D#(pow(X, Y)) > D#(X) because [35], by definition 35] D#*(pow(X, Y)) >= D#(X) because [36], by (Select) 36] pow(X, Y) >= D#(X) because [37], by (Star) 37] pow*(X, Y) >= D#(X) because pow > D# and [38], by (Copy) 38] pow*(X, Y) >= X because [39], by (Select) 39] X >= X by (Meta) 40] D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) because [41], by (Star) 41] D*(!facplus(X, Y)) >= !facplus(D(X), D(Y)) because D > !facplus, [42] and [45], by (Copy) 42] D*(!facplus(X, Y)) >= D(X) because D in Mul and [43], by (Stat) 43] !facplus(X, Y) > X because [44], by definition 44] !facplus*(X, Y) >= X because [4], by (Select) 45] D*(!facplus(X, Y)) >= D(Y) because D in Mul and [46], by (Stat) 46] !facplus(X, Y) > Y because [9], by definition 47] D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) because [48], by (Star) 48] D*(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) because D > !facplus, [49] and [55], by (Copy) 49] D*(!factimes(X, Y)) >= !factimes(Y, D(X)) because D > !factimes, [50] and [51], by (Copy) 50] D*(!factimes(X, Y)) >= Y because [12], by (Select) 51] D*(!factimes(X, Y)) >= D(X) because D in Mul and [52], by (Stat) 52] !factimes(X, Y) > X because [53], by definition 53] !factimes*(X, Y) >= X because [54], by (Select) 54] X >= X by (Meta) 55] D*(!factimes(X, Y)) >= !factimes(X, D(Y)) because D > !factimes, [56] and [58], by (Copy) 56] D*(!factimes(X, Y)) >= X because [57], by (Select) 57] !factimes(X, Y) >= X because [53], by (Star) 58] D*(!factimes(X, Y)) >= D(Y) because D in Mul and [59], by (Stat) 59] !factimes(X, Y) > Y because [60], by definition 60] !factimes*(X, Y) >= Y because [14], by (Select) 61] D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) because [62], by (Star) 62] D*(!facminus(X, Y)) >= !facminus(D(X), D(Y)) because D > !facminus, [63] and [64], by (Copy) 63] D*(!facminus(X, Y)) >= D(X) because D in Mul and [17], by (Stat) 64] D*(!facminus(X, Y)) >= D(Y) because D in Mul and [65], by (Stat) 65] !facminus(X, Y) > Y because [66], by definition 66] !facminus*(X, Y) >= Y because [67], by (Select) 67] Y >= Y by (Meta) 68] D(X) >= D(X) because D in Mul and [21], by (Fun) 69] D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, _|_))) because [70], by (Star) 70] D*(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, _|_))) because D > !facminus, [71] and [76], by (Copy) 71] D*(div(X, Y)) >= div(D(X), Y) because D > div, [72] and [75], by (Copy) 72] D*(div(X, Y)) >= D(X) because D in Mul and [73], by (Stat) 73] div(X, Y) > X because [74], by definition 74] div*(X, Y) >= X because [25], by (Select) 75] D*(div(X, Y)) >= Y because [27], by (Select) 76] D*(div(X, Y)) >= div(!factimes(X, D(Y)), pow(Y, _|_)) because D > div, [77] and [82], by (Copy) 77] D*(div(X, Y)) >= !factimes(X, D(Y)) because D > !factimes, [78] and [79], by (Copy) 78] D*(div(X, Y)) >= X because [23], by (Select) 79] D*(div(X, Y)) >= D(Y) because D in Mul and [80], by (Stat) 80] div(X, Y) > Y because [81], by definition 81] div*(X, Y) >= Y because [29], by (Select) 82] D*(div(X, Y)) >= pow(Y, _|_) because D > pow, [75] and [83], by (Copy) 83] D*(div(X, Y)) >= _|_ by (Bot) 84] D(ln(X)) >= div(D(X), X) because [85], by (Star) 85] D*(ln(X)) >= div(D(X), X) because D > div, [86] and [89], by (Copy) 86] D*(ln(X)) >= D(X) because D in Mul and [87], by (Stat) 87] ln(X) > X because [88], by definition 88] ln*(X) >= X because [33], by (Select) 89] D*(ln(X)) >= X because [31], by (Select) 90] D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, _|_))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) because [91], by (Star) 91] D*(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, _|_))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) because D > !facplus, [92] and [108], by (Copy) 92] D*(pow(X, Y)) >= !factimes(!factimes(Y, pow(X, !facminus(Y, _|_))), D(X)) because D > !factimes, [93] and [106], by (Copy) 93] D*(pow(X, Y)) >= !factimes(Y, pow(X, !facminus(Y, _|_))) because D > !factimes, [94] and [98], by (Copy) 94] D*(pow(X, Y)) >= Y because [95], by (Select) 95] pow(X, Y) >= Y because [96], by (Star) 96] pow*(X, Y) >= Y because [97], by (Select) 97] Y >= Y by (Meta) 98] D*(pow(X, Y)) >= pow(X, !facminus(Y, _|_)) because D > pow, [99] and [101], by (Copy) 99] D*(pow(X, Y)) >= X because [100], by (Select) 100] pow(X, Y) >= X because [38], by (Star) 101] D*(pow(X, Y)) >= !facminus(Y, _|_) because [102], by (Select) 102] pow(X, Y) >= !facminus(Y, _|_) because [103], by (Star) 103] pow*(X, Y) >= !facminus(Y, _|_) because pow > !facminus, [104] and [105], by (Copy) 104] pow*(X, Y) >= Y because [97], by (Select) 105] pow*(X, Y) >= _|_ by (Bot) 106] D*(pow(X, Y)) >= D(X) because D in Mul and [107], by (Stat) 107] pow(X, Y) > X because [38], by definition 108] D*(pow(X, Y)) >= !factimes(!factimes(pow(X, Y), ln(X)), D(Y)) because D > !factimes, [109] and [112], by (Copy) 109] D*(pow(X, Y)) >= !factimes(pow(X, Y), ln(X)) because D > !factimes, [110] and [111], by (Copy) 110] D*(pow(X, Y)) >= pow(X, Y) because D > pow, [99] and [94], by (Copy) 111] D*(pow(X, Y)) >= ln(X) because D > ln and [99], by (Copy) 112] D*(pow(X, Y)) >= D(Y) because D in Mul and [113], by (Stat) 113] pow(X, Y) > Y because [104], by definition By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_6, R_2, static, formative) by (P_7, R_2, static, formative), where P_7 consists of: D#(!facplus(X, Y)) =#> D#(X) D#(!facplus(X, Y)) =#> D#(Y) D#(!factimes(X, Y)) =#> D#(Y) D#(!facminus(X, Y)) =#> D#(X) D#(minus(X)) =#> D#(X) D#(div(X, Y)) =#> D#(X) D#(div(X, Y)) =#> D#(Y) D#(ln(X)) =#> D#(X) Thus, the original system is terminating if (P_7, R_2, static, formative) is finite. We consider the dependency pair problem (P_7, R_2, static, formative). 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#(!facplus(X, Y)) >? D#(X) D#(!facplus(X, Y)) >? D#(Y) D#(!factimes(X, Y)) >? D#(Y) D#(!facminus(X, Y)) >? D#(X) D#(minus(X)) >? D#(X) D#(div(X, Y)) >? D#(X) D#(div(X, Y)) >? D#(Y) D#(ln(X)) >? D#(X) D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) D(minus(X)) >= minus(D(X)) D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) D(ln(X)) >= div(D(X), X) D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) 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: [[!facminus(x_1, x_2)]] = x_1 [[1]] = _|_ [[2]] = _|_ [[minus(x_1)]] = x_1 We choose Lex = {} and Mul = {!facplus, !factimes, D, D#, div, ln, pow}, and the following precedence: D = ln = pow > !facplus > !factimes > div > D# Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: D#(!facplus(X, Y)) >= D#(X) D#(!facplus(X, Y)) >= D#(Y) D#(!factimes(X, Y)) >= D#(Y) D#(X) >= D#(X) D#(X) >= D#(X) D#(div(X, Y)) >= D#(X) D#(div(X, Y)) >= D#(Y) D#(ln(X)) > D#(X) D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(X) >= D(X) D(X) >= D(X) D(div(X, Y)) >= div(D(X), Y) D(ln(X)) >= div(D(X), X) D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, Y)), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) With these choices, we have: 1] D#(!facplus(X, Y)) >= D#(X) because D# in Mul and [2], by (Fun) 2] !facplus(X, Y) >= X because [3], by (Star) 3] !facplus*(X, Y) >= X because [4], by (Select) 4] X >= X by (Meta) 5] D#(!facplus(X, Y)) >= D#(Y) because D# in Mul and [6], by (Fun) 6] !facplus(X, Y) >= Y because [7], by (Star) 7] !facplus*(X, Y) >= Y because [8], by (Select) 8] Y >= Y by (Meta) 9] D#(!factimes(X, Y)) >= D#(Y) because D# in Mul and [10], by (Fun) 10] !factimes(X, Y) >= Y because [11], by (Star) 11] !factimes*(X, Y) >= Y because [12], by (Select) 12] Y >= Y by (Meta) 13] D#(X) >= D#(X) because D# in Mul and [14], by (Fun) 14] X >= X by (Meta) 15] D#(X) >= D#(X) because D# in Mul and [16], by (Fun) 16] X >= X by (Meta) 17] D#(div(X, Y)) >= D#(X) because D# in Mul and [18], by (Fun) 18] div(X, Y) >= X because [19], by (Star) 19] div*(X, Y) >= X because [20], by (Select) 20] X >= X by (Meta) 21] D#(div(X, Y)) >= D#(Y) because D# in Mul and [22], by (Fun) 22] div(X, Y) >= Y because [23], by (Star) 23] div*(X, Y) >= Y because [24], by (Select) 24] Y >= Y by (Meta) 25] D#(ln(X)) > D#(X) because [26], by definition 26] D#*(ln(X)) >= D#(X) because D# in Mul and [27], by (Stat) 27] ln(X) > X because [28], by definition 28] ln*(X) >= X because [29], by (Select) 29] X >= X by (Meta) 30] D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) because [31], by (Star) 31] D*(!facplus(X, Y)) >= !facplus(D(X), D(Y)) because D > !facplus, [32] and [35], by (Copy) 32] D*(!facplus(X, Y)) >= D(X) because D in Mul and [33], by (Stat) 33] !facplus(X, Y) > X because [34], by definition 34] !facplus*(X, Y) >= X because [4], by (Select) 35] D*(!facplus(X, Y)) >= D(Y) because D in Mul and [36], by (Stat) 36] !facplus(X, Y) > Y because [37], by definition 37] !facplus*(X, Y) >= Y because [8], by (Select) 38] D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) because [39], by (Star) 39] D*(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) because D > !facplus, [40] and [46], by (Copy) 40] D*(!factimes(X, Y)) >= !factimes(Y, D(X)) because D > !factimes, [41] and [42], by (Copy) 41] D*(!factimes(X, Y)) >= Y because [10], by (Select) 42] D*(!factimes(X, Y)) >= D(X) because D in Mul and [43], by (Stat) 43] !factimes(X, Y) > X because [44], by definition 44] !factimes*(X, Y) >= X because [45], by (Select) 45] X >= X by (Meta) 46] D*(!factimes(X, Y)) >= !factimes(X, D(Y)) because D > !factimes, [47] and [49], by (Copy) 47] D*(!factimes(X, Y)) >= X because [48], by (Select) 48] !factimes(X, Y) >= X because [44], by (Star) 49] D*(!factimes(X, Y)) >= D(Y) because D in Mul and [50], by (Stat) 50] !factimes(X, Y) > Y because [51], by definition 51] !factimes*(X, Y) >= Y because [12], by (Select) 52] D(X) >= D(X) because D in Mul and [14], by (Fun) 53] D(X) >= D(X) because D in Mul and [16], by (Fun) 54] D(div(X, Y)) >= div(D(X), Y) because [55], by (Star) 55] D*(div(X, Y)) >= div(D(X), Y) because D > div, [56] and [59], by (Copy) 56] D*(div(X, Y)) >= D(X) because D in Mul and [57], by (Stat) 57] div(X, Y) > X because [58], by definition 58] div*(X, Y) >= X because [20], by (Select) 59] D*(div(X, Y)) >= Y because [22], by (Select) 60] D(ln(X)) >= div(D(X), X) because [61], by (Star) 61] D*(ln(X)) >= div(D(X), X) because D > div, [62] and [63], by (Copy) 62] D*(ln(X)) >= D(X) because D in Mul and [27], by (Stat) 63] D*(ln(X)) >= X because [64], by (Select) 64] ln(X) >= X because [28], by (Star) 65] D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, Y)), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) because [66], by (Star) 66] D*(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, Y)), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) because D > !facplus, [67] and [80], by (Copy) 67] D*(pow(X, Y)) >= !factimes(!factimes(Y, pow(X, Y)), D(X)) because D > !factimes, [68] and [79], by (Copy) 68] D*(pow(X, Y)) >= !factimes(Y, pow(X, Y)) because D > !factimes, [69] and [73], by (Copy) 69] D*(pow(X, Y)) >= Y because [70], by (Select) 70] pow(X, Y) >= Y because [71], by (Star) 71] pow*(X, Y) >= Y because [72], by (Select) 72] Y >= Y by (Meta) 73] D*(pow(X, Y)) >= pow(X, Y) because D = pow, D in Mul, [74] and [77], by (Stat) 74] pow(X, Y) > X because [75], by definition 75] pow*(X, Y) >= X because [76], by (Select) 76] X >= X by (Meta) 77] pow(X, Y) > Y because [78], by definition 78] pow*(X, Y) >= Y because [72], by (Select) 79] D*(pow(X, Y)) >= D(X) because D in Mul and [74], by (Stat) 80] D*(pow(X, Y)) >= !factimes(!factimes(pow(X, Y), ln(X)), D(Y)) because D > !factimes, [81] and [87], by (Copy) 81] D*(pow(X, Y)) >= !factimes(pow(X, Y), ln(X)) because D > !factimes, [82] and [86], by (Copy) 82] D*(pow(X, Y)) >= pow(X, Y) because [83], by (Select) 83] pow(X, Y) >= pow(X, Y) because pow in Mul, [84] and [85], by (Fun) 84] X >= X by (Meta) 85] Y >= Y by (Meta) 86] D*(pow(X, Y)) >= ln(X) because D = ln, D in Mul and [74], by (Stat) 87] D*(pow(X, Y)) >= D(Y) because D in Mul and [88], by (Stat) 88] pow(X, Y) > Y because [78], by definition By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_7, R_2, static, formative) by (P_8, R_2, static, formative), where P_8 consists of: D#(!facplus(X, Y)) =#> D#(X) D#(!facplus(X, Y)) =#> D#(Y) D#(!factimes(X, Y)) =#> D#(Y) D#(!facminus(X, Y)) =#> D#(X) D#(minus(X)) =#> D#(X) D#(div(X, Y)) =#> D#(X) D#(div(X, Y)) =#> D#(Y) Thus, the original system is terminating if (P_8, R_2, static, formative) is finite. We consider the dependency pair problem (P_8, R_2, static, formative). 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#(!facplus(X, Y)) >? D#(X) D#(!facplus(X, Y)) >? D#(Y) D#(!factimes(X, Y)) >? D#(Y) D#(!facminus(X, Y)) >? D#(X) D#(minus(X)) >? D#(X) D#(div(X, Y)) >? D#(X) D#(div(X, Y)) >? D#(Y) D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) D(minus(X)) >= minus(D(X)) D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) D(ln(X)) >= div(D(X), X) D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) 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: [[!facminus(x_1, x_2)]] = !facminus(x_1) [[1]] = _|_ [[2]] = _|_ We choose Lex = {} and Mul = {!facminus, !facplus, !factimes, D, D#, div, ln, minus, pow}, and the following precedence: D = minus > !facminus > !facplus > !factimes > D# > ln > div > pow Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: D#(!facplus(X, Y)) >= D#(X) D#(!facplus(X, Y)) >= D#(Y) D#(!factimes(X, Y)) >= D#(Y) D#(!facminus(X)) >= D#(X) D#(minus(X)) > D#(X) D#(div(X, Y)) >= D#(X) D#(div(X, Y)) >= D#(Y) D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X)) >= !facminus(D(X)) D(minus(X)) >= minus(D(X)) D(div(X, Y)) >= !facminus(div(D(X), Y)) D(ln(X)) >= div(D(X), X) D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) With these choices, we have: 1] D#(!facplus(X, Y)) >= D#(X) because D# in Mul and [2], by (Fun) 2] !facplus(X, Y) >= X because [3], by (Star) 3] !facplus*(X, Y) >= X because [4], by (Select) 4] X >= X by (Meta) 5] D#(!facplus(X, Y)) >= D#(Y) because [6], by (Star) 6] D#*(!facplus(X, Y)) >= D#(Y) because D# in Mul and [7], by (Stat) 7] !facplus(X, Y) > Y because [8], by definition 8] !facplus*(X, Y) >= Y because [9], by (Select) 9] Y >= Y by (Meta) 10] D#(!factimes(X, Y)) >= D#(Y) because [11], by (Star) 11] D#*(!factimes(X, Y)) >= D#(Y) because [12], by (Select) 12] !factimes(X, Y) >= D#(Y) because [13], by (Star) 13] !factimes*(X, Y) >= D#(Y) because !factimes > D# and [14], by (Copy) 14] !factimes*(X, Y) >= Y because [15], by (Select) 15] Y >= Y by (Meta) 16] D#(!facminus(X)) >= D#(X) because [17], by (Star) 17] D#*(!facminus(X)) >= D#(X) because D# in Mul and [18], by (Stat) 18] !facminus(X) > X because [19], by definition 19] !facminus*(X) >= X because [20], by (Select) 20] X >= X by (Meta) 21] D#(minus(X)) > D#(X) because [22], by definition 22] D#*(minus(X)) >= D#(X) because [23], by (Select) 23] minus(X) >= D#(X) because [24], by (Star) 24] minus*(X) >= D#(X) because minus > D# and [25], by (Copy) 25] minus*(X) >= X because [26], by (Select) 26] X >= X by (Meta) 27] D#(div(X, Y)) >= D#(X) because D# in Mul and [28], by (Fun) 28] div(X, Y) >= X because [29], by (Star) 29] div*(X, Y) >= X because [30], by (Select) 30] X >= X by (Meta) 31] D#(div(X, Y)) >= D#(Y) because D# in Mul and [32], by (Fun) 32] div(X, Y) >= Y because [33], by (Star) 33] div*(X, Y) >= Y because [34], by (Select) 34] Y >= Y by (Meta) 35] D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) because [36], by (Star) 36] D*(!facplus(X, Y)) >= !facplus(D(X), D(Y)) because D > !facplus, [37] and [40], by (Copy) 37] D*(!facplus(X, Y)) >= D(X) because D in Mul and [38], by (Stat) 38] !facplus(X, Y) > X because [39], by definition 39] !facplus*(X, Y) >= X because [4], by (Select) 40] D*(!facplus(X, Y)) >= D(Y) because D in Mul and [7], by (Stat) 41] D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) because [42], by (Star) 42] D*(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) because D > !facplus, [43] and [50], by (Copy) 43] D*(!factimes(X, Y)) >= !factimes(Y, D(X)) because D > !factimes, [44] and [46], by (Copy) 44] D*(!factimes(X, Y)) >= Y because [45], by (Select) 45] !factimes(X, Y) >= Y because [14], by (Star) 46] D*(!factimes(X, Y)) >= D(X) because D in Mul and [47], by (Stat) 47] !factimes(X, Y) > X because [48], by definition 48] !factimes*(X, Y) >= X because [49], by (Select) 49] X >= X by (Meta) 50] D*(!factimes(X, Y)) >= !factimes(X, D(Y)) because D > !factimes, [51] and [53], by (Copy) 51] D*(!factimes(X, Y)) >= X because [52], by (Select) 52] !factimes(X, Y) >= X because [48], by (Star) 53] D*(!factimes(X, Y)) >= D(Y) because D in Mul and [54], by (Stat) 54] !factimes(X, Y) > Y because [14], by definition 55] D(!facminus(X)) >= !facminus(D(X)) because [56], by (Star) 56] D*(!facminus(X)) >= !facminus(D(X)) because D > !facminus and [57], by (Copy) 57] D*(!facminus(X)) >= D(X) because D in Mul and [18], by (Stat) 58] D(minus(X)) >= minus(D(X)) because D = minus, D in Mul and [59], by (Fun) 59] minus(X) >= D(X) because minus = D, minus in Mul and [60], by (Fun) 60] X >= X by (Meta) 61] D(div(X, Y)) >= !facminus(div(D(X), Y)) because [62], by (Star) 62] D*(div(X, Y)) >= !facminus(div(D(X), Y)) because D > !facminus and [63], by (Copy) 63] D*(div(X, Y)) >= div(D(X), Y) because D > div, [64] and [67], by (Copy) 64] D*(div(X, Y)) >= D(X) because D in Mul and [65], by (Stat) 65] div(X, Y) > X because [66], by definition 66] div*(X, Y) >= X because [30], by (Select) 67] D*(div(X, Y)) >= Y because [32], by (Select) 68] D(ln(X)) >= div(D(X), X) because [69], by (Star) 69] D*(ln(X)) >= div(D(X), X) because D > div, [70] and [74], by (Copy) 70] D*(ln(X)) >= D(X) because D in Mul and [71], by (Stat) 71] ln(X) > X because [72], by definition 72] ln*(X) >= X because [73], by (Select) 73] X >= X by (Meta) 74] D*(ln(X)) >= X because [75], by (Select) 75] ln(X) >= X because [72], by (Star) 76] D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) because [77], by (Star) 77] D*(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) because D > !facplus, [78] and [93], by (Copy) 78] D*(pow(X, Y)) >= !factimes(!factimes(Y, pow(X, !facminus(Y))), D(X)) because D > !factimes, [79] and [90], by (Copy) 79] D*(pow(X, Y)) >= !factimes(Y, pow(X, !facminus(Y))) because D > !factimes, [80] and [84], by (Copy) 80] D*(pow(X, Y)) >= Y because [81], by (Select) 81] pow(X, Y) >= Y because [82], by (Star) 82] pow*(X, Y) >= Y because [83], by (Select) 83] Y >= Y by (Meta) 84] D*(pow(X, Y)) >= pow(X, !facminus(Y)) because D > pow, [85] and [89], by (Copy) 85] D*(pow(X, Y)) >= X because [86], by (Select) 86] pow(X, Y) >= X because [87], by (Star) 87] pow*(X, Y) >= X because [88], by (Select) 88] X >= X by (Meta) 89] D*(pow(X, Y)) >= !facminus(Y) because D > !facminus and [80], by (Copy) 90] D*(pow(X, Y)) >= D(X) because D in Mul and [91], by (Stat) 91] pow(X, Y) > X because [92], by definition 92] pow*(X, Y) >= X because [88], by (Select) 93] D*(pow(X, Y)) >= !factimes(!factimes(pow(X, Y), ln(X)), D(Y)) because D > !factimes, [94] and [97], by (Copy) 94] D*(pow(X, Y)) >= !factimes(pow(X, Y), ln(X)) because D > !factimes, [95] and [96], by (Copy) 95] D*(pow(X, Y)) >= pow(X, Y) because D > pow, [85] and [80], by (Copy) 96] D*(pow(X, Y)) >= ln(X) because D > ln and [85], by (Copy) 97] D*(pow(X, Y)) >= D(Y) because D in Mul and [98], by (Stat) 98] pow(X, Y) > Y because [99], by definition 99] pow*(X, Y) >= Y because [83], by (Select) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_8, R_2, static, formative) by (P_9, R_2, static, formative), where P_9 consists of: D#(!facplus(X, Y)) =#> D#(X) D#(!facplus(X, Y)) =#> D#(Y) D#(!factimes(X, Y)) =#> D#(Y) D#(!facminus(X, Y)) =#> D#(X) D#(div(X, Y)) =#> D#(X) D#(div(X, Y)) =#> D#(Y) Thus, the original system is terminating if (P_9, R_2, static, formative) is finite. We consider the dependency pair problem (P_9, R_2, static, formative). The formative rules of (P_9, R_2) are R_3 ::= D(!facplus(X, Y)) => !facplus(D(X), D(Y)) D(!factimes(X, Y)) => !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X, Y)) => !facminus(D(X), D(Y)) D(div(X, Y)) => !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) D(ln(X)) => div(D(X), X) D(pow(X, Y)) => !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) By [Kop12, Thm. 7.17], we may replace the dependency pair problem (P_9, R_2, static, formative) by (P_9, R_3, static, formative). Thus, the original system is terminating if (P_9, R_3, static, formative) is finite. We consider the dependency pair problem (P_9, R_3, static, formative). 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#(!facplus(X, Y)) >? D#(X) D#(!facplus(X, Y)) >? D#(Y) D#(!factimes(X, Y)) >? D#(Y) D#(!facminus(X, Y)) >? D#(X) D#(div(X, Y)) >? D#(X) D#(div(X, Y)) >? D#(Y) D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) D(ln(X)) >= div(D(X), X) D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) 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: [[!facminus(x_1, x_2)]] = !facminus(x_1) [[1]] = _|_ [[2]] = _|_ We choose Lex = {} and Mul = {!facminus, !facplus, !factimes, D, D#, div, ln, pow}, and the following precedence: D > !facminus > ln > pow > !factimes > D# > div > !facplus Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: D#(!facplus(X, Y)) > D#(X) D#(!facplus(X, Y)) >= D#(Y) D#(!factimes(X, Y)) >= D#(Y) D#(!facminus(X)) >= D#(X) D#(div(X, Y)) >= D#(X) D#(div(X, Y)) >= D#(Y) D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X)) >= !facminus(D(X)) D(div(X, Y)) >= !facminus(div(D(X), Y)) D(ln(X)) >= div(D(X), X) D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) With these choices, we have: 1] D#(!facplus(X, Y)) > D#(X) because [2], by definition 2] D#*(!facplus(X, Y)) >= D#(X) because D# in Mul and [3], by (Stat) 3] !facplus(X, Y) > X because [4], by definition 4] !facplus*(X, Y) >= X because [5], by (Select) 5] X >= X by (Meta) 6] D#(!facplus(X, Y)) >= D#(Y) because D# in Mul and [7], by (Fun) 7] !facplus(X, Y) >= Y because [8], by (Star) 8] !facplus*(X, Y) >= Y because [9], by (Select) 9] Y >= Y by (Meta) 10] D#(!factimes(X, Y)) >= D#(Y) because D# in Mul and [11], by (Fun) 11] !factimes(X, Y) >= Y because [12], by (Star) 12] !factimes*(X, Y) >= Y because [13], by (Select) 13] Y >= Y by (Meta) 14] D#(!facminus(X)) >= D#(X) because [15], by (Star) 15] D#*(!facminus(X)) >= D#(X) because D# in Mul and [16], by (Stat) 16] !facminus(X) > X because [17], by definition 17] !facminus*(X) >= X because [18], by (Select) 18] X >= X by (Meta) 19] D#(div(X, Y)) >= D#(X) because [20], by (Star) 20] D#*(div(X, Y)) >= D#(X) because D# in Mul and [21], by (Stat) 21] div(X, Y) > X because [22], by definition 22] div*(X, Y) >= X because [23], by (Select) 23] X >= X by (Meta) 24] D#(div(X, Y)) >= D#(Y) because D# in Mul and [25], by (Fun) 25] div(X, Y) >= Y because [26], by (Star) 26] div*(X, Y) >= Y because [27], by (Select) 27] Y >= Y by (Meta) 28] D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) because [29], by (Star) 29] D*(!facplus(X, Y)) >= !facplus(D(X), D(Y)) because D > !facplus, [30] and [31], by (Copy) 30] D*(!facplus(X, Y)) >= D(X) because D in Mul and [3], by (Stat) 31] D*(!facplus(X, Y)) >= D(Y) because D in Mul and [32], by (Stat) 32] !facplus(X, Y) > Y because [33], by definition 33] !facplus*(X, Y) >= Y because [9], by (Select) 34] D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) because [35], by (Star) 35] D*(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) because D > !facplus, [36] and [42], by (Copy) 36] D*(!factimes(X, Y)) >= !factimes(Y, D(X)) because D > !factimes, [37] and [38], by (Copy) 37] D*(!factimes(X, Y)) >= Y because [11], by (Select) 38] D*(!factimes(X, Y)) >= D(X) because D in Mul and [39], by (Stat) 39] !factimes(X, Y) > X because [40], by definition 40] !factimes*(X, Y) >= X because [41], by (Select) 41] X >= X by (Meta) 42] D*(!factimes(X, Y)) >= !factimes(X, D(Y)) because D > !factimes, [43] and [45], by (Copy) 43] D*(!factimes(X, Y)) >= X because [44], by (Select) 44] !factimes(X, Y) >= X because [40], by (Star) 45] D*(!factimes(X, Y)) >= D(Y) because D in Mul and [46], by (Stat) 46] !factimes(X, Y) > Y because [47], by definition 47] !factimes*(X, Y) >= Y because [13], by (Select) 48] D(!facminus(X)) >= !facminus(D(X)) because [49], by (Star) 49] D*(!facminus(X)) >= !facminus(D(X)) because D > !facminus and [50], by (Copy) 50] D*(!facminus(X)) >= D(X) because D in Mul and [16], by (Stat) 51] D(div(X, Y)) >= !facminus(div(D(X), Y)) because [52], by (Star) 52] D*(div(X, Y)) >= !facminus(div(D(X), Y)) because D > !facminus and [53], by (Copy) 53] D*(div(X, Y)) >= div(D(X), Y) because D > div, [54] and [55], by (Copy) 54] D*(div(X, Y)) >= D(X) because D in Mul and [21], by (Stat) 55] D*(div(X, Y)) >= Y because [25], by (Select) 56] D(ln(X)) >= div(D(X), X) because [57], by (Star) 57] D*(ln(X)) >= div(D(X), X) because D > div, [58] and [62], by (Copy) 58] D*(ln(X)) >= D(X) because D in Mul and [59], by (Stat) 59] ln(X) > X because [60], by definition 60] ln*(X) >= X because [61], by (Select) 61] X >= X by (Meta) 62] D*(ln(X)) >= X because [63], by (Select) 63] ln(X) >= X because [60], by (Star) 64] D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) because [65], by (Star) 65] D*(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) because D > !facplus, [66] and [81], by (Copy) 66] D*(pow(X, Y)) >= !factimes(!factimes(Y, pow(X, !facminus(Y))), D(X)) because D > !factimes, [67] and [78], by (Copy) 67] D*(pow(X, Y)) >= !factimes(Y, pow(X, !facminus(Y))) because D > !factimes, [68] and [72], by (Copy) 68] D*(pow(X, Y)) >= Y because [69], by (Select) 69] pow(X, Y) >= Y because [70], by (Star) 70] pow*(X, Y) >= Y because [71], by (Select) 71] Y >= Y by (Meta) 72] D*(pow(X, Y)) >= pow(X, !facminus(Y)) because D > pow, [73] and [77], by (Copy) 73] D*(pow(X, Y)) >= X because [74], by (Select) 74] pow(X, Y) >= X because [75], by (Star) 75] pow*(X, Y) >= X because [76], by (Select) 76] X >= X by (Meta) 77] D*(pow(X, Y)) >= !facminus(Y) because D > !facminus and [68], by (Copy) 78] D*(pow(X, Y)) >= D(X) because D in Mul and [79], by (Stat) 79] pow(X, Y) > X because [80], by definition 80] pow*(X, Y) >= X because [76], by (Select) 81] D*(pow(X, Y)) >= !factimes(!factimes(pow(X, Y), ln(X)), D(Y)) because D > !factimes, [82] and [85], by (Copy) 82] D*(pow(X, Y)) >= !factimes(pow(X, Y), ln(X)) because D > !factimes, [83] and [84], by (Copy) 83] D*(pow(X, Y)) >= pow(X, Y) because D > pow, [73] and [68], by (Copy) 84] D*(pow(X, Y)) >= ln(X) because D > ln and [73], by (Copy) 85] D*(pow(X, Y)) >= D(Y) because D in Mul and [86], by (Stat) 86] pow(X, Y) > Y because [87], by definition 87] pow*(X, Y) >= Y because [71], by (Select) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_9, R_3, static, formative) by (P_10, R_3, static, formative), where P_10 consists of: D#(!facplus(X, Y)) =#> D#(Y) D#(!factimes(X, Y)) =#> D#(Y) D#(!facminus(X, Y)) =#> D#(X) D#(div(X, Y)) =#> D#(X) D#(div(X, Y)) =#> D#(Y) Thus, the original system is terminating if (P_10, R_3, static, formative) is finite. We consider the dependency pair problem (P_10, R_3, static, formative). 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#(!facplus(X, Y)) >? D#(Y) D#(!factimes(X, Y)) >? D#(Y) D#(!facminus(X, Y)) >? D#(X) D#(div(X, Y)) >? D#(X) D#(div(X, Y)) >? D#(Y) D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) D(ln(X)) >= div(D(X), X) D(pow(X, Y)) >= !facplus(!factimes(!factimes(Y, pow(X, !facminus(Y, 1))), D(X)), !factimes(!factimes(pow(X, Y), ln(X)), D(Y))) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: !facminus = \y0y1.y0 !facplus = \y0y1.1 + y1 !factimes = \y0y1.2 + y1 1 = 0 2 = 0 D = \y0.2y0 D# = \y0.y0 div = \y0y1.y0 + 2y1 ln = \y0.2y0 pow = \y0y1.2 + y1 Using this interpretation, the requirements translate to: [[D#(!facplus(_x0, _x1))]] = 1 + x1 > x1 = [[D#(_x1)]] [[D#(!factimes(_x0, _x1))]] = 2 + x1 > x1 = [[D#(_x1)]] [[D#(!facminus(_x0, _x1))]] = x0 >= x0 = [[D#(_x0)]] [[D#(div(_x0, _x1))]] = x0 + 2x1 >= x0 = [[D#(_x0)]] [[D#(div(_x0, _x1))]] = x0 + 2x1 >= x1 = [[D#(_x1)]] [[D(!facplus(_x0, _x1))]] = 2 + 2x1 >= 1 + 2x1 = [[!facplus(D(_x0), D(_x1))]] [[D(!factimes(_x0, _x1))]] = 4 + 2x1 >= 3 + 2x1 = [[!facplus(!factimes(_x1, D(_x0)), !factimes(_x0, D(_x1)))]] [[D(!facminus(_x0, _x1))]] = 2x0 >= 2x0 = [[!facminus(D(_x0), D(_x1))]] [[D(div(_x0, _x1))]] = 2x0 + 4x1 >= 2x0 + 2x1 = [[!facminus(div(D(_x0), _x1), div(!factimes(_x0, D(_x1)), pow(_x1, 2)))]] [[D(ln(_x0))]] = 4x0 >= 4x0 = [[div(D(_x0), _x0)]] [[D(pow(_x0, _x1))]] = 4 + 2x1 >= 3 + 2x1 = [[!facplus(!factimes(!factimes(_x1, pow(_x0, !facminus(_x1, 1))), D(_x0)), !factimes(!factimes(pow(_x0, _x1), ln(_x0)), D(_x1)))]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_10, R_3, static, formative) by (P_11, R_3, static, formative), where P_11 consists of: D#(!facminus(X, Y)) =#> D#(X) D#(div(X, Y)) =#> D#(X) D#(div(X, Y)) =#> D#(Y) Thus, the original system is terminating if (P_11, R_3, static, formative) is finite. We consider the dependency pair problem (P_11, R_3, static, formative). The formative rules of (P_11, R_3) are R_4 ::= D(!facminus(X, Y)) => !facminus(D(X), D(Y)) D(div(X, Y)) => !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) D(ln(X)) => div(D(X), X) By [Kop12, Thm. 7.17], we may replace the dependency pair problem (P_11, R_3, static, formative) by (P_11, R_4, static, formative). Thus, the original system is terminating if (P_11, R_4, static, formative) is finite. We consider the dependency pair problem (P_11, R_4, static, formative). 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#(!facminus(X, Y)) >? D#(X) D#(div(X, Y)) >? D#(X) D#(div(X, Y)) >? D#(Y) D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) D(div(X, Y)) >= !facminus(div(D(X), Y), div(!factimes(X, D(Y)), pow(Y, 2))) D(ln(X)) >= div(D(X), X) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: !facminus = \y0y1.1 + y0 !factimes = \y0y1.0 2 = 0 D = \y0.2y0 D# = \y0.y0 div = \y0y1.2 + y0 + 2y1 ln = \y0.3 + 3y0 pow = \y0y1.0 Using this interpretation, the requirements translate to: [[D#(!facminus(_x0, _x1))]] = 1 + x0 > x0 = [[D#(_x0)]] [[D#(div(_x0, _x1))]] = 2 + x0 + 2x1 > x0 = [[D#(_x0)]] [[D#(div(_x0, _x1))]] = 2 + x0 + 2x1 > x1 = [[D#(_x1)]] [[D(!facminus(_x0, _x1))]] = 2 + 2x0 >= 1 + 2x0 = [[!facminus(D(_x0), D(_x1))]] [[D(div(_x0, _x1))]] = 4 + 2x0 + 4x1 >= 3 + 2x0 + 2x1 = [[!facminus(div(D(_x0), _x1), div(!factimes(_x0, D(_x1)), pow(_x1, 2)))]] [[D(ln(_x0))]] = 6 + 6x0 >= 2 + 4x0 = [[div(D(_x0), _x0)]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_11, R_4) by ({}, R_4). By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed. As all dependency pair problems were succesfully simplified with sound (and complete) processors until nothing remained, we conclude termination. +++ Citations +++ [Kop12] C. Kop. Higher Order Termination. PhD Thesis, 2012. [Kop13] C. Kop. Static Dependency Pairs with Accessibility. Unpublished manuscript, http://cl-informatik.uibk.ac.at/users/kop/static.pdf, 2013. [KusIsoSakBla09] K. Kusakari, Y. Isogai, M. Sakai, and F. Blanqui. Static Dependency Pair Method Based On Strong Computability for Higher-Order Rewrite Systems. In volume 92(10) of IEICE Transactions on Information and Systems. 2007--2015, 2009.