We consider the system h60. Alphabet: 0 : [] --> nat rec : [nat * a * nat -> a -> a] --> a s : [nat] --> nat xap : [nat -> a -> a * nat] --> a -> a yap : [a -> a * a] --> a 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))) 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 rec : [nat * a * nat -> a -> a] --> a s : [nat] --> nat yap : [a -> a * a] --> a 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))) 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))) 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}, rec, s, yap}, and the following precedence: rec > 0 > yap > @_{o -> o} > 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] yap(F, X) >= @_{o -> o}(F, X) because [24], by (Star) 24] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [25] and [27], by (Copy) 25] yap*(F, X) >= F because [26], by (Select) 26] F >= F by (Meta) 27] yap*(F, X) >= X because [28], by (Select) 28] X >= X by (Meta) We can thus remove the following rules: rec(0, X, /\x./\y.yap(F(x), y)) => 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(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 a recursive path ordering as defined in [Kop12, Chapter 5]. We choose Lex = {} and Mul = {@_{o -> o}, rec, s, yap}, and the following precedence: rec > s > yap > @_{o -> o} 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 (Star) 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] yap(F, X) > @_{o -> o}(F, X) because [21], by definition 21] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [22] and [24], by (Copy) 22] yap*(F, X) >= F because [23], by (Select) 23] F >= F by (Meta) 24] yap*(F, X) >= X because [25], by (Select) 25] X >= X by (Meta) We can thus remove the following rules: 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(s(X), Y, /\x./\y.yap(F(x), y)) >? yap(F(X), rec(X, Y, /\z./\u.yap(F(z), u))) We use a recursive path ordering as defined in [Kop12, Chapter 5]. We choose Lex = {} and Mul = {rec, s, yap}, and the following precedence: rec > yap > 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) 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))) 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.