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]] = _|_ [[true]] = _|_ We choose Lex = {} and Mul = {0, eq, fork, if, lt, member, null, s}, and the following precedence: s > member > if > fork > null > 0 > eq > lt 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 [2], by (Star) 2] lt*(s(X), s(Y)) >= lt(X, Y) because lt in Mul, [3] and [6], by (Stat) 3] s(X) >= X because [4], by (Star) 4] s*(X) >= X because [5], by (Select) 5] X >= X by (Meta) 6] s(Y) > Y because [7], by definition 7] s*(Y) >= Y because [8], by (Select) 8] Y >= Y by (Meta) 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)) >= _|_ by (Bot) 15] member(X, null) >= _|_ by (Bot) 16] member(X, fork(Y, Z, U)) >= if(lt(X, Z), member(X, Y), if(eq(X, Z), _|_, member(X, U))) because [17], by (Star) 17] member*(X, fork(Y, Z, U)) >= if(lt(X, Z), member(X, Y), if(eq(X, Z), _|_, member(X, U))) because member > if, [18], [25] and [30], by (Copy) 18] member*(X, fork(Y, Z, U)) >= lt(X, Z) because member > lt, [19] and [21], by (Copy) 19] member*(X, fork(Y, Z, U)) >= X because [20], by (Select) 20] X >= X by (Meta) 21] member*(X, fork(Y, Z, U)) >= Z because [22], by (Select) 22] fork(Y, Z, U) >= Z because [23], by (Star) 23] fork*(Y, Z, U) >= Z because [24], by (Select) 24] Z >= Z by (Meta) 25] member*(X, fork(Y, Z, U)) >= member(X, Y) because member in Mul, [26] and [27], by (Stat) 26] X >= X by (Meta) 27] fork(Y, Z, U) > Y because [28], by definition 28] fork*(Y, Z, U) >= Y because [29], by (Select) 29] Y >= Y by (Meta) 30] member*(X, fork(Y, Z, U)) >= if(eq(X, Z), _|_, member(X, U)) because member > if, [31], [32] and [33], by (Copy) 31] member*(X, fork(Y, Z, U)) >= eq(X, Z) because member > eq, [19] and [21], by (Copy) 32] member*(X, fork(Y, Z, U)) >= _|_ by (Bot) 33] member*(X, fork(Y, Z, U)) >= member(X, U) because member in Mul, [26] and [34], by (Stat) 34] fork(Y, Z, U) > U because [35], by definition 35] fork*(Y, Z, U) >= U because [36], by (Select) 36] U >= U by (Meta) We can thus remove the following rules: lt(X, 0) => 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) lt(0, s(X)) >? true 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]] = _|_ [[true]] = _|_ We choose Lex = {} and Mul = {0, eq, fork, if, lt, member, null, s}, and the following precedence: null > lt = member > 0 > eq > s > fork > if 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)) >= _|_ 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 [2], by (Star) 2] lt*(s(X), s(Y)) >= lt(X, Y) because lt in Mul, [3] and [6], by (Stat) 3] s(X) >= X because [4], by (Star) 4] s*(X) >= X because [5], by (Select) 5] X >= X by (Meta) 6] s(Y) > Y because [7], by definition 7] s*(Y) >= Y because [8], by (Select) 8] Y >= Y by (Meta) 9] lt(0, s(X)) >= _|_ by (Bot) 10] eq(X, X) >= _|_ by (Bot) 11] eq(s(X), 0) >= _|_ by (Bot) 12] eq(0, s(X)) > _|_ because [13], by definition 13] eq*(0, s(X)) >= _|_ by (Bot) 14] member(X, null) >= _|_ by (Bot) 15] member(X, fork(Y, Z, U)) >= if(lt(X, Z), member(X, Y), if(eq(X, Z), _|_, member(X, U))) because [16], by (Star) 16] member*(X, fork(Y, Z, U)) >= if(lt(X, Z), member(X, Y), if(eq(X, Z), _|_, member(X, U))) because member > if, [17], [22] and [26], by (Copy) 17] member*(X, fork(Y, Z, U)) >= lt(X, Z) because member = lt, member in Mul, [18] and [19], by (Stat) 18] X >= X by (Meta) 19] fork(Y, Z, U) > Z because [20], by definition 20] fork*(Y, Z, U) >= Z because [21], by (Select) 21] Z >= Z by (Meta) 22] member*(X, fork(Y, Z, U)) >= member(X, Y) because member in Mul, [18] and [23], by (Stat) 23] fork(Y, Z, U) > Y because [24], by definition 24] fork*(Y, Z, U) >= Y because [25], by (Select) 25] Y >= Y by (Meta) 26] member*(X, fork(Y, Z, U)) >= if(eq(X, Z), _|_, member(X, U)) because member > if, [27], [31] and [32], by (Copy) 27] member*(X, fork(Y, Z, U)) >= eq(X, Z) because member > eq, [28] and [29], by (Copy) 28] member*(X, fork(Y, Z, U)) >= X because [18], by (Select) 29] member*(X, fork(Y, Z, U)) >= Z because [30], by (Select) 30] fork(Y, Z, U) >= Z because [20], by (Star) 31] member*(X, fork(Y, Z, U)) >= _|_ by (Bot) 32] member*(X, fork(Y, Z, U)) >= member(X, U) because member in Mul, [18] and [33], by (Stat) 33] fork(Y, Z, U) > U because [34], by definition 34] fork*(Y, Z, U) >= U because [35], by (Select) 35] U >= U by (Meta) We can thus remove the following rules: 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) lt(0, s(X)) >? true 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]] = _|_ [[true]] = _|_ We choose Lex = {} and Mul = {0, eq, fork, if, lt, member, null, s}, and the following precedence: s > fork > member > lt > eq > if > 0 > null 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)) >= _|_ 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 [2], by (Star) 2] lt*(s(X), s(Y)) >= lt(X, Y) because lt in Mul, [3] and [6], by (Stat) 3] s(X) >= X because [4], by (Star) 4] s*(X) >= X because [5], by (Select) 5] X >= X by (Meta) 6] s(Y) > Y because [7], by definition 7] s*(Y) >= Y because [8], by (Select) 8] Y >= Y by (Meta) 9] lt(0, s(X)) >= _|_ by (Bot) 10] eq(X, X) > _|_ because [11], by definition 11] eq*(X, X) >= _|_ by (Bot) 12] eq(s(X), 0) >= _|_ by (Bot) 13] member(X, null) >= _|_ by (Bot) 14] member(X, fork(Y, Z, U)) > if(lt(X, Z), member(X, Y), if(eq(X, Z), _|_, member(X, U))) because [15], by definition 15] member*(X, fork(Y, Z, U)) >= if(lt(X, Z), member(X, Y), if(eq(X, Z), _|_, member(X, U))) because member > if, [16], [23] and [28], by (Copy) 16] member*(X, fork(Y, Z, U)) >= lt(X, Z) because member > lt, [17] and [19], by (Copy) 17] member*(X, fork(Y, Z, U)) >= X because [18], by (Select) 18] X >= X by (Meta) 19] member*(X, fork(Y, Z, U)) >= Z because [20], by (Select) 20] fork(Y, Z, U) >= Z because [21], by (Star) 21] fork*(Y, Z, U) >= Z because [22], by (Select) 22] Z >= Z by (Meta) 23] member*(X, fork(Y, Z, U)) >= member(X, Y) because member in Mul, [24] and [25], by (Stat) 24] X >= X by (Meta) 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], [30] and [31], by (Copy) 29] member*(X, fork(Y, Z, U)) >= eq(X, Z) because member > eq, [17] and [19], by (Copy) 30] member*(X, fork(Y, Z, U)) >= _|_ by (Bot) 31] member*(X, fork(Y, Z, U)) >= member(X, U) because member in Mul, [24] and [32], by (Stat) 32] fork(Y, Z, U) > U because [33], by definition 33] fork*(Y, Z, U) >= U because [34], by (Select) 34] 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) lt(0, s(X)) >? true eq(s(X), 0) >? false member(X, null) >? false We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[false]] = _|_ [[true]] = _|_ We choose Lex = {} and Mul = {0, eq, lt, member, null, s}, and the following precedence: 0 > s > lt > eq > null > member 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)) >= _|_ eq(s(X), 0) >= _|_ member(X, null) >= _|_ With these choices, we have: 1] lt(s(X), s(Y)) > lt(X, Y) because [2], by definition 2] lt*(s(X), s(Y)) >= lt(X, Y) because lt in Mul, [3] and [6], by (Stat) 3] s(X) > X because [4], by definition 4] s*(X) >= X because [5], by (Select) 5] X >= X by (Meta) 6] s(Y) >= Y because [7], by (Star) 7] s*(Y) >= Y because [8], by (Select) 8] Y >= Y by (Meta) 9] lt(0, s(X)) >= _|_ by (Bot) 10] eq(s(X), 0) >= _|_ by (Bot) 11] member(X, null) >= _|_ by (Bot) We can thus remove the following rules: lt(s(X), s(Y)) => lt(X, Y) 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(0, s(X)) >? true eq(s(X), 0) >? false member(X, null) >? false We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[false]] = _|_ [[s(x_1)]] = x_1 [[true]] = _|_ We choose Lex = {} and Mul = {0, eq, lt, member, null}, and the following precedence: 0 > eq > lt > null > member Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: lt(0, X) > _|_ eq(X, 0) >= _|_ member(X, null) >= _|_ With these choices, we have: 1] lt(0, X) > _|_ because [2], by definition 2] lt*(0, X) >= _|_ by (Bot) 3] eq(X, 0) >= _|_ by (Bot) 4] member(X, null) >= _|_ by (Bot) We can thus remove the following rules: lt(0, s(X)) => true We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): eq(s(X), 0) >? false member(X, null) >? false We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[false]] = _|_ [[s(x_1)]] = x_1 We choose Lex = {} and Mul = {0, eq, member, null}, and the following precedence: 0 > eq > member > null Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: eq(X, 0) > _|_ member(X, null) >= _|_ With these choices, we have: 1] eq(X, 0) > _|_ because [2], by definition 2] eq*(X, 0) >= _|_ by (Bot) 3] member(X, null) >= _|_ by (Bot) We can thus remove the following rules: eq(s(X), 0) => 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]): member(X, null) >? false We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[false]] = _|_ We choose Lex = {} and Mul = {member, null}, and the following precedence: member > null Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: member(X, null) > _|_ With these choices, we have: 1] member(X, null) > _|_ because [2], by definition 2] member*(X, null) >= _|_ by (Bot) We can thus remove the following rules: 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.