We consider the system 1037. Alphabet: 0 : [] --> nat rec : [nat * nat * nat -> nat -> nat] --> nat s : [nat] --> nat v : [var] --> nat xplus : [nat * nat] --> nat xtimes : [nat * nat] --> nat Rules: xplus(X, 0) => X xplus(X, s(Y)) => s(xplus(X, Y)) rec(0, X, /\x./\y.Y(x, y)) => X rec(s(v(X)), Y, /\x./\y.Z(x, y)) => Z(v(X), rec(v(X), Y, /\z./\u.Z(z, u))) xtimes(X, Y) => rec(Y, 0, /\x./\y.xplus(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]): xplus(X, 0) >? X xplus(X, s(Y)) >? s(xplus(X, Y)) rec(0, X, /\x./\y.Y(x, y)) >? X rec(s(v(X)), Y, /\x./\y.Z(x, y)) >? Z(v(X), rec(v(X), Y, /\z./\u.Z(z, u))) xtimes(X, Y) >? rec(Y, 0, /\x./\y.xplus(X, y)) We use a recursive path ordering as defined in [Kop12, Chapter 5]. We choose Lex = {} and Mul = {0, rec, s, v, xplus, xtimes}, and the following precedence: 0 = xtimes > rec > xplus > s > v With these choices, we have: 1] xplus(X, 0) >= X because [2], by (Star) 2] xplus*(X, 0) >= X because [3], by (Select) 3] X >= X by (Meta) 4] xplus(X, s(Y)) > s(xplus(X, Y)) because [5], by definition 5] xplus*(X, s(Y)) >= s(xplus(X, Y)) because xplus > s and [6], by (Copy) 6] xplus*(X, s(Y)) >= xplus(X, Y) because xplus in Mul, [7] and [8], by (Stat) 7] X >= X by (Meta) 8] s(Y) > Y because [9], by definition 9] s*(Y) >= Y because [10], by (Select) 10] Y >= Y by (Meta) 11] rec(0, X, /\x./\y.Y(x, y)) >= X because [12], by (Star) 12] rec*(0, X, /\x./\y.Y(x, y)) >= X because [13], by (Select) 13] X >= X by (Meta) 14] rec(s(v(X)), Y, /\x./\y.Z(x, y)) > Z(v(X), rec(v(X), Y, /\x./\y.Z(x, y))) because [15], by definition 15] rec*(s(v(X)), Y, /\x./\y.Z(x, y)) >= Z(v(X), rec(v(X), Y, /\x./\y.Z(x, y))) because [16], by (Select) 16] Z(rec*(s(v(X)), Y, /\x./\y.Z(x, y)), rec*(s(v(X)), Y, /\z./\u.Z(z, u))) >= Z(v(X), rec(v(X), Y, /\x./\y.Z(x, y))) because [17] and [22], by (Meta) 17] rec*(s(v(X)), Y, /\x./\y.Z(x, y)) >= v(X) because [18], by (Select) 18] s(v(X)) >= v(X) because [19], by (Star) 19] s*(v(X)) >= v(X) because [20], by (Select) 20] v(X) >= v(X) because v in Mul and [21], by (Fun) 21] X >= X by (Meta) 22] rec*(s(v(X)), Y, /\x./\y.Z(x, y)) >= rec(v(X), Y, /\x./\y.Z(x, y)) because rec in Mul, [23], [25] and [26], by (Stat) 23] s(v(X)) > v(X) because [24], by definition 24] s*(v(X)) >= v(X) because [20], by (Select) 25] Y >= Y by (Meta) 26] /\x./\z.Z(x, z) >= /\x./\z.Z(x, z) because [27], by (Abs) 27] /\z.Z(y, z) >= /\z.Z(y, z) because [28], by (Abs) 28] Z(y, x) >= Z(y, x) because [29] and [30], by (Meta) 29] y >= y by (Var) 30] x >= x by (Var) 31] xtimes(X, Y) >= rec(Y, 0, /\x./\y.xplus(X, y)) because [32], by (Star) 32] xtimes*(X, Y) >= rec(Y, 0, /\x./\y.xplus(X, y)) because xtimes > rec, [33], [35] and [36], by (Copy) 33] xtimes*(X, Y) >= Y because [34], by (Select) 34] Y >= Y by (Meta) 35] xtimes*(X, Y) >= 0 because xtimes = 0 and xtimes in Mul, by (Stat) 36] xtimes*(X, Y) >= /\y./\z.xplus(X, z) because [37], by (F-Abs) 37] xtimes*(X, Y, x) >= /\z.xplus(X, z) because [38], by (F-Abs) 38] xtimes*(X, Y, x, y) >= xplus(X, y) because xtimes > xplus, [39] and [41], by (Copy) 39] xtimes*(X, Y, x, y) >= X because [40], by (Select) 40] X >= X by (Meta) 41] xtimes*(X, Y, x, y) >= y because [42], by (Select) 42] y >= y by (Var) We can thus remove the following rules: xplus(X, s(Y)) => s(xplus(X, Y)) rec(s(v(X)), Y, /\x./\y.Z(x, y)) => Z(v(X), rec(v(X), Y, /\z./\u.Z(z, 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]): xplus(X, 0) >? X rec(0, X, /\x./\y.Y(x, y)) >? X xtimes(X, Y) >? rec(Y, 0, /\x./\y.xplus(X, y)) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ We choose Lex = {} and Mul = {rec, xplus, xtimes}, and the following precedence: xtimes > rec > xplus Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: xplus(X, _|_) >= X rec(_|_, X, /\x./\y.Y(x, y)) >= X xtimes(X, Y) > rec(Y, _|_, /\x./\y.xplus(X, y)) With these choices, we have: 1] xplus(X, _|_) >= X because [2], by (Star) 2] xplus*(X, _|_) >= X because [3], by (Select) 3] X >= X by (Meta) 4] rec(_|_, X, /\x./\y.Y(x, y)) >= X because [5], by (Star) 5] rec*(_|_, X, /\x./\y.Y(x, y)) >= X because [6], by (Select) 6] X >= X by (Meta) 7] xtimes(X, Y) > rec(Y, _|_, /\x./\y.xplus(X, y)) because [8], by definition 8] xtimes*(X, Y) >= rec(Y, _|_, /\x./\y.xplus(X, y)) because xtimes > rec, [9], [11] and [12], by (Copy) 9] xtimes*(X, Y) >= Y because [10], by (Select) 10] Y >= Y by (Meta) 11] xtimes*(X, Y) >= _|_ by (Bot) 12] xtimes*(X, Y) >= /\y./\z.xplus(X, z) because [13], by (F-Abs) 13] xtimes*(X, Y, x) >= /\z.xplus(X, z) because [14], by (F-Abs) 14] xtimes*(X, Y, x, y) >= xplus(X, y) because xtimes > xplus, [15] and [17], by (Copy) 15] xtimes*(X, Y, x, y) >= X because [16], by (Select) 16] X >= X by (Meta) 17] xtimes*(X, Y, x, y) >= y because [18], by (Select) 18] y >= y by (Var) We can thus remove the following rules: xtimes(X, Y) => rec(Y, 0, /\x./\y.xplus(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]): xplus(X, 0) >? X rec(0, X, /\x./\y.Y(x, y)) >? X We use a recursive path ordering as defined in [Kop12, Chapter 5]. We choose Lex = {} and Mul = {0, rec, xplus}, and the following precedence: rec > xplus > 0 With these choices, we have: 1] xplus(X, 0) > X because [2], by definition 2] xplus*(X, 0) >= X because [3], by (Select) 3] X >= X by (Meta) 4] rec(0, X, /\x./\y.Y(x, y)) >= X because [5], by (Star) 5] rec*(0, X, /\x./\y.Y(x, y)) >= X because [6], by (Select) 6] X >= X by (Meta) We can thus remove the following rules: xplus(X, 0) => 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.Y(x, y)) >? X We use a recursive path ordering as defined in [Kop12, Chapter 5]. We choose Lex = {} and Mul = {0, rec}, and the following precedence: 0 > rec With these choices, we have: 1] rec(0, X, /\x./\y.Y(x, y)) > X because [2], by definition 2] rec*(0, X, /\x./\y.Y(x, y)) >= X because [3], by (Select) 3] X >= X by (Meta) We can thus remove the following rules: rec(0, X, /\x./\y.Y(x, y)) => 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.