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