We consider the system Applicative_first_order_05__#3.13. Alphabet: 0 : [] --> a cons : [d * e] --> e edge : [a * a * b] --> b empty : [] --> b eq : [a * a] --> c false : [] --> c filter : [d -> c * e] --> e filter2 : [c * d -> c * d * e] --> e if!fac6220reach!fac62201 : [c * a * a * b * b] --> c if!fac6220reach!fac62202 : [c * a * a * b * b] --> c map : [d -> d * e] --> e nil : [] --> e or : [c * c] --> c reach : [a * a * b * b] --> c s : [a] --> a true : [] --> c union : [b * b] --> b Rules: eq(0, 0) => true eq(0, s(x)) => false eq(s(x), 0) => false eq(s(x), s(y)) => eq(x, y) or(true, x) => true or(false, x) => x union(empty, x) => x union(edge(x, y, z), u) => edge(x, y, union(z, u)) reach(x, y, empty, z) => false reach(x, y, edge(z, u, v), w) => if!fac6220reach!fac62201(eq(x, z), x, y, edge(z, u, v), w) if!fac6220reach!fac62201(true, x, y, edge(z, u, v), w) => if!fac6220reach!fac62202(eq(y, u), x, y, edge(z, u, v), w) if!fac6220reach!fac62201(false, x, y, edge(z, u, v), w) => reach(x, y, v, edge(z, u, w)) if!fac6220reach!fac62202(true, x, y, edge(z, u, v), w) => true if!fac6220reach!fac62202(false, x, y, edge(z, u, v), w) => or(reach(x, y, v, w), reach(u, y, union(v, w), empty)) 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 observe that the rules contain a first-order subset: eq(0, 0) => true eq(0, s(X)) => false eq(s(X), 0) => false eq(s(X), s(Y)) => eq(X, Y) or(true, X) => true or(false, X) => X union(empty, X) => X union(edge(X, Y, Z), U) => edge(X, Y, union(Z, U)) reach(X, Y, empty, Z) => false reach(X, Y, edge(Z, U, V), W) => if!fac6220reach!fac62201(eq(X, Z), X, Y, edge(Z, U, V), W) if!fac6220reach!fac62201(true, X, Y, edge(Z, U, V), W) => if!fac6220reach!fac62202(eq(Y, U), X, Y, edge(Z, U, V), W) if!fac6220reach!fac62201(false, X, Y, edge(Z, U, V), W) => reach(X, Y, V, edge(Z, U, W)) if!fac6220reach!fac62202(true, X, Y, edge(Z, U, V), W) => true if!fac6220reach!fac62202(false, X, Y, edge(Z, U, V), W) => or(reach(X, Y, V, W), reach(U, Y, union(V, W), empty)) Moreover, the system is orthogonal. Thus, by [Kop12, Thm. 7.55], we may omit all first-order dependency pairs from the dependency pair problem (DP(R), R) if this first-order part is terminating when seen as a many-sorted first-order TRS. According to nattprover, this system is indeed terminating: || Input TRS: || 1: eq(0(),0()) -> true() || 2: eq(0(),s(PeRCenTX)) -> false() || 3: eq(s(PeRCenTX),0()) -> false() || 4: eq(s(PeRCenTX),s(PeRCenTY)) -> eq(PeRCenTX,PeRCenTY) || 5: or(true(),PeRCenTX) -> true() || 6: or(false(),PeRCenTX) -> PeRCenTX || 7: union(empty(),PeRCenTX) -> PeRCenTX || 8: union(edge(PeRCenTX,PeRCenTY,PeRCenTZ),PeRCenTU) -> edge(PeRCenTX,PeRCenTY,union(PeRCenTZ,PeRCenTU)) || 9: reach(PeRCenTX,PeRCenTY,empty(),PeRCenTZ) -> false() || 10: reach(PeRCenTX,PeRCenTY,edge(PeRCenTZ,PeRCenTU,PeRCenTV),PeRCenTW) -> if!fac6220reach!fac62201(eq(PeRCenTX,PeRCenTZ),PeRCenTX,PeRCenTY,edge(PeRCenTZ,PeRCenTU,PeRCenTV),PeRCenTW) || 11: if!fac6220reach!fac62201(true(),PeRCenTX,PeRCenTY,edge(PeRCenTZ,PeRCenTU,PeRCenTV),PeRCenTW) -> if!fac6220reach!fac62202(eq(PeRCenTY,PeRCenTU),PeRCenTX,PeRCenTY,edge(PeRCenTZ,PeRCenTU,PeRCenTV),PeRCenTW) || 12: if!fac6220reach!fac62201(false(),PeRCenTX,PeRCenTY,edge(PeRCenTZ,PeRCenTU,PeRCenTV),PeRCenTW) -> reach(PeRCenTX,PeRCenTY,PeRCenTV,edge(PeRCenTZ,PeRCenTU,PeRCenTW)) || 13: if!fac6220reach!fac62202(true(),PeRCenTX,PeRCenTY,edge(PeRCenTZ,PeRCenTU,PeRCenTV),PeRCenTW) -> true() || 14: if!fac6220reach!fac62202(false(),PeRCenTX,PeRCenTY,edge(PeRCenTZ,PeRCenTU,PeRCenTV),PeRCenTW) -> or(reach(PeRCenTX,PeRCenTY,PeRCenTV,PeRCenTW),reach(PeRCenTU,PeRCenTY,union(PeRCenTV,PeRCenTW),empty())) || Number of strict rules: 14 || Direct POLO(bPol) ... failed. || Uncurrying ... failed. || Dependency Pairs: || #1: #if!fac6220reach!fac62201(true(),PeRCenTX,PeRCenTY,edge(PeRCenTZ,PeRCenTU,PeRCenTV),PeRCenTW) -> #if!fac6220reach!fac62202(eq(PeRCenTY,PeRCenTU),PeRCenTX,PeRCenTY,edge(PeRCenTZ,PeRCenTU,PeRCenTV),PeRCenTW) || #2: #if!fac6220reach!fac62201(true(),PeRCenTX,PeRCenTY,edge(PeRCenTZ,PeRCenTU,PeRCenTV),PeRCenTW) -> #eq(PeRCenTY,PeRCenTU) || #3: #if!fac6220reach!fac62201(false(),PeRCenTX,PeRCenTY,edge(PeRCenTZ,PeRCenTU,PeRCenTV),PeRCenTW) -> #reach(PeRCenTX,PeRCenTY,PeRCenTV,edge(PeRCenTZ,PeRCenTU,PeRCenTW)) || #4: #if!fac6220reach!fac62202(false(),PeRCenTX,PeRCenTY,edge(PeRCenTZ,PeRCenTU,PeRCenTV),PeRCenTW) -> #or(reach(PeRCenTX,PeRCenTY,PeRCenTV,PeRCenTW),reach(PeRCenTU,PeRCenTY,union(PeRCenTV,PeRCenTW),empty())) || #5: #if!fac6220reach!fac62202(false(),PeRCenTX,PeRCenTY,edge(PeRCenTZ,PeRCenTU,PeRCenTV),PeRCenTW) -> #reach(PeRCenTX,PeRCenTY,PeRCenTV,PeRCenTW) || #6: #if!fac6220reach!fac62202(false(),PeRCenTX,PeRCenTY,edge(PeRCenTZ,PeRCenTU,PeRCenTV),PeRCenTW) -> #reach(PeRCenTU,PeRCenTY,union(PeRCenTV,PeRCenTW),empty()) || #7: #if!fac6220reach!fac62202(false(),PeRCenTX,PeRCenTY,edge(PeRCenTZ,PeRCenTU,PeRCenTV),PeRCenTW) -> #union(PeRCenTV,PeRCenTW) || #8: #reach(PeRCenTX,PeRCenTY,edge(PeRCenTZ,PeRCenTU,PeRCenTV),PeRCenTW) -> #if!fac6220reach!fac62201(eq(PeRCenTX,PeRCenTZ),PeRCenTX,PeRCenTY,edge(PeRCenTZ,PeRCenTU,PeRCenTV),PeRCenTW) || #9: #reach(PeRCenTX,PeRCenTY,edge(PeRCenTZ,PeRCenTU,PeRCenTV),PeRCenTW) -> #eq(PeRCenTX,PeRCenTZ) || #10: #union(edge(PeRCenTX,PeRCenTY,PeRCenTZ),PeRCenTU) -> #union(PeRCenTZ,PeRCenTU) || #11: #eq(s(PeRCenTX),s(PeRCenTY)) -> #eq(PeRCenTX,PeRCenTY) || Number of SCCs: 3, DPs: 7 || SCC { #11 } || POLO(Sum)... succeeded. || s w: x1 + 1 || if!fac6220reach!fac62201 w: 0 || edge w: 0 || if!fac6220reach!fac62202 w: 0 || eq w: 0 || false w: 0 || #if!fac6220reach!fac62202 w: 0 || reach w: 0 || true w: 0 || #reach w: 0 || #eq w: x1 || 0 w: 0 || union w: 0 || or w: 0 || #if!fac6220reach!fac62201 w: 0 || empty w: 0 || #or w: 0 || #union w: 0 || USABLE RULES: { } || Removed DPs: #11 || Number of SCCs: 2, DPs: 6 || SCC { #10 } || POLO(Sum)... succeeded. || s w: 1 || if!fac6220reach!fac62201 w: 0 || edge w: x3 + 1 || if!fac6220reach!fac62202 w: 0 || eq w: 0 || false w: 0 || #if!fac6220reach!fac62202 w: 0 || reach w: 0 || true w: 0 || #reach w: 0 || #eq w: 0 || 0 w: 0 || union w: 0 || or w: 0 || #if!fac6220reach!fac62201 w: 0 || empty w: 0 || #or w: 0 || #union w: x1 || USABLE RULES: { } || Removed DPs: #10 || Number of SCCs: 1, DPs: 5 || SCC { #1 #3 #5 #6 #8 } || POLO(Sum)... succeeded. || s w: x1 + 1 || if!fac6220reach!fac62201 w: 0 || edge w: x2 + x3 + 4 || if!fac6220reach!fac62202 w: 0 || eq w: x2 + 1 || false w: 3 || #if!fac6220reach!fac62202 w: x2 + x3 + x4 + x5 || reach w: 0 || true w: 3 || #reach w: x1 + x2 + x3 + x4 + 1 || #eq w: 0 || 0 w: 1 || union w: x1 + x2 + 1 || or w: 0 || #if!fac6220reach!fac62201 w: x2 + x3 + x4 + x5 + 1 || empty w: 1 || #or w: 0 || #union w: 0 || USABLE RULES: { 7 8 } || Removed DPs: #1 #5 #6 || Number of SCCs: 1, DPs: 2 || SCC { #3 #8 } || POLO(Sum)... succeeded. || s w: x1 || if!fac6220reach!fac62201 w: 0 || edge w: x2 + x3 + 4 || if!fac6220reach!fac62202 w: 0 || eq w: 1 || false w: 1 || #if!fac6220reach!fac62202 w: 0 || reach w: 0 || true w: 1 || #reach w: x1 + x3 + 3 || #eq w: 0 || 0 w: 1 || union w: x1 + x2 + 1 || or w: 0 || #if!fac6220reach!fac62201 w: x1 + x2 + x4 + 1 || empty w: 1 || #or w: 0 || #union w: 0 || USABLE RULES: { 1..4 7 8 } || Removed DPs: #3 #8 || Number of SCCs: 0, DPs: 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 [FuhKop19]). We thus obtain the following dependency pair problem (P_0, R_0, computable, formative): Dependency Pairs P_0: 0] map#(F, cons(X, Y)) =#> map#(F, Y) 1] filter#(F, cons(X, Y)) =#> filter2#(F X, F, X, Y) 2] filter2#(true, F, X, Y) =#> filter#(F, Y) 3] filter2#(false, F, X, Y) =#> filter#(F, Y) Rules R_0: eq(0, 0) => true eq(0, s(X)) => false eq(s(X), 0) => false eq(s(X), s(Y)) => eq(X, Y) or(true, X) => true or(false, X) => X union(empty, X) => X union(edge(X, Y, Z), U) => edge(X, Y, union(Z, U)) reach(X, Y, empty, Z) => false reach(X, Y, edge(Z, U, V), W) => if!fac6220reach!fac62201(eq(X, Z), X, Y, edge(Z, U, V), W) if!fac6220reach!fac62201(true, X, Y, edge(Z, U, V), W) => if!fac6220reach!fac62202(eq(Y, U), X, Y, edge(Z, U, V), W) if!fac6220reach!fac62201(false, X, Y, edge(Z, U, V), W) => reach(X, Y, V, edge(Z, U, W)) if!fac6220reach!fac62202(true, X, Y, edge(Z, U, V), W) => true if!fac6220reach!fac62202(false, X, Y, edge(Z, U, V), W) => or(reach(X, Y, V, W), reach(U, Y, union(V, W), empty)) 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, computable, formative) is finite. We consider the dependency pair problem (P_0, R_0, computable, 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 * 2 : 1 * 3 : 1 This graph has the following strongly connected components: P_1: map#(F, cons(X, Y)) =#> map#(F, Y) P_2: 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) and (P_2, R_0, m, f). Thus, the original system is terminating if each of (P_1, R_0, computable, formative) and (P_2, R_0, computable, formative) is finite. We consider the dependency pair problem (P_2, R_0, computable, 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 [FuhKop19, Thm. 61], we may replace a dependency pair problem (P_2, R_0, computable, f) by (P_3, R_0, computable, f), where P_3 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, computable, formative) and (P_3, R_0, computable, formative) is finite. We consider the dependency pair problem (P_3, R_0, computable, 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 (P_1, R_0, computable, formative) is finite. We consider the dependency pair problem (P_1, R_0, computable, 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 [FuhKop19, Thm. 61], we may replace a dependency pair problem (P_1, R_0, computable, f) by ({}, R_0, computable, 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 +++ [FuhKop19] C. Fuhs, and C. Kop. A static higher-order dependency pair framework. In Proceedings of ESOP 2019, 2019. [Kop12] C. Kop. Higher Order Termination. PhD Thesis, 2012. [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.