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 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] eq#(s(X), s(Y)) =#> eq#(X, Y) 1] le#(s(X), s(Y)) =#> le#(X, Y) 2] min#(cons(X, cons(Y, Z))) =#> if!fac6220min#(le(X, Y), cons(X, cons(Y, Z))) 3] min#(cons(X, cons(Y, Z))) =#> le#(X, Y) 4] if!fac6220min#(true, cons(X, cons(Y, Z))) =#> min#(cons(X, Z)) 5] if!fac6220min#(false, cons(X, cons(Y, Z))) =#> min#(cons(Y, Z)) 6] replace#(X, Y, cons(Z, U)) =#> if!fac6220replace#(eq(X, Z), X, Y, cons(Z, U)) 7] replace#(X, Y, cons(Z, U)) =#> eq#(X, Z) 8] if!fac6220replace#(false, X, Y, cons(Z, U)) =#> replace#(X, Y, U) 9] sort#(cons(X, Y)) =#> min#(cons(X, Y)) 10] sort#(cons(X, Y)) =#> sort#(replace(min(cons(X, Y)), X, Y)) 11] sort#(cons(X, Y)) =#> replace#(min(cons(X, Y)), X, Y) 12] sort#(cons(X, Y)) =#> min#(cons(X, Y)) 13] map#(F, cons(X, Y)) =#> map#(F, Y) 14] filter#(F, cons(X, Y)) =#> filter2#(F X, F, X, Y) 15] filter2#(true, F, X, Y) =#> filter#(F, Y) 16] 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 : 1 * 2 : 4, 5 * 3 : 1 * 4 : 2, 3 * 5 : 2, 3 * 6 : 8 * 7 : 0 * 8 : 6, 7 * 9 : 2, 3 * 10 : 9, 10, 11, 12 * 11 : 6, 7 * 12 : 2, 3 * 13 : 13 * 14 : 15, 16 * 15 : 14 * 16 : 14 This graph has the following strongly connected components: P_1: eq#(s(X), s(Y)) =#> eq#(X, Y) P_2: le#(s(X), s(Y)) =#> le#(X, Y) P_3: 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)) P_4: replace#(X, Y, cons(Z, U)) =#> if!fac6220replace#(eq(X, Z), X, Y, cons(Z, U)) if!fac6220replace#(false, X, Y, cons(Z, U)) =#> replace#(X, Y, U) P_5: sort#(cons(X, Y)) =#> sort#(replace(min(cons(X, Y)), X, Y)) P_6: map#(F, cons(X, Y)) =#> map#(F, Y) P_7: 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), (P_3, R_0, m, f), (P_4, R_0, m, f), (P_5, R_0, m, f), (P_6, R_0, m, f) and (P_7, R_0, m, f). Thus, the original system is terminating if each of (P_1, R_0, computable, formative), (P_2, R_0, computable, formative), (P_3, R_0, computable, formative), (P_4, R_0, computable, formative), (P_5, R_0, computable, formative), (P_6, R_0, computable, formative) and (P_7, R_0, computable, formative) is finite. We consider the dependency pair problem (P_7, 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_7, R_0, computable, f) by (P_8, R_0, computable, f), where P_8 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), (P_2, R_0, computable, formative), (P_3, R_0, computable, formative), (P_4, R_0, computable, formative), (P_5, R_0, computable, formative), (P_6, R_0, computable, formative) and (P_8, R_0, computable, formative) is finite. We consider the dependency pair problem (P_8, 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 each of (P_1, R_0, computable, formative), (P_2, R_0, computable, formative), (P_3, R_0, computable, formative), (P_4, R_0, computable, formative), (P_5, R_0, computable, formative) and (P_6, R_0, computable, formative) is finite. We consider the dependency pair problem (P_6, 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_6, R_0, computable, f) by ({}, R_0, computable, f). By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed. Thus, the original system is terminating if each of (P_1, R_0, computable, formative), (P_2, R_0, computable, formative), (P_3, R_0, computable, formative), (P_4, R_0, computable, formative) and (P_5, R_0, computable, formative) is finite. We consider the dependency pair problem (P_5, R_0, computable, formative). We will use the reduction pair processor with usable rules [Kop12, Thm. 7.44]. The usable rules of (P_5, R_0) are: 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)) It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: sort#(cons(X, Y)) >? sort#(replace(min(cons(X, Y)), X, Y)) 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)) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 0 cons = \y0y1.1 + y1 eq = \y0y1.0 false = 0 if!fac6220min = \y0y1.2 if!fac6220replace = \y0y1y2y3.y3 le = \y0y1.2 min = \y0.2 nil = 0 replace = \y0y1y2.y2 s = \y0.0 sort# = \y0.y0 true = 0 Using this interpretation, the requirements translate to: [[sort#(cons(_x0, _x1))]] = 1 + x1 > x1 = [[sort#(replace(min(cons(_x0, _x1)), _x0, _x1))]] [[eq(0, 0)]] = 0 >= 0 = [[true]] [[eq(0, s(_x0))]] = 0 >= 0 = [[false]] [[eq(s(_x0), 0)]] = 0 >= 0 = [[false]] [[eq(s(_x0), s(_x1))]] = 0 >= 0 = [[eq(_x0, _x1)]] [[le(0, _x0)]] = 2 >= 0 = [[true]] [[le(s(_x0), 0)]] = 2 >= 0 = [[false]] [[le(s(_x0), s(_x1))]] = 2 >= 2 = [[le(_x0, _x1)]] [[min(cons(0, nil))]] = 2 >= 0 = [[0]] [[min(cons(s(_x0), nil))]] = 2 >= 0 = [[s(_x0)]] [[min(cons(_x0, cons(_x1, _x2)))]] = 2 >= 2 = [[if!fac6220min(le(_x0, _x1), cons(_x0, cons(_x1, _x2)))]] [[if!fac6220min(true, cons(_x0, cons(_x1, _x2)))]] = 2 >= 2 = [[min(cons(_x0, _x2))]] [[if!fac6220min(false, cons(_x0, cons(_x1, _x2)))]] = 2 >= 2 = [[min(cons(_x1, _x2))]] [[replace(_x0, _x1, nil)]] = 0 >= 0 = [[nil]] [[replace(_x0, _x1, cons(_x2, _x3))]] = 1 + x3 >= 1 + x3 = [[if!fac6220replace(eq(_x0, _x2), _x0, _x1, cons(_x2, _x3))]] [[if!fac6220replace(true, _x0, _x1, cons(_x2, _x3))]] = 1 + x3 >= 1 + x3 = [[cons(_x1, _x3)]] [[if!fac6220replace(false, _x0, _x1, cons(_x2, _x3))]] = 1 + x3 >= 1 + x3 = [[cons(_x2, replace(_x0, _x1, _x3))]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_5, R_0) by ({}, R_0). By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed. Thus, the original system is terminating if each of (P_1, R_0, computable, formative), (P_2, R_0, computable, formative), (P_3, R_0, computable, formative) and (P_4, R_0, computable, formative) is finite. We consider the dependency pair problem (P_4, R_0, computable, formative). We apply the subterm criterion with the following projection function: nu(if!fac6220replace#) = 4 nu(replace#) = 3 Thus, we can orient the dependency pairs as follows: nu(replace#(X, Y, cons(Z, U))) = cons(Z, U) = cons(Z, U) = nu(if!fac6220replace#(eq(X, Z), X, Y, cons(Z, U))) nu(if!fac6220replace#(false, X, Y, cons(Z, U))) = cons(Z, U) |> U = nu(replace#(X, Y, U)) By [FuhKop19, Thm. 61], we may replace a dependency pair problem (P_4, R_0, computable, f) by (P_9, R_0, computable, f), where P_9 contains: replace#(X, Y, cons(Z, U)) =#> if!fac6220replace#(eq(X, Z), X, Y, cons(Z, U)) Thus, the original system is terminating if each of (P_1, R_0, computable, formative), (P_2, R_0, computable, formative), (P_3, R_0, computable, formative) and (P_9, R_0, computable, formative) is finite. We consider the dependency pair problem (P_9, 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 : 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, computable, formative), (P_2, 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 will use the reduction pair processor with usable rules [Kop12, Thm. 7.44]. The usable rules of (P_3, R_0) are: le(0, X) => true le(s(X), 0) => false le(s(X), s(Y)) => le(X, Y) It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: 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)) le(0, X) >= true le(s(X), 0) >= false le(s(X), s(Y)) >= le(X, Y) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 3 cons = \y0y1.2 + 3y0 + 3y1 false = 0 if!fac6220min# = \y0y1.y1 le = \y0y1.y1 + 2y0 min# = \y0.1 + y0 s = \y0.3 + 2y0 true = 0 Using this interpretation, the requirements translate to: [[min#(cons(_x0, cons(_x1, _x2)))]] = 9 + 3x0 + 9x1 + 9x2 > 8 + 3x0 + 9x1 + 9x2 = [[if!fac6220min#(le(_x0, _x1), cons(_x0, cons(_x1, _x2)))]] [[if!fac6220min#(true, cons(_x0, cons(_x1, _x2)))]] = 8 + 3x0 + 9x1 + 9x2 > 3 + 3x0 + 3x2 = [[min#(cons(_x0, _x2))]] [[if!fac6220min#(false, cons(_x0, cons(_x1, _x2)))]] = 8 + 3x0 + 9x1 + 9x2 > 3 + 3x1 + 3x2 = [[min#(cons(_x1, _x2))]] [[le(0, _x0)]] = 6 + x0 >= 0 = [[true]] [[le(s(_x0), 0)]] = 9 + 4x0 >= 0 = [[false]] [[le(s(_x0), s(_x1))]] = 9 + 2x1 + 4x0 >= x1 + 2x0 = [[le(_x0, _x1)]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_3, R_0) by ({}, R_0). By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed. 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(le#) = 1 Thus, we can orient the dependency pairs as follows: nu(le#(s(X), s(Y))) = s(X) |> X = nu(le#(X, Y)) By [FuhKop19, Thm. 61], we may replace a dependency pair problem (P_2, R_0, computable, f) by ({}, R_0, computable, 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, 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(eq#) = 1 Thus, we can orient the dependency pairs as follows: nu(eq#(s(X), s(Y))) = s(X) |> X = nu(eq#(X, 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.