We consider the system kop11cai1. Alphabet: 0 : [] --> nat cons : [nat * list] --> list map : [nat -> nat * list] --> list nil : [] --> list op : [nat -> nat * nat -> nat] --> nat -> nat pow : [nat -> nat * nat] --> nat -> nat s : [nat] --> nat Rules: map(f, nil) => nil map(f, cons(x, y)) => cons(f x, map(f, y)) pow(f, 0) => /\x.x pow(f, s(x)) => op(f, pow(f, x)) op(f, g) x => f (g x) /\x.f x => f Using the transformations described in [Kop11], this system can be brought in a form without leading free variables in the left-hand side, and where the left-hand side of a variable is always a functional term or application headed by a functional term. We now transform the resulting AFS into an AFSM by replacing all free variables by meta-variables (with arity 0). This leads to the following AFSM: Alphabet: 0 : [] --> nat cons : [nat * list] --> list map : [nat -> nat * list] --> list nil : [] --> list op : [nat -> nat * nat -> nat] --> nat -> nat pow : [nat -> nat * nat] --> nat -> nat s : [nat] --> nat ~AP1 : [nat -> nat * nat] --> nat ~L1 : [nat -> nat] --> nat -> nat Rules: map(F, nil) => nil map(F, cons(X, Y)) => cons(~AP1(F, X), map(F, Y)) pow(F, 0) => ~L1(/\x.x) pow(F, s(X)) => op(F, pow(F, X)) op(F, G) X => ~AP1(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) => F ~L1(/\x.op(F, G) x) => op(F, G) ~AP1(F, X) => F X ~L1(F) => F We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): map(F, nil) >? nil map(F, cons(X, Y)) >? cons(~AP1(F, X), map(F, Y)) pow(F, 0) >? ~L1(/\x.x) pow(F, s(X)) >? op(F, pow(F, X)) op(F, G) X >? ~AP1(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) >? F ~L1(/\x.op(F, G) x) >? op(F, G) ~AP1(F, X) >? F X ~L1(F) >? F We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[nil]] = _|_ We choose Lex = {} and Mul = {0, @_{o -> o}, cons, map, op, pow, s, ~AP1, ~L1}, and the following precedence: pow > s > 0 > map > ~L1 > op > cons > ~AP1 > @_{o -> o} Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: map(F, _|_) >= _|_ map(F, cons(X, Y)) > cons(~AP1(F, X), map(F, Y)) pow(F, 0) >= ~L1(/\x.x) pow(F, s(X)) >= op(F, pow(F, X)) @_{o -> o}(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) >= F ~L1(/\x.@_{o -> o}(op(F, G), x)) > op(F, G) ~AP1(F, X) >= @_{o -> o}(F, X) ~L1(F) >= F With these choices, we have: 1] map(F, _|_) >= _|_ by (Bot) 2] map(F, cons(X, Y)) > cons(~AP1(F, X), map(F, Y)) because [3], by definition 3] map*(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) because map > cons, [4] and [11], by (Copy) 4] map*(F, cons(X, Y)) >= ~AP1(F, X) because map > ~AP1, [5] and [7], by (Copy) 5] map*(F, cons(X, Y)) >= F because [6], by (Select) 6] F >= F by (Meta) 7] map*(F, cons(X, Y)) >= X because [8], by (Select) 8] cons(X, Y) >= X because [9], by (Star) 9] cons*(X, Y) >= X because [10], by (Select) 10] X >= X by (Meta) 11] map*(F, cons(X, Y)) >= map(F, Y) because map in Mul, [12] and [13], by (Stat) 12] F >= F by (Meta) 13] cons(X, Y) > Y because [14], by definition 14] cons*(X, Y) >= Y because [15], by (Select) 15] Y >= Y by (Meta) 16] pow(F, 0) >= ~L1(/\x.x) because [17], by (Star) 17] pow*(F, 0) >= ~L1(/\x.x) because pow > ~L1 and [18], by (Copy) 18] pow*(F, 0) >= /\y.y because [19], by (F-Abs) 19] pow*(F, 0, x) >= x because [20], by (Select) 20] x >= x by (Var) 21] pow(F, s(X)) >= op(F, pow(F, X)) because [22], by (Star) 22] pow*(F, s(X)) >= op(F, pow(F, X)) because pow > op, [23] and [25], by (Copy) 23] pow*(F, s(X)) >= F because [24], by (Select) 24] F >= F by (Meta) 25] pow*(F, s(X)) >= pow(F, X) because pow in Mul, [26] and [27], by (Stat) 26] F >= F by (Meta) 27] s(X) > X because [28], by definition 28] s*(X) >= X because [29], by (Select) 29] X >= X by (Meta) 30] @_{o -> o}(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [31], by (Star) 31] @_{o -> o}*(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [32], by (Select) 32] op(F, G) @_{o -> o}*(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [33] 33] op*(F, G, @_{o -> o}*(op(F, G), X)) >= ~AP1(F, ~AP1(G, X)) because op > ~AP1, [34] and [36], by (Copy) 34] op*(F, G, @_{o -> o}*(op(F, G), X)) >= F because [35], by (Select) 35] F >= F by (Meta) 36] op*(F, G, @_{o -> o}*(op(F, G), X)) >= ~AP1(G, X) because op > ~AP1, [37] and [39], by (Copy) 37] op*(F, G, @_{o -> o}*(op(F, G), X)) >= G because [38], by (Select) 38] G >= G by (Meta) 39] op*(F, G, @_{o -> o}*(op(F, G), X)) >= X because [40], by (Select) 40] @_{o -> o}*(op(F, G), X) >= X because [41], by (Select) 41] X >= X by (Meta) 42] ~L1(/\x.~AP1(F, x)) >= F because [43], by (Star) 43] ~L1*(/\x.~AP1(F, x)) >= F because [44], by (Select) 44] /\x.~AP1(F, x) >= F because [45], by (Eta)[Kop13:2] 45] F >= F by (Meta) 46] ~L1(/\x.@_{o -> o}(op(F, G), x)) > op(F, G) because [47], by definition 47] ~L1*(/\x.@_{o -> o}(op(F, G), x)) >= op(F, G) because ~L1 > op, [48] and [53], by (Copy) 48] ~L1*(/\x.@_{o -> o}(op(F, G), x)) >= F because [49], by (Select) 49] /\x.@_{o -> o}(op(F, G), x) >= F because [50], by (Eta)[Kop13:2] 50] op(F, G) >= F because [51], by (Star) 51] op*(F, G) >= F because [52], by (Select) 52] F >= F by (Meta) 53] ~L1*(/\x.@_{o -> o}(op(F, G), x)) >= G because [54], by (Select) 54] /\x.@_{o -> o}(op(F, G), x) >= G because [55], by (Eta)[Kop13:2] 55] op(F, G) >= G because [56], by (Star) 56] op*(F, G) >= G because [57], by (Select) 57] G >= G by (Meta) 58] ~AP1(F, X) >= @_{o -> o}(F, X) because [59], by (Star) 59] ~AP1*(F, X) >= @_{o -> o}(F, X) because ~AP1 > @_{o -> o}, [60] and [62], by (Copy) 60] ~AP1*(F, X) >= F because [61], by (Select) 61] F >= F by (Meta) 62] ~AP1*(F, X) >= X because [63], by (Select) 63] X >= X by (Meta) 64] ~L1(F) >= F because [65], by (Star) 65] ~L1*(F) >= F because [66], by (Select) 66] F >= F by (Meta) We can thus remove the following rules: map(F, cons(X, Y)) => cons(~AP1(F, X), map(F, Y)) ~L1(/\x.op(F, G) x) => op(F, G) We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): map(F, nil) >? nil pow(F, 0) >? ~L1(/\x.x) pow(F, s(X)) >? op(F, pow(F, X)) op(F, G) X >? ~AP1(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) >? F ~AP1(F, X) >? F X ~L1(F) >? F We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[nil]] = _|_ [[~L1(x_1)]] = x_1 We choose Lex = {} and Mul = {0, @_{o -> o}, map, op, pow, s, ~AP1}, and the following precedence: 0 > pow > op > @_{o -> o} = ~AP1 > map > s Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: map(F, _|_) >= _|_ pow(F, 0) >= /\x.x pow(F, s(X)) >= op(F, pow(F, X)) @_{o -> o}(op(F, G), X) > ~AP1(F, ~AP1(G, X)) /\x.~AP1(F, x) >= F ~AP1(F, X) >= @_{o -> o}(F, X) F >= F With these choices, we have: 1] map(F, _|_) >= _|_ by (Bot) 2] pow(F, 0) >= /\x.x because [3], by (Star) 3] pow*(F, 0) >= /\y.y because [4], by (F-Abs) 4] pow*(F, 0, x) >= x because [5], by (Select) 5] x >= x by (Var) 6] pow(F, s(X)) >= op(F, pow(F, X)) because [7], by (Star) 7] pow*(F, s(X)) >= op(F, pow(F, X)) because pow > op, [8] and [10], by (Copy) 8] pow*(F, s(X)) >= F because [9], by (Select) 9] F >= F by (Meta) 10] pow*(F, s(X)) >= pow(F, X) because pow in Mul, [11] and [12], by (Stat) 11] F >= F by (Meta) 12] s(X) > X because [13], by definition 13] s*(X) >= X because [14], by (Select) 14] X >= X by (Meta) 15] @_{o -> o}(op(F, G), X) > ~AP1(F, ~AP1(G, X)) because [16], by definition 16] @_{o -> o}*(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [17], by (Select) 17] op(F, G) @_{o -> o}*(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [18] 18] op*(F, G, @_{o -> o}*(op(F, G), X)) >= ~AP1(F, ~AP1(G, X)) because op > ~AP1, [19] and [21], by (Copy) 19] op*(F, G, @_{o -> o}*(op(F, G), X)) >= F because [20], by (Select) 20] F >= F by (Meta) 21] op*(F, G, @_{o -> o}*(op(F, G), X)) >= ~AP1(G, X) because op > ~AP1, [22] and [24], by (Copy) 22] op*(F, G, @_{o -> o}*(op(F, G), X)) >= G because [23], by (Select) 23] G >= G by (Meta) 24] op*(F, G, @_{o -> o}*(op(F, G), X)) >= X because [25], by (Select) 25] @_{o -> o}*(op(F, G), X) >= X because [26], by (Select) 26] X >= X by (Meta) 27] /\x.~AP1(F, x) >= F because [28], by (Eta)[Kop13:2] 28] F >= F by (Meta) 29] ~AP1(F, X) >= @_{o -> o}(F, X) because ~AP1 = @_{o -> o}, ~AP1 in Mul, [30] and [31], by (Fun) 30] F >= F by (Meta) 31] X >= X by (Meta) 32] F >= F by (Meta) We can thus remove the following rules: op(F, G) X => ~AP1(F, ~AP1(G, 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]): map(F, nil) >? nil pow(F, 0) >? ~L1(/\x.x) pow(F, s(X)) >? op(F, pow(F, X)) ~L1(/\x.~AP1(F, x)) >? F ~AP1(F, X) >? F X ~L1(F) >? F We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[nil]] = _|_ [[~L1(x_1)]] = x_1 We choose Lex = {} and Mul = {0, @_{o -> o}, map, op, pow, s, ~AP1}, and the following precedence: map > ~AP1 > @_{o -> o} > s > pow > 0 > op Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: map(F, _|_) >= _|_ pow(F, 0) > /\x.x pow(F, s(X)) >= op(F, pow(F, X)) /\x.~AP1(F, x) > F ~AP1(F, X) > @_{o -> o}(F, X) F >= F With these choices, we have: 1] map(F, _|_) >= _|_ by (Bot) 2] pow(F, 0) > /\x.x because [3], by definition 3] pow*(F, 0) >= /\y.y because [4], by (F-Abs) 4] pow*(F, 0, x) >= x because [5], by (Select) 5] x >= x by (Var) 6] pow(F, s(X)) >= op(F, pow(F, X)) because [7], by (Star) 7] pow*(F, s(X)) >= op(F, pow(F, X)) because pow > op, [8] and [10], by (Copy) 8] pow*(F, s(X)) >= F because [9], by (Select) 9] F >= F by (Meta) 10] pow*(F, s(X)) >= pow(F, X) because pow in Mul, [11] and [12], by (Stat) 11] F >= F by (Meta) 12] s(X) > X because [13], by definition 13] s*(X) >= X because [14], by (Select) 14] X >= X by (Meta) 15] /\x.~AP1(F, x) > F because [16], by definition 16] /\x.~AP1*(F, x) >= F because [17], by (Eta)[Kop13:2] 17] F >= F by (Meta) 18] ~AP1(F, X) > @_{o -> o}(F, X) because [19], by definition 19] ~AP1*(F, X) >= @_{o -> o}(F, X) because ~AP1 > @_{o -> o}, [20] and [22], by (Copy) 20] ~AP1*(F, X) >= F because [21], by (Select) 21] F >= F by (Meta) 22] ~AP1*(F, X) >= X because [23], by (Select) 23] X >= X by (Meta) 24] F >= F by (Meta) We can thus remove the following rules: pow(F, 0) => ~L1(/\x.x) ~L1(/\x.~AP1(F, x)) => F ~AP1(F, X) => F 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]): map(F, nil) >? nil pow(F, s(X)) >? op(F, pow(F, X)) ~L1(F) >? F We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[nil]] = _|_ We choose Lex = {} and Mul = {map, op, pow, s, ~L1}, and the following precedence: pow > s > op > map > ~L1 Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: map(F, _|_) > _|_ pow(F, s(X)) >= op(F, pow(F, X)) ~L1(F) >= F With these choices, we have: 1] map(F, _|_) > _|_ because [2], by definition 2] map*(F, _|_) >= _|_ by (Bot) 3] pow(F, s(X)) >= op(F, pow(F, X)) because [4], by (Star) 4] pow*(F, s(X)) >= op(F, pow(F, X)) because pow > op, [5] and [7], by (Copy) 5] pow*(F, s(X)) >= F because [6], by (Select) 6] F >= F by (Meta) 7] pow*(F, s(X)) >= pow(F, X) because pow in Mul, [8] and [9], by (Stat) 8] F >= F by (Meta) 9] s(X) > X because [10], by definition 10] s*(X) >= X because [11], by (Select) 11] X >= X by (Meta) 12] ~L1(F) >= F because [13], by (Star) 13] ~L1*(F) >= F because [14], by (Select) 14] F >= F by (Meta) We can thus remove the following rules: map(F, nil) => nil We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): pow(F, s(X)) >? op(F, pow(F, X)) ~L1(F) >? F We use a recursive path ordering as defined in [Kop12, Chapter 5]. We choose Lex = {} and Mul = {op, pow, s, ~L1}, and the following precedence: ~L1 > pow > op > s With these choices, we have: 1] pow(F, s(X)) >= op(F, pow(F, X)) because [2], by (Star) 2] pow*(F, s(X)) >= op(F, pow(F, X)) because pow > op, [3] and [5], by (Copy) 3] pow*(F, s(X)) >= F because [4], by (Select) 4] F >= F by (Meta) 5] pow*(F, s(X)) >= pow(F, X) because pow in Mul, [6] and [7], by (Stat) 6] F >= F by (Meta) 7] s(X) > X because [8], by definition 8] s*(X) >= X because [9], by (Select) 9] X >= X by (Meta) 10] ~L1(F) > F because [11], by definition 11] ~L1*(F) >= F because [12], by (Select) 12] F >= F by (Meta) We can thus remove the following rules: ~L1(F) => F We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): pow(F, s(X)) >? op(F, pow(F, X)) We use a recursive path ordering as defined in [Kop12, Chapter 5]. We choose Lex = {} and Mul = {op, pow, s}, and the following precedence: pow > op > s With these choices, we have: 1] pow(F, s(X)) > op(F, pow(F, X)) because [2], by definition 2] pow*(F, s(X)) >= op(F, pow(F, X)) because pow > op, [3] and [5], by (Copy) 3] pow*(F, s(X)) >= F because [4], by (Select) 4] F >= F by (Meta) 5] pow*(F, s(X)) >= pow(F, X) because pow in Mul, [6] and [7], by (Stat) 6] F >= F by (Meta) 7] s(X) > X because [8], by definition 8] s*(X) >= X because [9], by (Select) 9] X >= X by (Meta) We can thus remove the following rules: pow(F, s(X)) => op(F, pow(F, 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 +++ [Kop11] C. Kop. Simplifying Algebraic Functional Systems. In Proceedings of CAI 2011, volume 6742 of LNCS. 201--215, Springer, 2011. [Kop12] C. Kop. Higher Order Termination. PhD Thesis, 2012. [Kop13:2] C. Kop. StarHorpo with an Eta-Rule. Unpublished manuscript, http://cl-informatik.uibk.ac.at/users/kop/etahorpo.pdf, 2013.