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