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