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). We place the elements of P in a dependency graph approximation G (see e.g. [Kop12, Thm. 7.27, 7.29], as follows: * 0 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 * 1 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 * 2 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 * 3 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 * 4 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 * 5 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 * 6 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 * 7 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 * 8 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 * 9 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 * 10 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 * 11 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 * 12 : 12 * 13 : 14, 15 * 14 : 13 * 15 : 13 This graph has the following strongly connected components: P_1: 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) P_2: map#(F, cons(X, Y)) =#> map#(F, Y) P_3: 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) By [Kop12, Thm. 7.31], we may replace any dependency pair problem (P_0, R_0, m, f) by (P_1, R_0, m, f), (P_2, R_0, m, f) and (P_3, R_0, m, f). Thus, the original system is terminating if each of (P_1, R_0, static, formative), (P_2, R_0, static, formative) and (P_3, R_0, static, formative) is finite. We consider the dependency pair problem (P_3, R_0, static, formative). We apply the subterm criterion with the following projection function: nu(filter2#) = 4 nu(filter#) = 2 Thus, we can orient the dependency pairs as follows: nu(filter#(F, cons(X, Y))) = cons(X, Y) |> Y = nu(filter2#(F X, F, X, Y)) nu(filter2#(true, F, X, Y)) = Y = Y = nu(filter#(F, Y)) nu(filter2#(false, F, X, Y)) = Y = Y = nu(filter#(F, Y)) By [Kop12, Thm. 7.35] and [Kop13, Thm. 5], we may replace a dependency pair problem (P_3, R_0, static, f) by (P_4, R_0, static, f), where P_4 contains: filter2#(true, F, X, Y) =#> filter#(F, Y) filter2#(false, F, X, Y) =#> filter#(F, Y) Thus, the original system is terminating if each of (P_1, R_0, static, formative), (P_2, R_0, static, formative) and (P_4, R_0, static, formative) is finite. We consider the dependency pair problem (P_4, R_0, static, formative). We place the elements of P in a dependency graph approximation G (see e.g. [Kop12, Thm. 7.27, 7.29], as follows: * 0 : * 1 : This graph has no strongly connected components. By [Kop12, Thm. 7.31], this implies finiteness of the dependency pair problem. Thus, the original system is terminating if each of (P_1, R_0, static, formative) and (P_2, R_0, static, formative) is finite. We consider the dependency pair problem (P_2, R_0, static, formative). We apply the subterm criterion with the following projection function: nu(map#) = 2 Thus, we can orient the dependency pairs as follows: nu(map#(F, cons(X, Y))) = cons(X, Y) |> Y = nu(map#(F, Y)) By [Kop12, Thm. 7.35] and [Kop13, Thm. 5], we may replace a dependency pair problem (P_2, R_0, static, f) by ({}, R_0, static, f). By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed. Thus, the original system is terminating if (P_1, R_0, static, formative) is finite. We consider the dependency pair problem (P_1, R_0, static, formative). We apply the subterm criterion with the following projection function: nu(D#) = 1 Thus, we can orient the dependency pairs as follows: nu(D#(!facplus(X, Y))) = !facplus(X, Y) |> X = nu(D#(X)) nu(D#(!facplus(X, Y))) = !facplus(X, Y) |> Y = nu(D#(Y)) nu(D#(!factimes(X, Y))) = !factimes(X, Y) |> X = nu(D#(X)) nu(D#(!factimes(X, Y))) = !factimes(X, Y) |> Y = nu(D#(Y)) nu(D#(!facminus(X, Y))) = !facminus(X, Y) |> X = nu(D#(X)) nu(D#(!facminus(X, Y))) = !facminus(X, Y) |> Y = nu(D#(Y)) nu(D#(minus(X))) = minus(X) |> X = nu(D#(X)) nu(D#(div(X, Y))) = div(X, Y) |> X = nu(D#(X)) nu(D#(div(X, Y))) = div(X, Y) |> Y = nu(D#(Y)) nu(D#(ln(X))) = ln(X) |> X = nu(D#(X)) nu(D#(pow(X, Y))) = pow(X, Y) |> X = nu(D#(X)) nu(D#(pow(X, Y))) = pow(X, Y) |> Y = nu(D#(Y)) By [Kop12, Thm. 7.35] and [Kop13, Thm. 5], we may replace a dependency pair problem (P_1, R_0, static, f) by ({}, R_0, static, f). 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.