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