We consider the system Applicative_first_order_05__06. Alphabet: cons : [c * d] --> d f : [a] --> a false : [] --> b filter : [c -> b * d] --> d filter2 : [b * c -> b * c * d] --> d g : [a] --> a map : [c -> c * d] --> d nil : [] --> d true : [] --> b Rules: f(g(x)) => g(g(f(x))) f(g(x)) => g(g(g(x))) map(h, nil) => nil map(h, cons(x, y)) => cons(h x, map(h, y)) filter(h, nil) => nil filter(h, cons(x, y)) => filter2(h x, h, x, y) filter2(true, h, x, y) => cons(x, filter(h, y)) filter2(false, h, x, y) => filter(h, y) 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]): f(g(X)) >? g(g(f(X))) f(g(X)) >? g(g(g(X))) map(F, nil) >? nil map(F, cons(X, Y)) >? cons(F X, map(F, Y)) filter(F, nil) >? nil filter(F, cons(X, Y)) >? filter2(F X, F, X, Y) filter2(true, F, X, Y) >? cons(X, filter(F, Y)) filter2(false, F, X, Y) >? filter(F, Y) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[filter(x_1, x_2)]] = filter(x_2, x_1) [[filter2(x_1, x_2, x_3, x_4)]] = filter2(x_4, x_2, x_1, x_3) We choose Lex = {f, filter, filter2} and Mul = {@_{o -> o}, cons, false, g, map, nil, true}, and the following precedence: map > false > f > nil > filter = filter2 > @_{o -> o} > cons > g > true Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: f(g(X)) > g(g(f(X))) f(g(X)) >= g(g(g(X))) map(F, nil) >= nil map(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) filter(F, nil) > nil filter(F, cons(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) filter2(true, F, X, Y) > cons(X, filter(F, Y)) filter2(false, F, X, Y) >= filter(F, Y) With these choices, we have: 1] f(g(X)) > g(g(f(X))) because [2], by definition 2] f*(g(X)) >= g(g(f(X))) because f > g and [3], by (Copy) 3] f*(g(X)) >= g(f(X)) because f > g and [4], by (Copy) 4] f*(g(X)) >= f(X) because [5] and [8], by (Stat) 5] g(X) > X because [6], by definition 6] g*(X) >= X because [7], by (Select) 7] X >= X by (Meta) 8] f*(g(X)) >= X because [9], by (Select) 9] g(X) >= X because [6], by (Star) 10] f(g(X)) >= g(g(g(X))) because [11], by (Star) 11] f*(g(X)) >= g(g(g(X))) because f > g and [12], by (Copy) 12] f*(g(X)) >= g(g(X)) because f > g and [13], by (Copy) 13] f*(g(X)) >= g(X) because f > g and [14], by (Copy) 14] f*(g(X)) >= X because [15], by (Select) 15] g(X) >= X because [16], by (Star) 16] g*(X) >= X because [17], by (Select) 17] X >= X by (Meta) 18] map(F, nil) >= nil because [19], by (Star) 19] map*(F, nil) >= nil because [20], by (Select) 20] nil >= nil by (Fun) 21] map(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) because [22], by (Star) 22] map*(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) because map > cons, [23] and [30], by (Copy) 23] map*(F, cons(X, Y)) >= @_{o -> o}(F, X) because map > @_{o -> o}, [24] and [26], by (Copy) 24] map*(F, cons(X, Y)) >= F because [25], by (Select) 25] F >= F by (Meta) 26] map*(F, cons(X, Y)) >= X because [27], by (Select) 27] cons(X, Y) >= X because [28], by (Star) 28] cons*(X, Y) >= X because [29], by (Select) 29] X >= X by (Meta) 30] map*(F, cons(X, Y)) >= map(F, Y) because map in Mul, [31] and [32], by (Stat) 31] F >= F by (Meta) 32] cons(X, Y) > Y because [33], by definition 33] cons*(X, Y) >= Y because [34], by (Select) 34] Y >= Y by (Meta) 35] filter(F, nil) > nil because [36], by definition 36] filter*(F, nil) >= nil because [20], by (Select) 37] filter(F, cons(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because [38], by (Star) 38] filter*(F, cons(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because filter = filter2, [39], [42], [43], [45] and [49], by (Stat) 39] cons(X, Y) > Y because [40], by definition 40] cons*(X, Y) >= Y because [41], by (Select) 41] Y >= Y by (Meta) 42] filter*(F, cons(X, Y)) >= @_{o -> o}(F, X) because filter > @_{o -> o}, [43] and [45], by (Copy) 43] filter*(F, cons(X, Y)) >= F because [44], by (Select) 44] F >= F by (Meta) 45] filter*(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] filter*(F, cons(X, Y)) >= Y because [50], by (Select) 50] cons(X, Y) >= Y because [40], by (Star) 51] filter2(true, F, X, Y) > cons(X, filter(F, Y)) because [52], by definition 52] filter2*(true, F, X, Y) >= cons(X, filter(F, Y)) because filter2 > cons, [53] and [55], by (Copy) 53] filter2*(true, F, X, Y) >= X because [54], by (Select) 54] X >= X by (Meta) 55] filter2*(true, F, X, Y) >= filter(F, Y) because filter2 = filter, [56], [57], [58] and [59], by (Stat) 56] F >= F by (Meta) 57] Y >= Y by (Meta) 58] filter2*(true, F, X, Y) >= F because [56], by (Select) 59] filter2*(true, F, X, Y) >= Y because [57], by (Select) 60] filter2(false, F, X, Y) >= filter(F, Y) because [61], by (Star) 61] filter2*(false, F, X, Y) >= filter(F, Y) because filter2 = filter, [62], [63], [64] and [65], by (Stat) 62] F >= F by (Meta) 63] Y >= Y by (Meta) 64] filter2*(false, F, X, Y) >= F because [62], by (Select) 65] filter2*(false, F, X, Y) >= Y because [63], by (Select) We can thus remove the following rules: f(g(X)) => g(g(f(X))) filter(F, nil) => nil filter2(true, F, X, Y) => cons(X, filter(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]): f(g(X)) >? g(g(g(X))) map(F, nil) >? nil map(F, cons(X, Y)) >? cons(F X, map(F, Y)) filter(F, cons(X, Y)) >? filter2(F X, F, X, Y) filter2(false, F, X, Y) >? filter(F, Y) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[filter2(x_1, x_2, x_3, x_4)]] = filter2(x_2, x_4, x_3, x_1) We choose Lex = {filter, filter2} and Mul = {@_{o -> o}, cons, f, false, g, map, nil}, and the following precedence: nil > filter = filter2 > f > map > @_{o -> o} > false > g > cons Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: f(g(X)) >= g(g(g(X))) map(F, nil) > nil map(F, cons(X, Y)) > cons(@_{o -> o}(F, X), map(F, Y)) filter(F, cons(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) filter2(false, F, X, Y) >= filter(F, Y) With these choices, we have: 1] f(g(X)) >= g(g(g(X))) because [2], by (Star) 2] f*(g(X)) >= g(g(g(X))) because f > g and [3], by (Copy) 3] f*(g(X)) >= g(g(X)) because f > g and [4], by (Copy) 4] f*(g(X)) >= g(X) because [5], by (Select) 5] g(X) >= g(X) because g in Mul and [6], by (Fun) 6] X >= X by (Meta) 7] map(F, nil) > nil because [8], by definition 8] map*(F, nil) >= nil because [9], by (Select) 9] nil >= nil by (Fun) 10] map(F, cons(X, Y)) > cons(@_{o -> o}(F, X), map(F, Y)) because [11], by definition 11] map*(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) because map > cons, [12] and [19], by (Copy) 12] map*(F, cons(X, Y)) >= @_{o -> o}(F, X) because map > @_{o -> o}, [13] and [15], by (Copy) 13] map*(F, cons(X, Y)) >= F because [14], by (Select) 14] F >= F by (Meta) 15] map*(F, cons(X, Y)) >= X because [16], by (Select) 16] cons(X, Y) >= X because [17], by (Star) 17] cons*(X, Y) >= X because [18], by (Select) 18] X >= X by (Meta) 19] map*(F, cons(X, Y)) >= map(F, Y) because map in Mul, [20] and [21], by (Stat) 20] F >= F by (Meta) 21] cons(X, Y) > Y because [22], by definition 22] cons*(X, Y) >= Y because [23], by (Select) 23] Y >= Y by (Meta) 24] filter(F, cons(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because [25], by (Star) 25] filter*(F, cons(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because filter = filter2, [26], [27], [30], [31], [32] and [36], by (Stat) 26] F >= F by (Meta) 27] cons(X, Y) > Y because [28], by definition 28] cons*(X, Y) >= Y because [29], by (Select) 29] Y >= Y by (Meta) 30] filter*(F, cons(X, Y)) >= @_{o -> o}(F, X) because filter > @_{o -> o}, [31] and [32], by (Copy) 31] filter*(F, cons(X, Y)) >= F because [26], by (Select) 32] filter*(F, cons(X, Y)) >= X because [33], by (Select) 33] cons(X, Y) >= X because [34], by (Star) 34] cons*(X, Y) >= X because [35], by (Select) 35] X >= X by (Meta) 36] filter*(F, cons(X, Y)) >= Y because [37], by (Select) 37] cons(X, Y) >= Y because [28], by (Star) 38] filter2(false, F, X, Y) >= filter(F, Y) because [39], by (Star) 39] filter2*(false, F, X, Y) >= filter(F, Y) because filter2 = filter, [40], [41], [42] and [43], by (Stat) 40] F >= F by (Meta) 41] Y >= Y by (Meta) 42] filter2*(false, F, X, Y) >= F because [40], by (Select) 43] filter2*(false, F, X, Y) >= Y because [41], by (Select) We can thus remove the following rules: 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]): f(g(X)) >? g(g(g(X))) filter(F, cons(X, Y)) >? filter2(F X, F, X, Y) filter2(false, F, X, Y) >? filter(F, Y) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[filter2(x_1, x_2, x_3, x_4)]] = filter2(x_2, x_4, x_1, x_3) We choose Lex = {filter, filter2} and Mul = {@_{o -> o}, cons, f, false, g}, and the following precedence: cons > f > filter = filter2 > false = g > @_{o -> o} Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: f(g(X)) >= g(g(g(X))) filter(F, cons(X, Y)) > filter2(@_{o -> o}(F, X), F, X, Y) filter2(false, F, X, Y) > filter(F, Y) With these choices, we have: 1] f(g(X)) >= g(g(g(X))) because [2], by (Star) 2] f*(g(X)) >= g(g(g(X))) because f > g and [3], by (Copy) 3] f*(g(X)) >= g(g(X)) because f > g and [4], by (Copy) 4] f*(g(X)) >= g(X) because [5], by (Select) 5] g(X) >= g(X) because g in Mul and [6], by (Fun) 6] X >= X by (Meta) 7] filter(F, cons(X, Y)) > filter2(@_{o -> o}(F, X), F, X, Y) because [8], by definition 8] filter*(F, cons(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because filter = filter2, [9], [10], [13], [14], [15] and [19], by (Stat) 9] F >= F by (Meta) 10] cons(X, Y) > Y because [11], by definition 11] cons*(X, Y) >= Y because [12], by (Select) 12] Y >= Y by (Meta) 13] filter*(F, cons(X, Y)) >= @_{o -> o}(F, X) because filter > @_{o -> o}, [14] and [15], by (Copy) 14] filter*(F, cons(X, Y)) >= F because [9], by (Select) 15] filter*(F, cons(X, Y)) >= X because [16], by (Select) 16] cons(X, Y) >= X because [17], by (Star) 17] cons*(X, Y) >= X because [18], by (Select) 18] X >= X by (Meta) 19] filter*(F, cons(X, Y)) >= Y because [20], by (Select) 20] cons(X, Y) >= Y because [11], by (Star) 21] filter2(false, F, X, Y) > filter(F, Y) because [22], by definition 22] filter2*(false, F, X, Y) >= filter(F, Y) because filter2 = filter, [23], [24], [25] and [26], by (Stat) 23] F >= F by (Meta) 24] Y >= Y by (Meta) 25] filter2*(false, F, X, Y) >= F because [23], by (Select) 26] filter2*(false, F, X, Y) >= Y because [24], by (Select) We can thus remove the following rules: filter(F, cons(X, Y)) => filter2(F X, F, X, Y) filter2(false, F, X, Y) => filter(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]): f(g(X)) >? g(g(g(X))) We use a recursive path ordering as defined in [Kop12, Chapter 5]. We choose Lex = {} and Mul = {f, g}, and the following precedence: f > g With these choices, we have: 1] f(g(X)) > g(g(g(X))) because [2], by definition 2] f*(g(X)) >= g(g(g(X))) because f > g and [3], by (Copy) 3] f*(g(X)) >= g(g(X)) because f > g and [4], by (Copy) 4] f*(g(X)) >= g(X) because [5], by (Select) 5] g(X) >= g(X) because g in Mul and [6], by (Fun) 6] X >= X by (Meta) We can thus remove the following rules: f(g(X)) => g(g(g(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 +++ [Kop12] C. Kop. Higher Order Termination. PhD Thesis, 2012.