We consider the system AotoYamada_05__Ex5TermProof. Alphabet: 0 : [] --> a add : [a * a] --> a fact : [] --> a -> a mult : [] --> a -> a -> a rec : [a -> a -> a * a] --> a -> a s : [a] --> a Rules: add(0, x) => x add(s(x), y) => s(add(x, y)) mult 0 x => 0 mult s(x) y => add(mult x y, y) rec(f, x) 0 => x rec(f, x) s(y) => f s(y) (rec(f, x) y) fact => rec(mult, s(0)) 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]): add(0, X) >? X add(s(X), Y) >? s(add(X, Y)) mult 0 X >? 0 mult s(X) Y >? add(mult X Y, Y) rec(F, X) 0 >? X rec(F, X) s(Y) >? F s(Y) (rec(F, X) Y) fact >? rec(mult, s(0)) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[add(x_1, x_2)]] = add(x_2, x_1) [[rec(x_1, x_2)]] = rec(x_2, x_1) We choose Lex = {add, fact, rec, s} and Mul = {@_{o -> o -> o}, @_{o -> o}, mult}, and the following precedence: fact > mult > rec > @_{o -> o -> o} > add > s > @_{o -> o} Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: add(_|_, X) >= X add(s(X), Y) >= s(add(X, Y)) @_{o -> o}(@_{o -> o -> o}(mult, _|_), X) > _|_ @_{o -> o}(@_{o -> o -> o}(mult, s(X)), Y) > add(@_{o -> o}(@_{o -> o -> o}(mult, X), Y), Y) @_{o -> o}(rec(F, X), _|_) > X @_{o -> o}(rec(F, X), s(Y)) >= @_{o -> o}(@_{o -> o -> o}(F, s(Y)), @_{o -> o}(rec(F, X), Y)) fact >= rec(mult, s(_|_)) With these choices, we have: 1] add(_|_, X) >= X because [2], by (Star) 2] add*(_|_, X) >= X because [3], by (Select) 3] X >= X by (Meta) 4] add(s(X), Y) >= s(add(X, Y)) because [5], by (Star) 5] add*(s(X), Y) >= s(add(X, Y)) because add > s and [6], by (Copy) 6] add*(s(X), Y) >= add(X, Y) because [7], [10], [11] and [13], by (Stat) 7] s(X) > X because [8], by definition 8] s*(X) >= X because [9], by (Select) 9] X >= X by (Meta) 10] Y >= Y by (Meta) 11] add*(s(X), Y) >= X because [12], by (Select) 12] s(X) >= X because [8], by (Star) 13] add*(s(X), Y) >= Y because [10], by (Select) 14] @_{o -> o}(@_{o -> o -> o}(mult, _|_), X) > _|_ because [15], by definition 15] @_{o -> o}*(@_{o -> o -> o}(mult, _|_), X) >= _|_ by (Bot) 16] @_{o -> o}(@_{o -> o -> o}(mult, s(X)), Y) > add(@_{o -> o}(@_{o -> o -> o}(mult, X), Y), Y) because [17], by definition 17] @_{o -> o}*(@_{o -> o -> o}(mult, s(X)), Y) >= add(@_{o -> o}(@_{o -> o -> o}(mult, X), Y), Y) because [18], by (Select) 18] @_{o -> o -> o}(mult, s(X)) @_{o -> o}*(@_{o -> o -> o}(mult, s(X)), Y) >= add(@_{o -> o}(@_{o -> o -> o}(mult, X), Y), Y) because [19] 19] @_{o -> o -> o}*(mult, s(X), @_{o -> o}*(@_{o -> o -> o}(mult, s(X)), Y)) >= add(@_{o -> o}(@_{o -> o -> o}(mult, X), Y), Y) because [20], by (Select) 20] mult @_{o -> o -> o}*(mult, s(X), @_{o -> o}*(@_{o -> o -> o}(mult, s(X)), Y)) @_{o -> o -> o}*(mult, s(X), @_{o -> o}*(@_{o -> o -> o}(mult, s(X)), Y)) >= add(@_{o -> o}(@_{o -> o -> o}(mult, X), Y), Y) because [21] 21] mult*(@_{o -> o -> o}*(mult, s(X), @_{o -> o}*(@_{o -> o -> o}(mult, s(X)), Y)), @_{o -> o -> o}*(mult, s(X), @_{o -> o}*(@_{o -> o -> o}(mult, s(X)), Y))) >= add(@_{o -> o}(@_{o -> o -> o}(mult, X), Y), Y) because mult > add, [22] and [32], by (Copy) 22] mult*(@_{o -> o -> o}*(mult, s(X), @_{o -> o}*(@_{o -> o -> o}(mult, s(X)), Y)), @_{o -> o -> o}*(mult, s(X), @_{o -> o}*(@_{o -> o -> o}(mult, s(X)), Y))) >= @_{o -> o}(@_{o -> o -> o}(mult, X), Y) because [23], by (Select) 23] @_{o -> o -> o}*(mult, s(X), @_{o -> o}*(@_{o -> o -> o}(mult, s(X)), Y)) >= @_{o -> o}(@_{o -> o -> o}(mult, X), Y) because @_{o -> o -> o} > @_{o -> o}, [24] and [29], by (Copy) 24] @_{o -> o -> o}*(mult, s(X), @_{o -> o}*(@_{o -> o -> o}(mult, s(X)), Y)) >= @_{o -> o -> o}(mult, X) because @_{o -> o -> o} in Mul, [25] and [26], by (Stat) 25] mult >= mult by (Fun) 26] s(X) > X because [27], by definition 27] s*(X) >= X because [28], by (Select) 28] X >= X by (Meta) 29] @_{o -> o -> o}*(mult, s(X), @_{o -> o}*(@_{o -> o -> o}(mult, s(X)), Y)) >= Y because [30], by (Select) 30] @_{o -> o}*(@_{o -> o -> o}(mult, s(X)), Y) >= Y because [31], by (Select) 31] Y >= Y by (Meta) 32] mult*(@_{o -> o -> o}*(mult, s(X), @_{o -> o}*(@_{o -> o -> o}(mult, s(X)), Y)), @_{o -> o -> o}*(mult, s(X), @_{o -> o}*(@_{o -> o -> o}(mult, s(X)), Y))) >= Y because [29], by (Select) 33] @_{o -> o}(rec(F, X), _|_) > X because [34], by definition 34] @_{o -> o}*(rec(F, X), _|_) >= X because [35], by (Select) 35] rec(F, X) @_{o -> o}*(rec(F, X), _|_) >= X because [36] 36] rec*(F, X, @_{o -> o}*(rec(F, X), _|_)) >= X because [37], by (Select) 37] @_{o -> o}*(rec(F, X), _|_) >= X because [38], by (Select) 38] rec(F, X) @_{o -> o}*(rec(F, X), _|_) >= X because [39] 39] rec*(F, X, @_{o -> o}*(rec(F, X), _|_)) >= X because [40], by (Select) 40] X >= X by (Meta) 41] @_{o -> o}(rec(F, X), s(Y)) >= @_{o -> o}(@_{o -> o -> o}(F, s(Y)), @_{o -> o}(rec(F, X), Y)) because [42], by (Star) 42] @_{o -> o}*(rec(F, X), s(Y)) >= @_{o -> o}(@_{o -> o -> o}(F, s(Y)), @_{o -> o}(rec(F, X), Y)) because [43], by (Select) 43] rec(F, X) @_{o -> o}*(rec(F, X), s(Y)) >= @_{o -> o}(@_{o -> o -> o}(F, s(Y)), @_{o -> o}(rec(F, X), Y)) because [44] 44] rec*(F, X, @_{o -> o}*(rec(F, X), s(Y))) >= @_{o -> o}(@_{o -> o -> o}(F, s(Y)), @_{o -> o}(rec(F, X), Y)) because rec > @_{o -> o}, [45] and [52], by (Copy) 45] rec*(F, X, @_{o -> o}*(rec(F, X), s(Y))) >= @_{o -> o -> o}(F, s(Y)) because rec > @_{o -> o -> o}, [46] and [48], by (Copy) 46] rec*(F, X, @_{o -> o}*(rec(F, X), s(Y))) >= F because [47], by (Select) 47] F >= F by (Meta) 48] rec*(F, X, @_{o -> o}*(rec(F, X), s(Y))) >= s(Y) because [49], by (Select) 49] @_{o -> o}*(rec(F, X), s(Y)) >= s(Y) because [50], by (Select) 50] s(Y) >= s(Y) because [51], by (Fun) 51] Y >= Y by (Meta) 52] rec*(F, X, @_{o -> o}*(rec(F, X), s(Y))) >= @_{o -> o}(rec(F, X), Y) because [53], by (Select) 53] @_{o -> o}*(rec(F, X), s(Y)) >= @_{o -> o}(rec(F, X), Y) because @_{o -> o} in Mul, [54] and [57], by (Stat) 54] rec(F, X) >= rec(F, X) because [55] and [56], by (Fun) 55] F >= F by (Meta) 56] X >= X by (Meta) 57] s(Y) > Y because [58], by definition 58] s*(Y) >= Y because [51], by (Select) 59] fact >= rec(mult, s(_|_)) because [60], by (Star) 60] fact* >= rec(mult, s(_|_)) because fact > rec, [61] and [62], by (Copy) 61] fact* >= mult because fact > mult, by (Copy) 62] fact* >= s(_|_) because fact > s and [63], by (Copy) 63] fact* >= _|_ by (Bot) We can thus remove the following rules: mult 0 X => 0 mult s(X) Y => add(mult X Y, Y) rec(F, 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]): add(0, X) >? X add(s(X), Y) >? s(add(X, Y)) rec(F, X) s(Y) >? F s(Y) (rec(F, X) Y) fact >? rec(mult, s(0)) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[mult]] = _|_ [[rec(x_1, x_2)]] = rec(x_2, x_1) We choose Lex = {rec} and Mul = {@_{o -> o -> o}, @_{o -> o}, add, fact, s}, and the following precedence: add > fact > rec > @_{o -> o -> o} > @_{o -> o} > s Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: add(_|_, X) > X add(s(X), Y) >= s(add(X, Y)) @_{o -> o}(rec(F, X), s(Y)) >= @_{o -> o}(@_{o -> o -> o}(F, s(Y)), @_{o -> o}(rec(F, X), Y)) fact > rec(_|_, s(_|_)) With these choices, we have: 1] add(_|_, X) > X because [2], by definition 2] add*(_|_, X) >= X because [3], by (Select) 3] X >= X by (Meta) 4] add(s(X), Y) >= s(add(X, Y)) because [5], by (Star) 5] add*(s(X), Y) >= s(add(X, Y)) because add > s and [6], by (Copy) 6] add*(s(X), Y) >= add(X, Y) because add in Mul, [7] and [10], by (Stat) 7] s(X) > X because [8], by definition 8] s*(X) >= X because [9], by (Select) 9] X >= X by (Meta) 10] Y >= Y by (Meta) 11] @_{o -> o}(rec(F, X), s(Y)) >= @_{o -> o}(@_{o -> o -> o}(F, s(Y)), @_{o -> o}(rec(F, X), Y)) because [12], by (Star) 12] @_{o -> o}*(rec(F, X), s(Y)) >= @_{o -> o}(@_{o -> o -> o}(F, s(Y)), @_{o -> o}(rec(F, X), Y)) because [13], by (Select) 13] rec(F, X) @_{o -> o}*(rec(F, X), s(Y)) >= @_{o -> o}(@_{o -> o -> o}(F, s(Y)), @_{o -> o}(rec(F, X), Y)) because [14] 14] rec*(F, X, @_{o -> o}*(rec(F, X), s(Y))) >= @_{o -> o}(@_{o -> o -> o}(F, s(Y)), @_{o -> o}(rec(F, X), Y)) because rec > @_{o -> o}, [15] and [28], by (Copy) 15] rec*(F, X, @_{o -> o}*(rec(F, X), s(Y))) >= @_{o -> o -> o}(F, s(Y)) because rec > @_{o -> o -> o}, [16] and [18], by (Copy) 16] rec*(F, X, @_{o -> o}*(rec(F, X), s(Y))) >= F because [17], by (Select) 17] F >= F by (Meta) 18] rec*(F, X, @_{o -> o}*(rec(F, X), s(Y))) >= s(Y) because [19], by (Select) 19] @_{o -> o}*(rec(F, X), s(Y)) >= s(Y) because [20], by (Select) 20] rec(F, X) @_{o -> o}*(rec(F, X), s(Y)) >= s(Y) because [21] 21] rec*(F, X, @_{o -> o}*(rec(F, X), s(Y))) >= s(Y) because [22], by (Select) 22] @_{o -> o}*(rec(F, X), s(Y)) >= s(Y) because [23], by (Select) 23] rec(F, X) @_{o -> o}*(rec(F, X), s(Y)) >= s(Y) because [24] 24] rec*(F, X, @_{o -> o}*(rec(F, X), s(Y))) >= s(Y) because [25], by (Select) 25] @_{o -> o}*(rec(F, X), s(Y)) >= s(Y) because [26], by (Select) 26] s(Y) >= s(Y) because s in Mul and [27], by (Fun) 27] Y >= Y by (Meta) 28] rec*(F, X, @_{o -> o}*(rec(F, X), s(Y))) >= @_{o -> o}(rec(F, X), Y) because [29], by (Select) 29] @_{o -> o}*(rec(F, X), s(Y)) >= @_{o -> o}(rec(F, X), Y) because @_{o -> o} in Mul, [30] and [33], by (Stat) 30] rec(F, X) >= rec(F, X) because [31] and [32], by (Fun) 31] F >= F by (Meta) 32] X >= X by (Meta) 33] s(Y) > Y because [34], by definition 34] s*(Y) >= Y because [27], by (Select) 35] fact > rec(_|_, s(_|_)) because [36], by definition 36] fact* >= rec(_|_, s(_|_)) because fact > rec, [37] and [38], by (Copy) 37] fact* >= _|_ by (Bot) 38] fact* >= s(_|_) because fact > s and [39], by (Copy) 39] fact* >= _|_ by (Bot) We can thus remove the following rules: add(0, X) => X fact => rec(mult, s(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]): add(s(X), Y) >? s(add(X, Y)) rec(F, X, s(Y)) >? F s(Y) rec(F, X, Y) We use a recursive path ordering as defined in [Kop12, Chapter 5]. We choose Lex = {@_{o -> o}} and Mul = {@_{o -> o -> o}, add, rec, s}, and the following precedence: add > @_{o -> o -> o} = rec > @_{o -> o} > s With these choices, we have: 1] add(s(X), Y) >= s(add(X, Y)) because [2], by (Star) 2] add*(s(X), Y) >= s(add(X, Y)) because add > s and [3], by (Copy) 3] add*(s(X), Y) >= add(X, Y) because add in Mul, [4] and [7], by (Stat) 4] s(X) > X because [5], by definition 5] s*(X) >= X because [6], by (Select) 6] X >= X by (Meta) 7] Y >= Y by (Meta) 8] rec(F, X, s(Y)) > @_{o -> o}(@_{o -> o -> o}(F, s(Y)), rec(F, X, Y)) because [9], by definition 9] rec*(F, X, s(Y)) >= @_{o -> o}(@_{o -> o -> o}(F, s(Y)), rec(F, X, Y)) because rec > @_{o -> o}, [10] and [14], by (Copy) 10] rec*(F, X, s(Y)) >= @_{o -> o -> o}(F, s(Y)) because rec = @_{o -> o -> o}, rec in Mul, [11] and [12], by (Stat) 11] F >= F by (Meta) 12] s(Y) >= s(Y) because s in Mul and [13], by (Fun) 13] Y >= Y by (Meta) 14] rec*(F, X, s(Y)) >= rec(F, X, Y) because rec in Mul, [15], [16], [11], [15] and [16], by (Stat) 15] X >= X by (Meta) 16] s(Y) > Y because [17], by definition 17] s*(Y) >= Y because [13], by (Select) We can thus remove the following rules: rec(F, X, s(Y)) => F s(Y) rec(F, 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]): add(s(X), Y) >? s(add(X, Y)) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: add = Lam[y0;y1].2*y1 + 3*y0 s = Lam[y0].2 + y0 Using this interpretation, the requirements translate to: [[add(s(_x0), _x1)]] = 6 + 2*x1 + 3*x0 > 2 + 2*x1 + 3*x0 = [[s(add(_x0, _x1))]] We can thus remove the following rules: add(s(X), Y) => s(add(X, 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.