We consider the system Applicative_first_order_05__08. Alphabet: !facminus : [a * a] --> a !facplus : [a * a] --> a !factimes : [a * a] --> a 0 : [] --> a 1 : [] --> a D : [a] --> a cons : [c * d] --> d constant : [] --> a false : [] --> b filter : [c -> b * d] --> d filter2 : [b * c -> b * c * d] --> d map : [c -> c * d] --> d nil : [] --> d t : [] --> a true : [] --> b Rules: D(t) => 1 D(constant) => 0 D(!facplus(x, y)) => !facplus(D(x), D(y)) D(!factimes(x, y)) => !facplus(!factimes(y, D(x)), !factimes(x, D(y))) D(!facminus(x, y)) => !facminus(D(x), D(y)) 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) 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]): D(t) >? 1 D(constant) >? 0 D(!facplus(X, Y)) >? !facplus(D(X), D(Y)) D(!factimes(X, Y)) >? !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X, Y)) >? !facminus(D(X), D(Y)) 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: [[!facplus(x_1, x_2)]] = !facplus(x_2, x_1) [[0]] = _|_ [[1]] = _|_ [[cons(x_1, x_2)]] = cons(x_2, x_1) [[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_3, x_1) We choose Lex = {!facplus, !factimes, D, cons, false, filter, filter2, true} and Mul = {!facminus, @_{o -> o}, constant, map, nil, t}, and the following precedence: constant > filter = filter2 > map > @_{o -> o} > !factimes = D > !facminus > false > !facplus > cons > nil > t > true Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: D(t) >= _|_ D(constant) > _|_ D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) 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] D(t) >= _|_ by (Bot) 2] D(constant) > _|_ because [3], by definition 3] D*(constant) >= _|_ by (Bot) 4] D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) because [5], by (Star) 5] D*(!facplus(X, Y)) >= !facplus(D(X), D(Y)) because D > !facplus, [6] and [12], by (Copy) 6] D*(!facplus(X, Y)) >= D(X) because [7], [10] and [7], by (Stat) 7] !facplus(X, Y) > X because [8], by definition 8] !facplus*(X, Y) >= X because [9], by (Select) 9] X >= X by (Meta) 10] D*(!facplus(X, Y)) >= X because [11], by (Select) 11] !facplus(X, Y) >= X because [8], by (Star) 12] D*(!facplus(X, Y)) >= D(Y) because [13], [16] and [13], by (Stat) 13] !facplus(X, Y) > Y because [14], by definition 14] !facplus*(X, Y) >= Y because [15], by (Select) 15] Y >= Y by (Meta) 16] D*(!facplus(X, Y)) >= Y because [17], by (Select) 17] !facplus(X, Y) >= Y because [14], by (Star) 18] D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) because [19], by (Star) 19] D*(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) because D > !facplus, [20] and [32], by (Copy) 20] D*(!factimes(X, Y)) >= !factimes(Y, D(X)) because D = !factimes, [21], [24] and [26], by (Stat) 21] !factimes(X, Y) > Y because [22], by definition 22] !factimes*(X, Y) >= Y because [23], by (Select) 23] Y >= Y by (Meta) 24] D*(!factimes(X, Y)) >= Y because [25], by (Select) 25] !factimes(X, Y) >= Y because [22], by (Star) 26] D*(!factimes(X, Y)) >= D(X) because [27], [30] and [27], by (Stat) 27] !factimes(X, Y) > X because [28], by definition 28] !factimes*(X, Y) >= X because [29], by (Select) 29] X >= X by (Meta) 30] D*(!factimes(X, Y)) >= X because [31], by (Select) 31] !factimes(X, Y) >= X because [28], by (Star) 32] D*(!factimes(X, Y)) >= !factimes(X, D(Y)) because D = !factimes, [27], [30] and [33], by (Stat) 33] D*(!factimes(X, Y)) >= D(Y) because [21], [24] and [21], by (Stat) 34] D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) because [35], by (Star) 35] D*(!facminus(X, Y)) >= !facminus(D(X), D(Y)) because D > !facminus, [36] and [42], by (Copy) 36] D*(!facminus(X, Y)) >= D(X) because [37], [40] and [37], by (Stat) 37] !facminus(X, Y) > X because [38], by definition 38] !facminus*(X, Y) >= X because [39], by (Select) 39] X >= X by (Meta) 40] D*(!facminus(X, Y)) >= X because [41], by (Select) 41] !facminus(X, Y) >= X because [38], by (Star) 42] D*(!facminus(X, Y)) >= D(Y) because [43], [46] and [43], by (Stat) 43] !facminus(X, Y) > Y because [44], by definition 44] !facminus*(X, Y) >= Y because [45], by (Select) 45] Y >= Y by (Meta) 46] D*(!facminus(X, Y)) >= Y because [47], by (Select) 47] !facminus(X, Y) >= Y because [44], by (Star) 48] map(F, nil) > nil because [49], by definition 49] map*(F, nil) >= nil because [50], by (Select) 50] nil >= nil by (Fun) 51] map(F, cons(X, Y)) > cons(@_{o -> o}(F, X), map(F, Y)) because [52], by definition 52] map*(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) because map > cons, [53] and [60], by (Copy) 53] map*(F, cons(X, Y)) >= @_{o -> o}(F, X) because map > @_{o -> o}, [54] and [56], by (Copy) 54] map*(F, cons(X, Y)) >= F because [55], by (Select) 55] F >= F by (Meta) 56] map*(F, cons(X, Y)) >= X because [57], by (Select) 57] cons(X, Y) >= X because [58], by (Star) 58] cons*(X, Y) >= X because [59], by (Select) 59] X >= X by (Meta) 60] map*(F, cons(X, Y)) >= map(F, Y) because map in Mul, [61] and [62], by (Stat) 61] F >= F by (Meta) 62] cons(X, Y) > Y because [63], by definition 63] cons*(X, Y) >= Y because [64], by (Select) 64] Y >= Y by (Meta) 65] filter(F, nil) > nil because [66], by definition 66] filter*(F, nil) >= nil because [50], by (Select) 67] filter(F, cons(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because [68], by (Star) 68] filter*(F, cons(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because filter = filter2, [69], [72], [73], [75] and [79], by (Stat) 69] cons(X, Y) > Y because [70], by definition 70] cons*(X, Y) >= Y because [71], by (Select) 71] Y >= Y by (Meta) 72] filter*(F, cons(X, Y)) >= @_{o -> o}(F, X) because filter > @_{o -> o}, [73] and [75], by (Copy) 73] filter*(F, cons(X, Y)) >= F because [74], by (Select) 74] F >= F by (Meta) 75] filter*(F, cons(X, Y)) >= X because [76], by (Select) 76] cons(X, Y) >= X because [77], by (Star) 77] cons*(X, Y) >= X because [78], by (Select) 78] X >= X by (Meta) 79] filter*(F, cons(X, Y)) >= Y because [80], by (Select) 80] cons(X, Y) >= Y because [70], by (Star) 81] filter2(true, F, X, Y) > cons(X, filter(F, Y)) because [82], by definition 82] filter2*(true, F, X, Y) >= cons(X, filter(F, Y)) because filter2 > cons, [83] and [85], by (Copy) 83] filter2*(true, F, X, Y) >= X because [84], by (Select) 84] X >= X by (Meta) 85] filter2*(true, F, X, Y) >= filter(F, Y) because filter2 = filter, [86], [87], [88], [89], [86] and [87], by (Stat) 86] F >= F by (Meta) 87] Y >= Y by (Meta) 88] filter2*(true, F, X, Y) >= F because [86], by (Select) 89] filter2*(true, F, X, Y) >= Y because [87], by (Select) 90] filter2(false, F, X, Y) >= filter(F, Y) because [91], by (Star) 91] filter2*(false, F, X, Y) >= filter(F, Y) because filter2 = filter, [92], [93], [94], [95], [92] and [93], by (Stat) 92] F >= F by (Meta) 93] Y >= Y by (Meta) 94] filter2*(false, F, X, Y) >= F because [92], by (Select) 95] filter2*(false, F, X, Y) >= Y because [93], by (Select) We can thus remove the following rules: D(constant) => 0 map(F, nil) => nil map(F, cons(X, Y)) => cons(F X, map(F, Y)) 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]): D(t) >? 1 D(!facplus(X, Y)) >? !facplus(D(X), D(Y)) D(!factimes(X, Y)) >? !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X, Y)) >? !facminus(D(X), D(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: [[1]] = _|_ [[filter2(x_1, x_2, x_3, x_4)]] = filter2(x_2, x_4, x_1, x_3) We choose Lex = {false, filter, filter2} and Mul = {!facminus, !facplus, !factimes, @_{o -> o}, D, cons, t}, and the following precedence: D > !facminus > !facplus > !factimes > cons > false > filter = filter2 > @_{o -> o} > t Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: D(t) > _|_ D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X, Y)) >= !facminus(D(X), D(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] D(t) > _|_ because [2], by definition 2] D*(t) >= _|_ by (Bot) 3] D(!facplus(X, Y)) >= !facplus(D(X), D(Y)) because [4], by (Star) 4] D*(!facplus(X, Y)) >= !facplus(D(X), D(Y)) because D > !facplus, [5] and [9], by (Copy) 5] D*(!facplus(X, Y)) >= D(X) because D in Mul and [6], by (Stat) 6] !facplus(X, Y) > X because [7], by definition 7] !facplus*(X, Y) >= X because [8], by (Select) 8] X >= X by (Meta) 9] D*(!facplus(X, Y)) >= D(Y) because D in Mul and [10], by (Stat) 10] !facplus(X, Y) > Y because [11], by definition 11] !facplus*(X, Y) >= Y because [12], by (Select) 12] Y >= Y by (Meta) 13] D(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) because [14], by (Star) 14] D*(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) because D > !facplus, [15] and [24], by (Copy) 15] D*(!factimes(X, Y)) >= !factimes(Y, D(X)) because D > !factimes, [16] and [20], by (Copy) 16] D*(!factimes(X, Y)) >= Y because [17], by (Select) 17] !factimes(X, Y) >= Y because [18], by (Star) 18] !factimes*(X, Y) >= Y because [19], by (Select) 19] Y >= Y by (Meta) 20] D*(!factimes(X, Y)) >= D(X) because D in Mul and [21], by (Stat) 21] !factimes(X, Y) > X because [22], by definition 22] !factimes*(X, Y) >= X because [23], by (Select) 23] X >= X by (Meta) 24] D*(!factimes(X, Y)) >= !factimes(X, D(Y)) because D > !factimes, [25] and [27], by (Copy) 25] D*(!factimes(X, Y)) >= X because [26], by (Select) 26] !factimes(X, Y) >= X because [22], by (Star) 27] D*(!factimes(X, Y)) >= D(Y) because D in Mul and [28], by (Stat) 28] !factimes(X, Y) > Y because [29], by definition 29] !factimes*(X, Y) >= Y because [19], by (Select) 30] D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) because [31], by (Star) 31] D*(!facminus(X, Y)) >= !facminus(D(X), D(Y)) because D > !facminus, [32] and [36], by (Copy) 32] D*(!facminus(X, Y)) >= D(X) because D in Mul and [33], by (Stat) 33] !facminus(X, Y) > X because [34], by definition 34] !facminus*(X, Y) >= X because [35], by (Select) 35] X >= X by (Meta) 36] D*(!facminus(X, Y)) >= D(Y) because D in Mul and [37], by (Stat) 37] !facminus(X, Y) > Y because [38], by definition 38] !facminus*(X, Y) >= Y because [39], by (Select) 39] Y >= Y by (Meta) 40] filter(F, cons(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because [41], by (Star) 41] filter*(F, cons(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because filter = filter2, [42], [43], [46], [47], [48] and [52], by (Stat) 42] F >= F by (Meta) 43] cons(X, Y) > Y because [44], by definition 44] cons*(X, Y) >= Y because [45], by (Select) 45] Y >= Y by (Meta) 46] filter*(F, cons(X, Y)) >= @_{o -> o}(F, X) because filter > @_{o -> o}, [47] and [48], by (Copy) 47] filter*(F, cons(X, Y)) >= F because [42], by (Select) 48] filter*(F, cons(X, Y)) >= X because [49], by (Select) 49] cons(X, Y) >= X because [50], by (Star) 50] cons*(X, Y) >= X because [51], by (Select) 51] X >= X by (Meta) 52] filter*(F, cons(X, Y)) >= Y because [53], by (Select) 53] cons(X, Y) >= Y because [44], by (Star) 54] filter2(false, F, X, Y) > filter(F, Y) because [55], by definition 55] filter2*(false, F, X, Y) >= filter(F, Y) because filter2 = filter, [56], [57], [58], [59], [56] and [57], by (Stat) 56] F >= F by (Meta) 57] Y >= Y by (Meta) 58] filter2*(false, F, X, Y) >= F because [56], by (Select) 59] filter2*(false, F, X, Y) >= Y because [57], by (Select) We can thus remove the following rules: D(t) => 1 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]): D(!facplus(X, Y)) >? !facplus(D(X), D(Y)) D(!factimes(X, Y)) >? !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) D(!facminus(X, Y)) >? !facminus(D(X), D(Y)) filter(F, cons(X, Y)) >? filter2(F X, F, X, Y) We use a recursive path ordering as defined in [Kop12, Chapter 5]. We choose Lex = {!facplus, !factimes} and Mul = {!facminus, @_{o -> o}, D, cons, filter, filter2}, and the following precedence: D > !facminus > !facplus = !factimes > cons > filter > @_{o -> o} > filter2 With these choices, we have: 1] D(!facplus(X, Y)) > !facplus(D(X), D(Y)) because [2], by definition 2] D*(!facplus(X, Y)) >= !facplus(D(X), D(Y)) because D > !facplus, [3] and [7], by (Copy) 3] D*(!facplus(X, Y)) >= D(X) because D in Mul and [4], by (Stat) 4] !facplus(X, Y) > X because [5], by definition 5] !facplus*(X, Y) >= X because [6], by (Select) 6] X >= X by (Meta) 7] D*(!facplus(X, Y)) >= D(Y) because D in Mul and [8], by (Stat) 8] !facplus(X, Y) > Y because [9], by definition 9] !facplus*(X, Y) >= Y because [10], by (Select) 10] Y >= Y by (Meta) 11] D(!factimes(X, Y)) > !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) because [12], by definition 12] D*(!factimes(X, Y)) >= !facplus(!factimes(Y, D(X)), !factimes(X, D(Y))) because D > !facplus, [13] and [22], by (Copy) 13] D*(!factimes(X, Y)) >= !factimes(Y, D(X)) because D > !factimes, [14] and [18], by (Copy) 14] D*(!factimes(X, Y)) >= Y because [15], by (Select) 15] !factimes(X, Y) >= Y because [16], by (Star) 16] !factimes*(X, Y) >= Y because [17], by (Select) 17] Y >= Y by (Meta) 18] D*(!factimes(X, Y)) >= D(X) because D in Mul and [19], by (Stat) 19] !factimes(X, Y) > X because [20], by definition 20] !factimes*(X, Y) >= X because [21], by (Select) 21] X >= X by (Meta) 22] D*(!factimes(X, Y)) >= !factimes(X, D(Y)) because D > !factimes, [23] and [25], by (Copy) 23] D*(!factimes(X, Y)) >= X because [24], by (Select) 24] !factimes(X, Y) >= X because [20], by (Star) 25] D*(!factimes(X, Y)) >= D(Y) because D in Mul and [26], by (Stat) 26] !factimes(X, Y) > Y because [27], by definition 27] !factimes*(X, Y) >= Y because [17], by (Select) 28] D(!facminus(X, Y)) >= !facminus(D(X), D(Y)) because [29], by (Star) 29] D*(!facminus(X, Y)) >= !facminus(D(X), D(Y)) because D > !facminus, [30] and [34], by (Copy) 30] D*(!facminus(X, Y)) >= D(X) because D in Mul and [31], by (Stat) 31] !facminus(X, Y) > X because [32], by definition 32] !facminus*(X, Y) >= X because [33], by (Select) 33] X >= X by (Meta) 34] D*(!facminus(X, Y)) >= D(Y) because D in Mul and [35], by (Stat) 35] !facminus(X, Y) > Y because [36], by definition 36] !facminus*(X, Y) >= Y because [37], by (Select) 37] Y >= Y by (Meta) 38] filter(F, cons(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because [39], by (Star) 39] filter*(F, cons(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because filter > filter2, [40], [41], [43] and [47], by (Copy) 40] filter*(F, cons(X, Y)) >= @_{o -> o}(F, X) because filter > @_{o -> o}, [41] and [43], by (Copy) 41] filter*(F, cons(X, Y)) >= F because [42], by (Select) 42] F >= F by (Meta) 43] filter*(F, cons(X, Y)) >= X because [44], by (Select) 44] cons(X, Y) >= X because [45], by (Star) 45] cons*(X, Y) >= X because [46], by (Select) 46] X >= X by (Meta) 47] filter*(F, cons(X, Y)) >= Y because [48], by (Select) 48] cons(X, Y) >= Y because [49], by (Star) 49] cons*(X, Y) >= Y because [50], by (Select) 50] Y >= Y by (Meta) We can thus remove the following rules: D(!facplus(X, Y)) => !facplus(D(X), D(Y)) D(!factimes(X, Y)) => !facplus(!factimes(Y, D(X)), !factimes(X, D(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]): D(!facminus(X, Y)) >? !facminus(D(X), D(Y)) filter(F, cons(X, Y)) >? filter2(F X, F, X, Y) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: !facminus = Lam[y0;y1].3 + y0 + y1 D = Lam[y0].3*y0 cons = Lam[y0;y1].3 + 3*y0 + 3*y1 filter = Lam[G0;y1].3 + 3*y1 + 3*y1*G0(y1) + 3*G0(0) + 3*G0(y1) filter2 = Lam[y0;G1;y2;y3].y0 + y2 + y3 + G1(y2) Using this interpretation, the requirements translate to: [[D(!facminus(_x0, _x1))]] = 9 + 3*x0 + 3*x1 > 3 + 3*x0 + 3*x1 = [[!facminus(D(_x0), D(_x1))]] [[filter(_F0, cons(_x1, _x2))]] = 12 + 9*x1 + 9*x2 + 3*F0(0) + 9*x1*F0(3 + 3*x1 + 3*x2) + 9*x2*F0(3 + 3*x1 + 3*x2) + 12*F0(3 + 3*x1 + 3*x2) > x2 + 2*x1 + 2*F0(x1) = [[filter2(_F0 _x1, _F0, _x1, _x2)]] We can thus remove the following rules: D(!facminus(X, Y)) => !facminus(D(X), D(Y)) filter(F, cons(X, Y)) => filter2(F X, F, 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.