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 rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): 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 use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[false]] = _|_ [[fork(x_1, x_2, x_3)]] = fork(x_3, x_1, x_2) [[if(x_1, x_2, x_3)]] = if(x_1, x_3, x_2) [[true]] = _|_ We choose Lex = {fork, if} and Mul = {0, eq, lt, member, null, s}, and the following precedence: 0 > fork > lt = member > eq > if > null > s Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: lt(s(X), s(Y)) >= lt(X, Y) lt(0, s(X)) > _|_ lt(X, 0) > _|_ eq(X, X) >= _|_ eq(s(X), 0) >= _|_ eq(0, s(X)) > _|_ member(X, null) >= _|_ member(X, fork(Y, Z, U)) >= if(lt(X, Z), member(X, Y), if(eq(X, Z), _|_, member(X, U))) With these choices, we have: 1] lt(s(X), s(Y)) >= lt(X, Y) because lt in Mul, [2] and [5], by (Fun) 2] s(X) >= X because [3], by (Star) 3] s*(X) >= X because [4], by (Select) 4] X >= X by (Meta) 5] s(Y) >= Y because [6], by (Star) 6] s*(Y) >= Y because [7], by (Select) 7] Y >= Y by (Meta) 8] lt(0, s(X)) > _|_ because [9], by definition 9] lt*(0, s(X)) >= _|_ by (Bot) 10] lt(X, 0) > _|_ because [11], by definition 11] lt*(X, 0) >= _|_ by (Bot) 12] eq(X, X) >= _|_ by (Bot) 13] eq(s(X), 0) >= _|_ by (Bot) 14] eq(0, s(X)) > _|_ because [15], by definition 15] eq*(0, s(X)) >= _|_ by (Bot) 16] member(X, null) >= _|_ by (Bot) 17] member(X, fork(Y, Z, U)) >= if(lt(X, Z), member(X, Y), if(eq(X, Z), _|_, member(X, U))) because [18], by (Star) 18] member*(X, fork(Y, Z, U)) >= if(lt(X, Z), member(X, Y), if(eq(X, Z), _|_, member(X, U))) because member > if, [19], [24] and [28], by (Copy) 19] member*(X, fork(Y, Z, U)) >= lt(X, Z) because member = lt, member in Mul, [20] and [21], by (Stat) 20] X >= X by (Meta) 21] fork(Y, Z, U) > Z because [22], by definition 22] fork*(Y, Z, U) >= Z because [23], by (Select) 23] Z >= Z by (Meta) 24] member*(X, fork(Y, Z, U)) >= member(X, Y) because member in Mul, [20] and [25], by (Stat) 25] fork(Y, Z, U) > Y because [26], by definition 26] fork*(Y, Z, U) >= Y because [27], by (Select) 27] Y >= Y by (Meta) 28] member*(X, fork(Y, Z, U)) >= if(eq(X, Z), _|_, member(X, U)) because member > if, [29], [33] and [34], by (Copy) 29] member*(X, fork(Y, Z, U)) >= eq(X, Z) because member > eq, [30] and [31], by (Copy) 30] member*(X, fork(Y, Z, U)) >= X because [20], by (Select) 31] member*(X, fork(Y, Z, U)) >= Z because [32], by (Select) 32] fork(Y, Z, U) >= Z because [22], by (Star) 33] member*(X, fork(Y, Z, U)) >= _|_ by (Bot) 34] member*(X, fork(Y, Z, U)) >= member(X, U) because member in Mul, [20] and [35], by (Stat) 35] fork(Y, Z, U) > U because [36], by definition 36] fork*(Y, Z, U) >= U because [37], by (Select) 37] U >= U by (Meta) We can thus remove the following rules: lt(0, s(X)) => true lt(X, 0) => false eq(0, s(X)) => false We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): lt(s(X), s(Y)) >? lt(X, Y) eq(X, X) >? true eq(s(X), 0) >? 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 use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[false]] = _|_ [[fork(x_1, x_2, x_3)]] = fork(x_3, x_1, x_2) [[if(x_1, x_2, x_3)]] = if(x_1, x_3, x_2) [[true]] = _|_ We choose Lex = {fork, if} and Mul = {0, eq, lt, member, null, s}, and the following precedence: 0 > fork > lt = member > eq > if > null > s Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: lt(s(X), s(Y)) >= lt(X, Y) eq(X, X) > _|_ eq(s(X), 0) >= _|_ member(X, null) >= _|_ member(X, fork(Y, Z, U)) > if(lt(X, Z), member(X, Y), if(eq(X, Z), _|_, member(X, U))) With these choices, we have: 1] lt(s(X), s(Y)) >= lt(X, Y) because lt in Mul, [2] and [5], by (Fun) 2] s(X) >= X because [3], by (Star) 3] s*(X) >= X because [4], by (Select) 4] X >= X by (Meta) 5] s(Y) >= Y because [6], by (Star) 6] s*(Y) >= Y because [7], by (Select) 7] Y >= Y by (Meta) 8] eq(X, X) > _|_ because [9], by definition 9] eq*(X, X) >= _|_ by (Bot) 10] eq(s(X), 0) >= _|_ by (Bot) 11] member(X, null) >= _|_ by (Bot) 12] member(X, fork(Y, Z, U)) > if(lt(X, Z), member(X, Y), if(eq(X, Z), _|_, member(X, U))) because [13], by definition 13] member*(X, fork(Y, Z, U)) >= if(lt(X, Z), member(X, Y), if(eq(X, Z), _|_, member(X, U))) because member > if, [14], [19] and [23], by (Copy) 14] member*(X, fork(Y, Z, U)) >= lt(X, Z) because member = lt, member in Mul, [15] and [16], by (Stat) 15] X >= X by (Meta) 16] fork(Y, Z, U) > Z because [17], by definition 17] fork*(Y, Z, U) >= Z because [18], by (Select) 18] Z >= Z by (Meta) 19] member*(X, fork(Y, Z, U)) >= member(X, Y) because member in Mul, [15] and [20], by (Stat) 20] fork(Y, Z, U) > Y because [21], by definition 21] fork*(Y, Z, U) >= Y because [22], by (Select) 22] Y >= Y by (Meta) 23] member*(X, fork(Y, Z, U)) >= if(eq(X, Z), _|_, member(X, U)) because member > if, [24], [28] and [29], by (Copy) 24] member*(X, fork(Y, Z, U)) >= eq(X, Z) because member > eq, [25] and [26], by (Copy) 25] member*(X, fork(Y, Z, U)) >= X because [15], by (Select) 26] member*(X, fork(Y, Z, U)) >= Z because [27], by (Select) 27] fork(Y, Z, U) >= Z because [17], by (Star) 28] member*(X, fork(Y, Z, U)) >= _|_ by (Bot) 29] member*(X, fork(Y, Z, U)) >= member(X, U) because member in Mul, [15] and [30], by (Stat) 30] fork(Y, Z, U) > U because [31], by definition 31] fork*(Y, Z, U) >= U because [32], by (Select) 32] U >= U by (Meta) We can thus remove the following rules: eq(X, X) => true member(X, fork(Y, Z, U)) => if(lt(X, Z), member(X, Y), if(eq(X, Z), true, member(X, U))) We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): lt(s(X), s(Y)) >? lt(X, Y) eq(s(X), 0) >? false member(X, null) >? false We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 3 eq = Lam[y0;y1].3 + 3*y0 + 3*y1 false = 0 lt = Lam[y0;y1].2*y0 + 2*y1 member = Lam[y0;y1].3 + 2*y0 + 3*y1 null = 3 s = Lam[y0].3 + 3*y0 Using this interpretation, the requirements translate to: [[lt(s(_x0), s(_x1))]] = 12 + 6*x0 + 6*x1 > 2*x0 + 2*x1 = [[lt(_x0, _x1)]] [[eq(s(_x0), 0)]] = 21 + 9*x0 > 0 = [[false]] [[member(_x0, null)]] = 12 + 2*x0 > 0 = [[false]] We can thus remove the following rules: lt(s(X), s(Y)) => lt(X, Y) eq(s(X), 0) => false member(X, null) => false All rules were succesfully removed. Thus, termination of the original system has been reduced to termination of the beta-rule, which is well-known to hold. +++ Citations +++ [Kop12] C. Kop. Higher Order Termination. PhD Thesis, 2012.