We consider the system h50. Alphabet: 0 : [] --> nat plus : [nat * nat] --> nat rec : [nat * nat * nat -> nat -> nat] --> nat s : [nat] --> nat succ : [] --> nat -> nat -> nat xap : [nat -> nat -> nat * nat] --> nat -> nat yap : [nat -> nat * nat] --> nat Rules: rec(0, x, /\y./\z.yap(xap(f, y), z)) => x rec(s(x), y, /\z./\u.yap(xap(f, z), u)) => yap(xap(f, x), rec(x, y, /\v./\w.yap(xap(f, v), w))) succ x y => s(y) plus(x, y) => rec(x, y, succ) xap(f, x) => f x yap(f, x) => f x This AFS is converted to an AFSM simply by replacing all free variables by meta-variables (with arity 0). Symbol xap is an encoding for application that is only used in innocuous ways. We can simplify the program (without losing non-termination) by removing it. This gives: Alphabet: 0 : [] --> nat plus : [nat * nat] --> nat rec : [nat * nat * nat -> nat -> nat] --> nat s : [nat] --> nat succ : [] --> nat -> nat -> nat yap : [nat -> nat * nat] --> nat Rules: rec(0, X, /\x./\y.yap(F(x), y)) => X rec(s(X), Y, /\x./\y.yap(F(x), y)) => yap(F(X), rec(X, Y, /\z./\u.yap(F(z), u))) succ X Y => s(Y) plus(X, Y) => rec(X, Y, succ) yap(F, X) => F 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]): rec(0, X, /\x./\y.yap(F(x), y)) >? X rec(s(X), Y, /\x./\y.yap(F(x), y)) >? yap(F(X), rec(X, Y, /\z./\u.yap(F(z), u))) succ X Y >? s(Y) plus(X, Y) >? rec(X, Y, succ) yap(F, X) >? F X We use a recursive path ordering as defined in [Kop12, Chapter 5]. We choose Lex = {} and Mul = {0, @_{o -> o -> o}, @_{o -> o}, plus, rec, s, succ, yap}, and the following precedence: @_{o -> o -> o} > plus > rec > @_{o -> o} = yap > succ > 0 > s With these choices, we have: 1] rec(0, X, /\x./\y.yap(F(x), y)) > X because [2], by definition 2] rec*(0, X, /\x./\y.yap(F(x), y)) >= X because [3], by (Select) 3] X >= X by (Meta) 4] rec(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) because [5], by (Star) 5] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) because rec > yap, [6] and [13], by (Copy) 6] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= F(X) because [7], by (Select) 7] /\x.yap(F(rec*(s(X), Y, /\y./\z.yap(F(y), z))), x) >= F(X) because [8], by (Eta)[Kop13:2] 8] F(rec*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(X) because [9], by (Meta) 9] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= X because [10], by (Select) 10] s(X) >= X because [11], by (Star) 11] s*(X) >= X because [12], by (Select) 12] X >= X by (Meta) 13] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= rec(X, Y, /\x./\y.yap(F(x), y)) because rec in Mul, [14], [16] and [17], by (Stat) 14] s(X) > X because [15], by definition 15] s*(X) >= X because [12], by (Select) 16] Y >= Y by (Meta) 17] /\x./\z.yap(F(x), z) >= /\x./\z.yap(F(x), z) because [18], by (Abs) 18] /\z.yap(F(y), z) >= /\z.yap(F(y), z) because [19], by (Abs) 19] yap(F(y), x) >= yap(F(y), x) because yap in Mul, [20] and [22], by (Fun) 20] F(y) >= F(y) because [21], by (Meta) 21] y >= y by (Var) 22] x >= x by (Var) 23] @_{o -> o}(@_{o -> o -> o}(succ, X), Y) >= s(Y) because [24], by (Star) 24] @_{o -> o}*(@_{o -> o -> o}(succ, X), Y) >= s(Y) because @_{o -> o} > s and [25], by (Copy) 25] @_{o -> o}*(@_{o -> o -> o}(succ, X), Y) >= Y because [26], by (Select) 26] Y >= Y by (Meta) 27] plus(X, Y) > rec(X, Y, succ) because [28], by definition 28] plus*(X, Y) >= rec(X, Y, succ) because plus > rec, [29], [31] and [33], by (Copy) 29] plus*(X, Y) >= X because [30], by (Select) 30] X >= X by (Meta) 31] plus*(X, Y) >= Y because [32], by (Select) 32] Y >= Y by (Meta) 33] plus*(X, Y) >= succ because plus > succ, by (Copy) 34] yap(F, X) >= @_{o -> o}(F, X) because yap = @_{o -> o}, yap in Mul, [35] and [36], by (Fun) 35] F >= F by (Meta) 36] X >= X by (Meta) We can thus remove the following rules: rec(0, X, /\x./\y.yap(F(x), y)) => X plus(X, Y) => rec(X, Y, succ) We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): rec(s(X), Y, /\x./\y.yap(F(x), y)) >? yap(F(X), rec(X, Y, /\z./\u.yap(F(z), u))) succ(X, Y) >? s(Y) yap(F, X) >? F X We use a recursive path ordering as defined in [Kop12, Chapter 5]. We choose Lex = {} and Mul = {@_{o -> o}, rec, s, succ, yap}, and the following precedence: rec > yap > @_{o -> o} = succ > s With these choices, we have: 1] rec(s(X), Y, /\x./\y.yap(F(x), y)) > yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) because [2], by definition 2] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) because rec > yap, [3] and [10], by (Copy) 3] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= F(X) because [4], by (Select) 4] /\x.yap(F(rec*(s(X), Y, /\y./\z.yap(F(y), z))), x) >= F(X) because [5], by (Eta)[Kop13:2] 5] F(rec*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(X) because [6], by (Meta) 6] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= X because [7], by (Select) 7] s(X) >= X because [8], by (Star) 8] s*(X) >= X because [9], by (Select) 9] X >= X by (Meta) 10] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= rec(X, Y, /\x./\y.yap(F(x), y)) because rec in Mul, [11], [13] and [14], by (Stat) 11] s(X) > X because [12], by definition 12] s*(X) >= X because [9], by (Select) 13] Y >= Y by (Meta) 14] /\x./\z.yap(F(x), z) >= /\x./\z.yap(F(x), z) because [15], by (Abs) 15] /\z.yap(F(y), z) >= /\z.yap(F(y), z) because [16], by (Abs) 16] yap(F(y), x) >= yap(F(y), x) because yap in Mul, [17] and [19], by (Fun) 17] F(y) >= F(y) because [18], by (Meta) 18] y >= y by (Var) 19] x >= x by (Var) 20] succ(X, Y) >= s(Y) because [21], by (Star) 21] succ*(X, Y) >= s(Y) because succ > s and [22], by (Copy) 22] succ*(X, Y) >= Y because [23], by (Select) 23] Y >= Y by (Meta) 24] yap(F, X) > @_{o -> o}(F, X) because [25], by definition 25] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [26] and [28], by (Copy) 26] yap*(F, X) >= F because [27], by (Select) 27] F >= F by (Meta) 28] yap*(F, X) >= X because [29], by (Select) 29] X >= X by (Meta) We can thus remove the following rules: rec(s(X), Y, /\x./\y.yap(F(x), y)) => yap(F(X), rec(X, Y, /\z./\u.yap(F(z), u))) yap(F, X) => F 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]): succ(X, Y) >? s(Y) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[s(x_1)]] = x_1 We choose Lex = {} and Mul = {succ}, and the following precedence: succ Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: succ(X, Y) > Y With these choices, we have: 1] succ(X, Y) > Y because [2], by definition 2] succ*(X, Y) >= Y because [3], by (Select) 3] Y >= Y by (Meta) We can thus remove the following rules: succ(X, Y) => s(Y) 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. [Kop13:2] C. Kop. StarHorpo with an Eta-Rule. Unpublished manuscript, http://cl-informatik.uibk.ac.at/users/kop/etahorpo.pdf, 2013.