We consider the system Applicative_first_order_05__#3.10. Alphabet: 0 : [] --> b add : [b * c] --> c app : [c * 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!fac6220minsort : [a * c * c] --> c if!fac6220rm : [a * b * c] --> c le : [b * b] --> a map : [b -> b * c] --> c min : [c] --> b minsort : [c * c] --> c nil : [] --> c rm : [b * c] --> c s : [b] --> b 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) app(nil, x) => x app(add(x, y), z) => add(x, app(y, z)) min(add(x, nil)) => x min(add(x, add(y, z))) => if!fac6220min(le(x, y), add(x, add(y, z))) if!fac6220min(true, add(x, add(y, z))) => min(add(x, z)) if!fac6220min(false, add(x, add(y, z))) => min(add(y, z)) rm(x, nil) => nil rm(x, add(y, z)) => if!fac6220rm(eq(x, y), x, add(y, z)) if!fac6220rm(true, x, add(y, z)) => rm(x, z) if!fac6220rm(false, x, add(y, z)) => add(y, rm(x, z)) minsort(nil, nil) => nil minsort(add(x, y), z) => if!fac6220minsort(eq(x, min(add(x, y))), add(x, y), z) if!fac6220minsort(true, add(x, y), z) => add(x, minsort(app(rm(x, y), z), nil)) if!fac6220minsort(false, add(x, y), z) => minsort(y, add(x, z)) map(f, nil) => nil map(f, add(x, y)) => add(f x, map(f, y)) filter(f, nil) => nil filter(f, add(x, y)) => filter2(f x, f, x, y) filter2(true, f, x, y) => add(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) app(nil, X) => X app(add(X, Y), Z) => add(X, app(Y, Z)) min(add(X, nil)) => X min(add(X, add(Y, Z))) => if!fac6220min(le(X, Y), add(X, add(Y, Z))) if!fac6220min(true, add(X, add(Y, Z))) => min(add(X, Z)) if!fac6220min(false, add(X, add(Y, Z))) => min(add(Y, Z)) rm(X, nil) => nil rm(X, add(Y, Z)) => if!fac6220rm(eq(X, Y), X, add(Y, Z)) if!fac6220rm(true, X, add(Y, Z)) => rm(X, Z) if!fac6220rm(false, X, add(Y, Z)) => add(Y, rm(X, Z)) minsort(nil, nil) => nil minsort(add(X, Y), Z) => if!fac6220minsort(eq(X, min(add(X, Y))), add(X, Y), Z) if!fac6220minsort(true, add(X, Y), Z) => add(X, minsort(app(rm(X, Y), Z), nil)) if!fac6220minsort(false, add(X, Y), Z) => minsort(Y, add(X, Z)) 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: app(nil(),PeRCenTX) -> PeRCenTX || 9: app(add(PeRCenTX,PeRCenTY),PeRCenTZ) -> add(PeRCenTX,app(PeRCenTY,PeRCenTZ)) || 10: min(add(PeRCenTX,nil())) -> PeRCenTX || 11: min(add(PeRCenTX,add(PeRCenTY,PeRCenTZ))) -> if!fac6220min(le(PeRCenTX,PeRCenTY),add(PeRCenTX,add(PeRCenTY,PeRCenTZ))) || 12: if!fac6220min(true(),add(PeRCenTX,add(PeRCenTY,PeRCenTZ))) -> min(add(PeRCenTX,PeRCenTZ)) || 13: if!fac6220min(false(),add(PeRCenTX,add(PeRCenTY,PeRCenTZ))) -> min(add(PeRCenTY,PeRCenTZ)) || 14: rm(PeRCenTX,nil()) -> nil() || 15: rm(PeRCenTX,add(PeRCenTY,PeRCenTZ)) -> if!fac6220rm(eq(PeRCenTX,PeRCenTY),PeRCenTX,add(PeRCenTY,PeRCenTZ)) || 16: if!fac6220rm(true(),PeRCenTX,add(PeRCenTY,PeRCenTZ)) -> rm(PeRCenTX,PeRCenTZ) || 17: if!fac6220rm(false(),PeRCenTX,add(PeRCenTY,PeRCenTZ)) -> add(PeRCenTY,rm(PeRCenTX,PeRCenTZ)) || 18: minsort(nil(),nil()) -> nil() || 19: minsort(add(PeRCenTX,PeRCenTY),PeRCenTZ) -> if!fac6220minsort(eq(PeRCenTX,min(add(PeRCenTX,PeRCenTY))),add(PeRCenTX,PeRCenTY),PeRCenTZ) || 20: if!fac6220minsort(true(),add(PeRCenTX,PeRCenTY),PeRCenTZ) -> add(PeRCenTX,minsort(app(rm(PeRCenTX,PeRCenTY),PeRCenTZ),nil())) || 21: if!fac6220minsort(false(),add(PeRCenTX,PeRCenTY),PeRCenTZ) -> minsort(PeRCenTY,add(PeRCenTX,PeRCenTZ)) || Number of strict rules: 21 || 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: app(nil(),PeRCenTX) -> PeRCenTX || 9: app(add(PeRCenTX,PeRCenTY),PeRCenTZ) -> add(PeRCenTX,app(PeRCenTY,PeRCenTZ)) || 10: min^1_add(PeRCenTX,nil()) -> PeRCenTX || 11: min^1_add(PeRCenTX,add(PeRCenTY,PeRCenTZ)) -> if!fac6220min(le(PeRCenTX,PeRCenTY),add(PeRCenTX,add(PeRCenTY,PeRCenTZ))) || 12: if!fac6220min(true(),add(PeRCenTX,add(PeRCenTY,PeRCenTZ))) -> min^1_add(PeRCenTX,PeRCenTZ) || 13: if!fac6220min(false(),add(PeRCenTX,add(PeRCenTY,PeRCenTZ))) -> min^1_add(PeRCenTY,PeRCenTZ) || 14: rm(PeRCenTX,nil()) -> nil() || 15: rm(PeRCenTX,add(PeRCenTY,PeRCenTZ)) -> if!fac6220rm(eq(PeRCenTX,PeRCenTY),PeRCenTX,add(PeRCenTY,PeRCenTZ)) || 16: if!fac6220rm(true(),PeRCenTX,add(PeRCenTY,PeRCenTZ)) -> rm(PeRCenTX,PeRCenTZ) || 17: if!fac6220rm(false(),PeRCenTX,add(PeRCenTY,PeRCenTZ)) -> add(PeRCenTY,rm(PeRCenTX,PeRCenTZ)) || 18: minsort(nil(),nil()) -> nil() || 19: minsort(add(PeRCenTX,PeRCenTY),PeRCenTZ) -> if!fac6220minsort(eq(PeRCenTX,min^1_add(PeRCenTX,PeRCenTY)),add(PeRCenTX,PeRCenTY),PeRCenTZ) || 20: if!fac6220minsort(true(),add(PeRCenTX,PeRCenTY),PeRCenTZ) -> add(PeRCenTX,minsort(app(rm(PeRCenTX,PeRCenTY),PeRCenTZ),nil())) || 21: if!fac6220minsort(false(),add(PeRCenTX,PeRCenTY),PeRCenTZ) -> minsort(PeRCenTY,add(PeRCenTX,PeRCenTZ)) || 22: min(add(_1,_2)) ->= min^1_add(_1,_2) || Number of strict rules: 21 || Direct POLO(bPol) ... failed. || Dependency Pairs: || #1: #if!fac6220min(false(),add(PeRCenTX,add(PeRCenTY,PeRCenTZ))) -> #min^1_add(PeRCenTY,PeRCenTZ) || #2: #app(add(PeRCenTX,PeRCenTY),PeRCenTZ) -> #app(PeRCenTY,PeRCenTZ) || #3: #min^1_add(PeRCenTX,add(PeRCenTY,PeRCenTZ)) -> #if!fac6220min(le(PeRCenTX,PeRCenTY),add(PeRCenTX,add(PeRCenTY,PeRCenTZ))) || #4: #min^1_add(PeRCenTX,add(PeRCenTY,PeRCenTZ)) -> #le(PeRCenTX,PeRCenTY) || #5: #if!fac6220min(true(),add(PeRCenTX,add(PeRCenTY,PeRCenTZ))) -> #min^1_add(PeRCenTX,PeRCenTZ) || #6: #if!fac6220minsort(true(),add(PeRCenTX,PeRCenTY),PeRCenTZ) -> #minsort(app(rm(PeRCenTX,PeRCenTY),PeRCenTZ),nil()) || #7: #if!fac6220minsort(true(),add(PeRCenTX,PeRCenTY),PeRCenTZ) -> #app(rm(PeRCenTX,PeRCenTY),PeRCenTZ) || #8: #if!fac6220minsort(true(),add(PeRCenTX,PeRCenTY),PeRCenTZ) -> #rm(PeRCenTX,PeRCenTY) || #9: #le(s(PeRCenTX),s(PeRCenTY)) -> #le(PeRCenTX,PeRCenTY) || #10: #min(add(_1,_2)) ->? #min^1_add(_1,_2) || #11: #if!fac6220rm(false(),PeRCenTX,add(PeRCenTY,PeRCenTZ)) -> #rm(PeRCenTX,PeRCenTZ) || #12: #minsort(add(PeRCenTX,PeRCenTY),PeRCenTZ) -> #if!fac6220minsort(eq(PeRCenTX,min^1_add(PeRCenTX,PeRCenTY)),add(PeRCenTX,PeRCenTY),PeRCenTZ) || #13: #minsort(add(PeRCenTX,PeRCenTY),PeRCenTZ) -> #eq(PeRCenTX,min^1_add(PeRCenTX,PeRCenTY)) || #14: #minsort(add(PeRCenTX,PeRCenTY),PeRCenTZ) -> #min^1_add(PeRCenTX,PeRCenTY) || #15: #if!fac6220minsort(false(),add(PeRCenTX,PeRCenTY),PeRCenTZ) -> #minsort(PeRCenTY,add(PeRCenTX,PeRCenTZ)) || #16: #if!fac6220rm(true(),PeRCenTX,add(PeRCenTY,PeRCenTZ)) -> #rm(PeRCenTX,PeRCenTZ) || #17: #rm(PeRCenTX,add(PeRCenTY,PeRCenTZ)) -> #if!fac6220rm(eq(PeRCenTX,PeRCenTY),PeRCenTX,add(PeRCenTY,PeRCenTZ)) || #18: #rm(PeRCenTX,add(PeRCenTY,PeRCenTZ)) -> #eq(PeRCenTX,PeRCenTY) || #19: #eq(s(PeRCenTX),s(PeRCenTY)) -> #eq(PeRCenTX,PeRCenTY) || Number of SCCs: 6, DPs: 12 || SCC { #19 } || POLO(Sum)... succeeded. || #if!fac6220min w: 0 || le w: 0 || s w: x1 + 1 || #le w: 0 || #if!fac6220minsort w: 0 || #if!fac6220rm w: 0 || eq w: 0 || false w: 0 || #min w: 0 || min^1_add w: 0 || true w: 0 || #eq w: x1 + x2 || if!fac6220minsort w: 0 || 0 w: 0 || if!fac6220min w: 0 || nil w: 0 || #app w: 0 || min w: 0 || #min^1_add w: 0 || #minsort w: 0 || add w: 0 || if!fac6220rm w: 0 || minsort w: 0 || rm w: 0 || #rm w: 0 || app w: 0 || USABLE RULES: { } || Removed DPs: #19 || Number of SCCs: 5, DPs: 11 || SCC { #9 } || POLO(Sum)... succeeded. || #if!fac6220min w: 0 || le w: 0 || s w: x1 + 1 || #le w: x1 || #if!fac6220minsort w: 0 || #if!fac6220rm w: 0 || eq w: 0 || false w: 0 || #min w: 0 || min^1_add w: 0 || true w: 0 || #eq w: 0 || if!fac6220minsort w: 0 || 0 w: 0 || if!fac6220min w: 0 || nil w: 0 || #app w: 0 || min w: 0 || #min^1_add w: 0 || #minsort w: 0 || add w: 0 || if!fac6220rm w: 0 || minsort w: 0 || rm w: 0 || #rm w: 0 || app w: 0 || USABLE RULES: { } || Removed DPs: #9 || Number of SCCs: 4, DPs: 10 || SCC { #2 } || POLO(Sum)... succeeded. || #if!fac6220min w: 0 || le w: 0 || s w: 1 || #le w: 0 || #if!fac6220minsort w: 0 || #if!fac6220rm w: 0 || eq w: 0 || false w: 0 || #min w: 0 || min^1_add w: 0 || true w: 0 || #eq w: 0 || if!fac6220minsort w: 0 || 0 w: 0 || if!fac6220min w: 0 || nil w: 0 || #app w: x1 || min w: 0 || #min^1_add w: 0 || #minsort w: 0 || add w: x2 + 1 || if!fac6220rm w: 0 || minsort w: 0 || rm w: 0 || #rm w: 0 || app w: 0 || USABLE RULES: { } || Removed DPs: #2 || Number of SCCs: 3, DPs: 9 || SCC { #11 #16 #17 } || POLO(Sum)... succeeded. || #if!fac6220min w: 0 || le w: 0 || s w: x1 + 1 || #le w: 0 || #if!fac6220minsort w: 0 || #if!fac6220rm w: x2 + x3 || eq w: x1 + x2 + 1 || false w: 4 || #min w: 0 || min^1_add w: 0 || true w: 4 || #eq w: 0 || if!fac6220minsort w: 0 || 0 w: 1 || if!fac6220min w: 0 || nil w: 0 || #app w: 0 || min w: 0 || #min^1_add w: 0 || #minsort w: 0 || add w: x2 + 2 || if!fac6220rm w: 0 || minsort w: 0 || rm w: 0 || #rm w: x1 + x2 + 1 || app w: 0 || USABLE RULES: { } || Removed DPs: #11 #16 #17 || Number of SCCs: 2, DPs: 6 || SCC { #1 #3 #5 } || POLO(Sum)... succeeded. || #if!fac6220min w: x1 + x2 || le w: 3 || s w: x1 + 1 || #le w: 0 || #if!fac6220minsort w: 0 || #if!fac6220rm w: 0 || eq w: x1 + x2 || false w: 3 || #min w: 0 || min^1_add w: 0 || true w: 3 || #eq w: 0 || if!fac6220minsort w: 0 || 0 w: 1 || if!fac6220min w: 0 || nil w: 0 || #app w: 0 || min w: 0 || #min^1_add w: x2 + 6 || #minsort w: 0 || add w: x2 + 2 || if!fac6220rm w: 0 || minsort w: 0 || rm w: 0 || #rm w: 1 || app w: 0 || USABLE RULES: { 5..7 } || Removed DPs: #1 #3 #5 || Number of SCCs: 1, DPs: 3 || SCC { #6 #12 #15 } || POLO(Sum)... succeeded. || #if!fac6220min w: x1 || le w: 3 || s w: x1 + 1 || #le w: 0 || #if!fac6220minsort w: x2 + x3 || #if!fac6220rm w: 0 || eq w: x1 + 1 || false w: 3 || #min w: 0 || min^1_add w: 9 || true w: 0 || #eq w: 0 || if!fac6220minsort w: 0 || 0 w: 1 || if!fac6220min w: x1 + x2 || nil w: 1 || #app w: 0 || min w: 0 || #min^1_add w: 6 || #minsort w: x1 + x2 || add w: x2 + 4 || if!fac6220rm w: x3 + 1 || minsort w: 0 || rm w: x2 + 1 || #rm w: 1 || app w: x1 + x2 + 1 || USABLE RULES: { 5..9 14..17 } || Removed DPs: #6 || Number of SCCs: 1, DPs: 2 || SCC { #12 #15 } || POLO(Sum)... succeeded. || #if!fac6220min w: x1 || le w: 3 || s w: x1 + 1 || #le w: 0 || #if!fac6220minsort w: x2 || #if!fac6220rm w: 0 || eq w: x1 + 1 || false w: 3 || #min w: 0 || min^1_add w: 9 || true w: 0 || #eq w: 0 || if!fac6220minsort w: 0 || 0 w: 1 || if!fac6220min w: x1 + x2 || nil w: 1 || #app w: 0 || min w: 0 || #min^1_add w: 6 || #minsort w: x1 + 1 || add w: x2 + 4 || if!fac6220rm w: x3 + 1 || minsort w: 0 || rm w: x2 + 1 || #rm w: 1 || app w: x1 + x2 + 1 || USABLE RULES: { 5..9 14..17 } || Removed DPs: #12 #15 || 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, add(X, Y)) =#> map#(F, Y) 1] filter#(F, add(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) app(nil, X) => X app(add(X, Y), Z) => add(X, app(Y, Z)) min(add(X, nil)) => X min(add(X, add(Y, Z))) => if!fac6220min(le(X, Y), add(X, add(Y, Z))) if!fac6220min(true, add(X, add(Y, Z))) => min(add(X, Z)) if!fac6220min(false, add(X, add(Y, Z))) => min(add(Y, Z)) rm(X, nil) => nil rm(X, add(Y, Z)) => if!fac6220rm(eq(X, Y), X, add(Y, Z)) if!fac6220rm(true, X, add(Y, Z)) => rm(X, Z) if!fac6220rm(false, X, add(Y, Z)) => add(Y, rm(X, Z)) minsort(nil, nil) => nil minsort(add(X, Y), Z) => if!fac6220minsort(eq(X, min(add(X, Y))), add(X, Y), Z) if!fac6220minsort(true, add(X, Y), Z) => add(X, minsort(app(rm(X, Y), Z), nil)) if!fac6220minsort(false, add(X, Y), Z) => minsort(Y, add(X, Z)) map(F, nil) => nil map(F, add(X, Y)) => add(F X, map(F, Y)) filter(F, nil) => nil filter(F, add(X, Y)) => filter2(F X, F, X, Y) filter2(true, F, X, Y) => add(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, add(X, Y)) =#> map#(F, Y) P_2: filter#(F, add(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, add(X, Y))) = add(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, add(X, Y))) = add(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.