We consider the system Applicative_05__BTreeMember. Alphabet: 0 : [] --> a eq : [a * a] --> c false : [] --> c fork : [b * a * b] --> b if : [c * c * c] --> c lt : [a * a] --> c member : [a * b] --> c null : [] --> b s : [a] --> a true : [] --> c Rules: lt(s(x), s(y)) => lt(x, y) lt(0, s(x)) => true lt(x, 0) => false eq(x, x) => true eq(s(x), 0) => false eq(0, s(x)) => false member(x, null) => false member(x, fork(y, z, u)) => if(lt(x, z), member(x, y), if(eq(x, z), true, member(x, u))) 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, all): Dependency Pairs P_0: 0] lt#(s(X), s(Y)) =#> lt#(X, Y) 1] member#(X, fork(Y, Z, U)) =#> lt#(X, Z) 2] member#(X, fork(Y, Z, U)) =#> member#(X, Y) 3] member#(X, fork(Y, Z, U)) =#> eq#(X, Z) 4] member#(X, fork(Y, Z, U)) =#> member#(X, U) Rules R_0: lt(s(X), s(Y)) => lt(X, Y) lt(0, s(X)) => true lt(X, 0) => false eq(X, X) => true eq(s(X), 0) => false eq(0, s(X)) => false member(X, null) => false member(X, fork(Y, Z, U)) => if(lt(X, Z), member(X, Y), if(eq(X, Z), true, member(X, U))) Thus, the original system is terminating if (P_0, R_0, static, all) is finite. We consider the dependency pair problem (P_0, R_0, static, all). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: lt#(s(X), s(Y)) >? lt#(X, Y) member#(X, fork(Y, Z, U)) >? lt#(X, Z) member#(X, fork(Y, Z, U)) >? member#(X, Y) member#(X, fork(Y, Z, U)) >? eq#(X, Z) member#(X, fork(Y, Z, U)) >? member#(X, U) lt(s(X), s(Y)) >= lt(X, Y) lt(0, s(X)) >= true lt(X, 0) >= false eq(X, X) >= true eq(s(X), 0) >= false eq(0, s(X)) >= false member(X, null) >= false member(X, fork(Y, Z, U)) >= if(lt(X, Z), member(X, Y), if(eq(X, Z), true, member(X, U))) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 3 eq = \y0y1.0 eq# = \y0y1.0 false = 0 fork = \y0y1y2.3 if = \y0y1y2.0 lt = \y0y1.0 lt# = \y0y1.0 member = \y0y1.0 member# = \y0y1.3 + 2y0 null = 3 s = \y0.3 true = 0 Using this interpretation, the requirements translate to: [[lt#(s(_x0), s(_x1))]] = 0 >= 0 = [[lt#(_x0, _x1)]] [[member#(_x0, fork(_x1, _x2, _x3))]] = 3 + 2x0 > 0 = [[lt#(_x0, _x2)]] [[member#(_x0, fork(_x1, _x2, _x3))]] = 3 + 2x0 >= 3 + 2x0 = [[member#(_x0, _x1)]] [[member#(_x0, fork(_x1, _x2, _x3))]] = 3 + 2x0 > 0 = [[eq#(_x0, _x2)]] [[member#(_x0, fork(_x1, _x2, _x3))]] = 3 + 2x0 >= 3 + 2x0 = [[member#(_x0, _x3)]] [[lt(s(_x0), s(_x1))]] = 0 >= 0 = [[lt(_x0, _x1)]] [[lt(0, s(_x0))]] = 0 >= 0 = [[true]] [[lt(_x0, 0)]] = 0 >= 0 = [[false]] [[eq(_x0, _x0)]] = 0 >= 0 = [[true]] [[eq(s(_x0), 0)]] = 0 >= 0 = [[false]] [[eq(0, s(_x0))]] = 0 >= 0 = [[false]] [[member(_x0, null)]] = 0 >= 0 = [[false]] [[member(_x0, fork(_x1, _x2, _x3))]] = 0 >= 0 = [[if(lt(_x0, _x2), member(_x0, _x1), if(eq(_x0, _x2), true, member(_x0, _x3)))]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_0, R_0, static, all) by (P_1, R_0, static, all), where P_1 consists of: lt#(s(X), s(Y)) =#> lt#(X, Y) member#(X, fork(Y, Z, U)) =#> member#(X, Y) member#(X, fork(Y, Z, U)) =#> member#(X, U) Thus, the original system is terminating if (P_1, R_0, static, all) is finite. We consider the dependency pair problem (P_1, R_0, static, all). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: lt#(s(X), s(Y)) >? lt#(X, Y) member#(X, fork(Y, Z, U)) >? member#(X, Y) member#(X, fork(Y, Z, U)) >? member#(X, U) lt(s(X), s(Y)) >= lt(X, Y) lt(0, s(X)) >= true lt(X, 0) >= false eq(X, X) >= true eq(s(X), 0) >= false eq(0, s(X)) >= false member(X, null) >= false member(X, fork(Y, Z, U)) >= if(lt(X, Z), member(X, Y), if(eq(X, Z), true, member(X, U))) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 3 eq = \y0y1.0 false = 0 fork = \y0y1y2.3 + y2 + 2y0 if = \y0y1y2.0 lt = \y0y1.0 lt# = \y0y1.y0 + y1 member = \y0y1.0 member# = \y0y1.y1 null = 3 s = \y0.3 + 2y0 true = 0 Using this interpretation, the requirements translate to: [[lt#(s(_x0), s(_x1))]] = 6 + 2x0 + 2x1 > x0 + x1 = [[lt#(_x0, _x1)]] [[member#(_x0, fork(_x1, _x2, _x3))]] = 3 + x3 + 2x1 > x1 = [[member#(_x0, _x1)]] [[member#(_x0, fork(_x1, _x2, _x3))]] = 3 + x3 + 2x1 > x3 = [[member#(_x0, _x3)]] [[lt(s(_x0), s(_x1))]] = 0 >= 0 = [[lt(_x0, _x1)]] [[lt(0, s(_x0))]] = 0 >= 0 = [[true]] [[lt(_x0, 0)]] = 0 >= 0 = [[false]] [[eq(_x0, _x0)]] = 0 >= 0 = [[true]] [[eq(s(_x0), 0)]] = 0 >= 0 = [[false]] [[eq(0, s(_x0))]] = 0 >= 0 = [[false]] [[member(_x0, null)]] = 0 >= 0 = [[false]] [[member(_x0, fork(_x1, _x2, _x3))]] = 0 >= 0 = [[if(lt(_x0, _x2), member(_x0, _x1), if(eq(_x0, _x2), true, member(_x0, _x3)))]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_1, R_0) by ({}, R_0). 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.