We consider the system Applicative_AG01_innermost__#4.36. Alphabet: 0 : [] --> b cons : [b * c] --> c eq : [b * b] --> a false : [] --> a filter : [b -> a * c] --> c filter2 : [a * b -> a * b * c] --> c if!fac6220min : [a * c] --> b if!fac6220replace : [a * b * b * c] --> c le : [b * b] --> a map : [b -> b * c] --> c min : [c] --> b nil : [] --> c replace : [b * b * c] --> c s : [b] --> b sort : [c] --> c true : [] --> a Rules: eq(0, 0) => true eq(0, s(x)) => false eq(s(x), 0) => false eq(s(x), s(y)) => eq(x, y) le(0, x) => true le(s(x), 0) => false le(s(x), s(y)) => le(x, y) min(cons(0, nil)) => 0 min(cons(s(x), nil)) => s(x) min(cons(x, cons(y, z))) => if!fac6220min(le(x, y), cons(x, cons(y, z))) if!fac6220min(true, cons(x, cons(y, z))) => min(cons(x, z)) if!fac6220min(false, cons(x, cons(y, z))) => min(cons(y, z)) replace(x, y, nil) => nil replace(x, y, cons(z, u)) => if!fac6220replace(eq(x, z), x, y, cons(z, u)) if!fac6220replace(true, x, y, cons(z, u)) => cons(y, u) if!fac6220replace(false, x, y, cons(z, u)) => cons(z, replace(x, y, u)) sort(nil) => nil sort(cons(x, y)) => cons(min(cons(x, y)), sort(replace(min(cons(x, y)), x, 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 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) le(0, X) => true le(s(X), 0) => false le(s(X), s(Y)) => le(X, Y) min(cons(0, nil)) => 0 min(cons(s(X), nil)) => s(X) min(cons(X, cons(Y, Z))) => if!fac6220min(le(X, Y), cons(X, cons(Y, Z))) if!fac6220min(true, cons(X, cons(Y, Z))) => min(cons(X, Z)) if!fac6220min(false, cons(X, cons(Y, Z))) => min(cons(Y, Z)) replace(X, Y, nil) => nil replace(X, Y, cons(Z, U)) => if!fac6220replace(eq(X, Z), X, Y, cons(Z, U)) if!fac6220replace(true, X, Y, cons(Z, U)) => cons(Y, U) if!fac6220replace(false, X, Y, cons(Z, U)) => cons(Z, replace(X, Y, U)) sort(nil) => nil sort(cons(X, Y)) => cons(min(cons(X, Y)), sort(replace(min(cons(X, Y)), X, Y))) 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: le(0(),PeRCenTX) -> true() || 6: le(s(PeRCenTX),0()) -> false() || 7: le(s(PeRCenTX),s(PeRCenTY)) -> le(PeRCenTX,PeRCenTY) || 8: min(cons(0(),nil())) -> 0() || 9: min(cons(s(PeRCenTX),nil())) -> s(PeRCenTX) || 10: min(cons(PeRCenTX,cons(PeRCenTY,PeRCenTZ))) -> if!fac6220min(le(PeRCenTX,PeRCenTY),cons(PeRCenTX,cons(PeRCenTY,PeRCenTZ))) || 11: if!fac6220min(true(),cons(PeRCenTX,cons(PeRCenTY,PeRCenTZ))) -> min(cons(PeRCenTX,PeRCenTZ)) || 12: if!fac6220min(false(),cons(PeRCenTX,cons(PeRCenTY,PeRCenTZ))) -> min(cons(PeRCenTY,PeRCenTZ)) || 13: replace(PeRCenTX,PeRCenTY,nil()) -> nil() || 14: replace(PeRCenTX,PeRCenTY,cons(PeRCenTZ,PeRCenTU)) -> if!fac6220replace(eq(PeRCenTX,PeRCenTZ),PeRCenTX,PeRCenTY,cons(PeRCenTZ,PeRCenTU)) || 15: if!fac6220replace(true(),PeRCenTX,PeRCenTY,cons(PeRCenTZ,PeRCenTU)) -> cons(PeRCenTY,PeRCenTU) || 16: if!fac6220replace(false(),PeRCenTX,PeRCenTY,cons(PeRCenTZ,PeRCenTU)) -> cons(PeRCenTZ,replace(PeRCenTX,PeRCenTY,PeRCenTU)) || 17: sort(nil()) -> nil() || 18: sort(cons(PeRCenTX,PeRCenTY)) -> cons(min(cons(PeRCenTX,PeRCenTY)),sort(replace(min(cons(PeRCenTX,PeRCenTY)),PeRCenTX,PeRCenTY))) || Number of strict rules: 18 || Direct POLO(bPol) ... failed. || Uncurrying min || 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: le(0(),PeRCenTX) -> true() || 6: le(s(PeRCenTX),0()) -> false() || 7: le(s(PeRCenTX),s(PeRCenTY)) -> le(PeRCenTX,PeRCenTY) || 8: min^1_cons(0(),nil()) -> 0() || 9: min^1_cons(s(PeRCenTX),nil()) -> s(PeRCenTX) || 10: min^1_cons(PeRCenTX,cons(PeRCenTY,PeRCenTZ)) -> if!fac6220min(le(PeRCenTX,PeRCenTY),cons(PeRCenTX,cons(PeRCenTY,PeRCenTZ))) || 11: if!fac6220min(true(),cons(PeRCenTX,cons(PeRCenTY,PeRCenTZ))) -> min^1_cons(PeRCenTX,PeRCenTZ) || 12: if!fac6220min(false(),cons(PeRCenTX,cons(PeRCenTY,PeRCenTZ))) -> min^1_cons(PeRCenTY,PeRCenTZ) || 13: replace(PeRCenTX,PeRCenTY,nil()) -> nil() || 14: replace(PeRCenTX,PeRCenTY,cons(PeRCenTZ,PeRCenTU)) -> if!fac6220replace(eq(PeRCenTX,PeRCenTZ),PeRCenTX,PeRCenTY,cons(PeRCenTZ,PeRCenTU)) || 15: if!fac6220replace(true(),PeRCenTX,PeRCenTY,cons(PeRCenTZ,PeRCenTU)) -> cons(PeRCenTY,PeRCenTU) || 16: if!fac6220replace(false(),PeRCenTX,PeRCenTY,cons(PeRCenTZ,PeRCenTU)) -> cons(PeRCenTZ,replace(PeRCenTX,PeRCenTY,PeRCenTU)) || 17: sort(nil()) -> nil() || 18: sort(cons(PeRCenTX,PeRCenTY)) -> cons(min^1_cons(PeRCenTX,PeRCenTY),sort(replace(min^1_cons(PeRCenTX,PeRCenTY),PeRCenTX,PeRCenTY))) || 19: min(cons(_1,_2)) ->= min^1_cons(_1,_2) || Number of strict rules: 18 || Direct POLO(bPol) ... failed. || Dependency Pairs: || #1: #if!fac6220min(true(),cons(PeRCenTX,cons(PeRCenTY,PeRCenTZ))) -> #min^1_cons(PeRCenTX,PeRCenTZ) || #2: #if!fac6220min(false(),cons(PeRCenTX,cons(PeRCenTY,PeRCenTZ))) -> #min^1_cons(PeRCenTY,PeRCenTZ) || #3: #replace(PeRCenTX,PeRCenTY,cons(PeRCenTZ,PeRCenTU)) -> #if!fac6220replace(eq(PeRCenTX,PeRCenTZ),PeRCenTX,PeRCenTY,cons(PeRCenTZ,PeRCenTU)) || #4: #replace(PeRCenTX,PeRCenTY,cons(PeRCenTZ,PeRCenTU)) -> #eq(PeRCenTX,PeRCenTZ) || #5: #le(s(PeRCenTX),s(PeRCenTY)) -> #le(PeRCenTX,PeRCenTY) || #6: #min^1_cons(PeRCenTX,cons(PeRCenTY,PeRCenTZ)) -> #if!fac6220min(le(PeRCenTX,PeRCenTY),cons(PeRCenTX,cons(PeRCenTY,PeRCenTZ))) || #7: #min^1_cons(PeRCenTX,cons(PeRCenTY,PeRCenTZ)) -> #le(PeRCenTX,PeRCenTY) || #8: #min(cons(_1,_2)) ->? #min^1_cons(_1,_2) || #9: #if!fac6220replace(false(),PeRCenTX,PeRCenTY,cons(PeRCenTZ,PeRCenTU)) -> #replace(PeRCenTX,PeRCenTY,PeRCenTU) || #10: #eq(s(PeRCenTX),s(PeRCenTY)) -> #eq(PeRCenTX,PeRCenTY) || #11: #sort(cons(PeRCenTX,PeRCenTY)) -> #min^1_cons(PeRCenTX,PeRCenTY) || #12: #sort(cons(PeRCenTX,PeRCenTY)) -> #sort(replace(min^1_cons(PeRCenTX,PeRCenTY),PeRCenTX,PeRCenTY)) || #13: #sort(cons(PeRCenTX,PeRCenTY)) -> #replace(min^1_cons(PeRCenTX,PeRCenTY),PeRCenTX,PeRCenTY) || #14: #sort(cons(PeRCenTX,PeRCenTY)) -> #min^1_cons(PeRCenTX,PeRCenTY) || Number of SCCs: 5, DPs: 8 || SCC { #10 } || POLO(Sum)... succeeded. || #if!fac6220replace w: 0 || #if!fac6220min w: 0 || le w: 0 || s w: x1 + 1 || #le w: 0 || min^1_cons w: 0 || eq w: 0 || if!fac6220replace w: 0 || false w: 0 || #min w: 0 || true w: 0 || #eq w: x1 + x2 || #sort w: 0 || 0 w: 0 || if!fac6220min w: 0 || nil w: 0 || sort w: 0 || #replace w: 0 || min w: 0 || #min^1_cons w: 0 || cons w: 0 || replace w: 0 || USABLE RULES: { } || Removed DPs: #10 || Number of SCCs: 4, DPs: 7 || SCC { #5 } || POLO(Sum)... succeeded. || #if!fac6220replace w: 0 || #if!fac6220min w: 0 || le w: 0 || s w: x1 + 1 || #le w: x1 || min^1_cons w: 0 || eq w: 0 || if!fac6220replace w: 0 || false w: 0 || #min w: 0 || true w: 0 || #eq w: 0 || #sort w: 0 || 0 w: 0 || if!fac6220min w: 0 || nil w: 0 || sort w: 0 || #replace w: 0 || min w: 0 || #min^1_cons w: 0 || cons w: 0 || replace w: 0 || USABLE RULES: { } || Removed DPs: #5 || Number of SCCs: 3, DPs: 6 || SCC { #12 } || POLO(Sum)... succeeded. || #if!fac6220replace w: 0 || #if!fac6220min w: 0 || le w: x2 + 1 || s w: 1 || #le w: 0 || min^1_cons w: 1 || eq w: x2 + 1 || if!fac6220replace w: x2 + x4 + 1 || false w: 3 || #min w: 0 || true w: 3 || #eq w: 0 || #sort w: x1 || 0 w: 1 || if!fac6220min w: 1 || nil w: 1 || sort w: 0 || #replace w: 0 || min w: 0 || #min^1_cons w: 0 || cons w: x2 + 3 || replace w: x1 + x3 + 1 || USABLE RULES: { 8..16 } || Removed DPs: #12 || Number of SCCs: 2, DPs: 5 || SCC { #3 #9 } || POLO(Sum)... succeeded. || #if!fac6220replace w: x2 + x4 || #if!fac6220min w: 0 || le w: 1 || s w: x1 + 1 || #le w: 0 || min^1_cons w: 1 || eq w: x1 + x2 || if!fac6220replace w: x2 + x4 || false w: 0 || #min w: 0 || true w: 2 || #eq w: 0 || #sort w: 0 || 0 w: 1 || if!fac6220min w: 1 || nil w: 1 || sort w: 0 || #replace w: x1 + x3 + 2 || min w: 0 || #min^1_cons w: 0 || cons w: x2 + 3 || replace w: x1 + x3 || USABLE RULES: { 1..3 8 13..16 } || Removed DPs: #3 #9 || Number of SCCs: 1, DPs: 3 || SCC { #1 #2 #6 } || POLO(Sum)... succeeded. || #if!fac6220replace w: 0 || #if!fac6220min w: x1 + x2 || le w: 2 || s w: x1 + 1 || #le w: 0 || min^1_cons w: 1 || eq w: x1 + x2 || if!fac6220replace w: x2 + x4 || false w: 2 || #min w: 0 || true w: 2 || #eq w: 0 || #sort w: 0 || 0 w: 1 || if!fac6220min w: 1 || nil w: 1 || sort w: 0 || #replace w: 2 || min w: 0 || #min^1_cons w: x2 + 5 || cons w: x2 + 2 || replace w: x1 + x3 || USABLE RULES: { 1..3 5..8 13..16 } || Removed DPs: #1 #2 #6 || 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) le(0, X) => true le(s(X), 0) => false le(s(X), s(Y)) => le(X, Y) min(cons(0, nil)) => 0 min(cons(s(X), nil)) => s(X) min(cons(X, cons(Y, Z))) => if!fac6220min(le(X, Y), cons(X, cons(Y, Z))) if!fac6220min(true, cons(X, cons(Y, Z))) => min(cons(X, Z)) if!fac6220min(false, cons(X, cons(Y, Z))) => min(cons(Y, Z)) replace(X, Y, nil) => nil replace(X, Y, cons(Z, U)) => if!fac6220replace(eq(X, Z), X, Y, cons(Z, U)) if!fac6220replace(true, X, Y, cons(Z, U)) => cons(Y, U) if!fac6220replace(false, X, Y, cons(Z, U)) => cons(Z, replace(X, Y, U)) sort(nil) => nil sort(cons(X, Y)) => cons(min(cons(X, Y)), sort(replace(min(cons(X, Y)), X, 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, 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.