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: [[nil]] = _|_ We choose Lex = {} and Mul = {0, @_{o -> o}, cons, double, inc, map, plus, s, times}, and the following precedence: double > inc > map > times > 0 > plus > @_{o -> o} > cons > s Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: @_{o -> o}(plus(0), X) >= X @_{o -> o}(plus(s(X)), Y) > s(@_{o -> o}(plus(X), Y)) @_{o -> o}(times(0), X) >= 0 @_{o -> o}(times(s(X)), Y) >= @_{o -> o}(plus(@_{o -> o}(times(X), Y)), Y) @_{o -> o}(map(F), _|_) >= _|_ @_{o -> o}(map(F), cons(X, Y)) >= cons(@_{o -> o}(F, X), @_{o -> o}(map(F), Y)) inc >= map(plus(s(0))) double >= map(times(s(s(0)))) With these choices, we have: 1] @_{o -> o}(plus(0), X) >= X because [2], by (Star) 2] @_{o -> o}*(plus(0), 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 definition 5] @_{o -> o}*(plus(s(X)), Y) >= s(@_{o -> o}(plus(X), Y)) because @_{o -> o} > s and [6], by (Copy) 6] @_{o -> o}*(plus(s(X)), Y) >= @_{o -> o}(plus(X), Y) because [7], by (Select) 7] plus(s(X)) @_{o -> o}*(plus(s(X)), Y) >= @_{o -> o}(plus(X), Y) because [8] 8] plus*(s(X), @_{o -> o}*(plus(s(X)), Y)) >= @_{o -> o}(plus(X), Y) because plus > @_{o -> o}, [9] and [13], by (Copy) 9] plus*(s(X), @_{o -> o}*(plus(s(X)), Y)) >= plus(X) because plus in Mul and [10], by (Stat) 10] s(X) > X because [11], by definition 11] s*(X) >= X because [12], by (Select) 12] X >= X by (Meta) 13] plus*(s(X), @_{o -> o}*(plus(s(X)), Y)) >= Y because [14], by (Select) 14] @_{o -> o}*(plus(s(X)), Y) >= Y because [15], by (Select) 15] Y >= Y by (Meta) 16] @_{o -> o}(times(0), X) >= 0 because [17], by (Star) 17] @_{o -> o}*(times(0), X) >= 0 because [18], by (Select) 18] times(0) @_{o -> o}*(times(0), X) >= 0 because [19] 19] times*(0, @_{o -> o}*(times(0), X)) >= 0 because times > 0, by (Copy) 20] @_{o -> o}(times(s(X)), Y) >= @_{o -> o}(plus(@_{o -> o}(times(X), Y)), Y) because [21], by (Star) 21] @_{o -> o}*(times(s(X)), Y) >= @_{o -> o}(plus(@_{o -> o}(times(X), Y)), Y) because [22], by (Select) 22] times(s(X)) @_{o -> o}*(times(s(X)), Y) >= @_{o -> o}(plus(@_{o -> o}(times(X), Y)), Y) because [23] 23] times*(s(X), @_{o -> o}*(times(s(X)), Y)) >= @_{o -> o}(plus(@_{o -> o}(times(X), Y)), Y) because times > @_{o -> o}, [24] and [30], by (Copy) 24] times*(s(X), @_{o -> o}*(times(s(X)), Y)) >= plus(@_{o -> o}(times(X), Y)) because times > plus and [25], by (Copy) 25] times*(s(X), @_{o -> o}*(times(s(X)), Y)) >= @_{o -> o}(times(X), Y) because times > @_{o -> o}, [26] and [30], by (Copy) 26] times*(s(X), @_{o -> o}*(times(s(X)), Y)) >= times(X) because times in Mul and [27], by (Stat) 27] s(X) > X because [28], by definition 28] s*(X) >= X because [29], by (Select) 29] X >= X by (Meta) 30] times*(s(X), @_{o -> o}*(times(s(X)), Y)) >= Y because [31], by (Select) 31] @_{o -> o}*(times(s(X)), Y) >= Y because [32], by (Select) 32] times(s(X)) @_{o -> o}*(times(s(X)), Y) >= Y because [33] 33] times*(s(X), @_{o -> o}*(times(s(X)), Y)) >= Y because [34], by (Select) 34] @_{o -> o}*(times(s(X)), Y) >= Y because [35], by (Select) 35] Y >= Y by (Meta) 36] @_{o -> o}(map(F), _|_) >= _|_ by (Bot) 37] @_{o -> o}(map(F), cons(X, Y)) >= cons(@_{o -> o}(F, X), @_{o -> o}(map(F), Y)) because [38], by (Star) 38] @_{o -> o}*(map(F), cons(X, Y)) >= cons(@_{o -> o}(F, X), @_{o -> o}(map(F), Y)) because @_{o -> o} > cons, [39] and [49], by (Copy) 39] @_{o -> o}*(map(F), cons(X, Y)) >= @_{o -> o}(F, X) because [40], by (Select) 40] map(F) @_{o -> o}*(map(F), cons(X, Y)) >= @_{o -> o}(F, X) because [41] 41] map*(F, @_{o -> o}*(map(F), cons(X, Y))) >= @_{o -> o}(F, X) because map > @_{o -> o}, [42] and [44], by (Copy) 42] map*(F, @_{o -> o}*(map(F), cons(X, Y))) >= F because [43], by (Select) 43] F >= F by (Meta) 44] map*(F, @_{o -> o}*(map(F), cons(X, Y))) >= X because [45], by (Select) 45] @_{o -> o}*(map(F), cons(X, Y)) >= X because [46], by (Select) 46] cons(X, Y) >= X because [47], by (Star) 47] cons*(X, Y) >= X because [48], by (Select) 48] X >= X by (Meta) 49] @_{o -> o}*(map(F), cons(X, Y)) >= @_{o -> o}(map(F), Y) because @_{o -> o} in Mul, [50] and [52], by (Stat) 50] map(F) >= map(F) because map in Mul and [51], by (Fun) 51] F >= F by (Meta) 52] cons(X, Y) > Y because [53], by definition 53] cons*(X, Y) >= Y because [54], by (Select) 54] Y >= Y by (Meta) 55] inc >= map(plus(s(0))) because [56], by (Star) 56] inc* >= map(plus(s(0))) because inc > map and [57], by (Copy) 57] inc* >= plus(s(0)) because inc > plus and [58], by (Copy) 58] inc* >= s(0) because inc > s and [59], by (Copy) 59] inc* >= 0 because inc > 0, by (Copy) 60] double >= map(times(s(s(0)))) because [61], by (Star) 61] double* >= map(times(s(s(0)))) because double > map and [62], by (Copy) 62] double* >= times(s(s(0))) because double > times and [63], by (Copy) 63] double* >= s(s(0)) because double > s and [64], by (Copy) 64] double* >= s(0) because double > s and [65], by (Copy) 65] double* >= 0 because double > 0, by (Copy) We can thus remove the following rules: plus(s(X)) Y => s(plus(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]): 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) 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]] = _|_ [[nil]] = _|_ We choose Lex = {} and Mul = {@_{o -> o}, cons, double, inc, map, plus, s, times}, and the following precedence: double > inc > map > s > cons > times > plus > @_{o -> o} 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}(times(_|_), X) >= _|_ @_{o -> o}(times(s(X)), Y) >= @_{o -> o}(plus(@_{o -> o}(times(X), Y)), Y) @_{o -> o}(map(F), _|_) > _|_ @_{o -> o}(map(F), cons(X, Y)) > cons(@_{o -> o}(F, X), @_{o -> o}(map(F), Y)) inc > map(plus(s(_|_))) double > map(times(s(s(_|_)))) With these choices, we have: 1] @_{o -> o}(plus(_|_), X) >= X because [2], by (Star) 2] @_{o -> o}*(plus(_|_), X) >= X because [3], by (Select) 3] X >= X by (Meta) 4] @_{o -> o}(times(_|_), X) >= _|_ by (Bot) 5] @_{o -> o}(times(s(X)), Y) >= @_{o -> o}(plus(@_{o -> o}(times(X), Y)), Y) because [6], by (Star) 6] @_{o -> o}*(times(s(X)), Y) >= @_{o -> o}(plus(@_{o -> o}(times(X), Y)), Y) because [7], by (Select) 7] times(s(X)) @_{o -> o}*(times(s(X)), Y) >= @_{o -> o}(plus(@_{o -> o}(times(X), Y)), Y) because [8] 8] times*(s(X), @_{o -> o}*(times(s(X)), Y)) >= @_{o -> o}(plus(@_{o -> o}(times(X), Y)), Y) because times > @_{o -> o}, [9] and [15], by (Copy) 9] times*(s(X), @_{o -> o}*(times(s(X)), Y)) >= plus(@_{o -> o}(times(X), Y)) because times > plus and [10], by (Copy) 10] times*(s(X), @_{o -> o}*(times(s(X)), Y)) >= @_{o -> o}(times(X), Y) because times > @_{o -> o}, [11] and [15], by (Copy) 11] times*(s(X), @_{o -> o}*(times(s(X)), Y)) >= times(X) because times 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] times*(s(X), @_{o -> o}*(times(s(X)), Y)) >= Y because [16], by (Select) 16] @_{o -> o}*(times(s(X)), Y) >= Y because [17], by (Select) 17] Y >= Y by (Meta) 18] @_{o -> o}(map(F), _|_) > _|_ because [19], by definition 19] @_{o -> o}*(map(F), _|_) >= _|_ by (Bot) 20] @_{o -> o}(map(F), cons(X, Y)) > cons(@_{o -> o}(F, X), @_{o -> o}(map(F), Y)) because [21], by definition 21] @_{o -> o}*(map(F), cons(X, Y)) >= cons(@_{o -> o}(F, X), @_{o -> o}(map(F), Y)) because [22], by (Select) 22] map(F) @_{o -> o}*(map(F), cons(X, Y)) >= cons(@_{o -> o}(F, X), @_{o -> o}(map(F), Y)) because [23] 23] map*(F, @_{o -> o}*(map(F), cons(X, Y))) >= cons(@_{o -> o}(F, X), @_{o -> o}(map(F), Y)) because map > cons, [24] and [32], by (Copy) 24] map*(F, @_{o -> o}*(map(F), cons(X, Y))) >= @_{o -> o}(F, X) because [25], by (Select) 25] @_{o -> o}*(map(F), cons(X, Y)) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [26] and [29], by (Stat) 26] map(F) > F because [27], by definition 27] map*(F) >= F because [28], by (Select) 28] F >= F by (Meta) 29] cons(X, Y) >= X because [30], by (Star) 30] cons*(X, Y) >= X because [31], by (Select) 31] X >= X by (Meta) 32] map*(F, @_{o -> o}*(map(F), cons(X, Y))) >= @_{o -> o}(map(F), Y) because [33], by (Select) 33] @_{o -> o}*(map(F), cons(X, Y)) >= @_{o -> o}(map(F), Y) because @_{o -> o} in Mul, [34] and [36], by (Stat) 34] map(F) >= map(F) because map in Mul and [35], by (Fun) 35] F >= F by (Meta) 36] cons(X, Y) > Y because [37], by definition 37] cons*(X, Y) >= Y because [38], by (Select) 38] Y >= Y by (Meta) 39] inc > map(plus(s(_|_))) because [40], by definition 40] inc* >= map(plus(s(_|_))) because inc > map and [41], by (Copy) 41] inc* >= plus(s(_|_)) because inc > plus and [42], by (Copy) 42] inc* >= s(_|_) because inc > s and [43], by (Copy) 43] inc* >= _|_ by (Bot) 44] double > map(times(s(s(_|_)))) because [45], by definition 45] double* >= map(times(s(s(_|_)))) because double > map and [46], by (Copy) 46] double* >= times(s(s(_|_))) because double > times and [47], by (Copy) 47] double* >= s(s(_|_)) because double > s and [48], by (Copy) 48] double* >= s(_|_) because double > s and [49], by (Copy) 49] double* >= _|_ by (Bot) We can thus remove the following rules: 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 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 times(0, X) >? 0 times(s(X), Y) >? plus(times(X, Y), Y) We use a recursive path ordering as defined in [Kop12, Chapter 5]. We choose Lex = {} and Mul = {0, plus, s, times}, and the following precedence: times > s > 0 > plus With these choices, we have: 1] plus(0, X) >= X because [2], by (Star) 2] plus*(0, X) >= X because [3], by (Select) 3] X >= X by (Meta) 4] times(0, X) >= 0 because [5], by (Star) 5] times*(0, X) >= 0 because times > 0, by (Copy) 6] times(s(X), Y) > plus(times(X, Y), Y) because [7], by definition 7] times*(s(X), Y) >= plus(times(X, Y), Y) because times > plus, [8] and [13], by (Copy) 8] times*(s(X), Y) >= times(X, Y) because times in Mul, [9] and [12], by (Stat) 9] s(X) > X because [10], by definition 10] s*(X) >= X because [11], by (Select) 11] X >= X by (Meta) 12] Y >= Y by (Meta) 13] times*(s(X), Y) >= Y because [12], by (Select) We can thus remove the following rules: times(s(X), Y) => plus(times(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(0, X) >? X times(0, X) >? 0 We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ We choose Lex = {} and Mul = {plus, times}, and the following precedence: plus > times Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: plus(_|_, X) > X times(_|_, X) >= _|_ 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] times(_|_, X) >= _|_ by (Bot) We can thus remove the following rules: plus(0, X) => 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]): times(0, X) >? 0 We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ We choose Lex = {} and Mul = {times}, and the following precedence: times Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: times(_|_, X) > _|_ With these choices, we have: 1] times(_|_, X) > _|_ because [2], by definition 2] times*(_|_, X) >= _|_ by (Bot) We can thus remove the following rules: times(0, X) => 0 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.