We consider the system Applicative_first_order_05__#3.16. Alphabet: 0 : [] --> a cons : [c * d] --> d false : [] --> b filter : [c -> b * d] --> d filter2 : [b * c -> b * c * d] --> d map : [c -> c * d] --> d nil : [] --> d plus : [a * a] --> a s : [a] --> a times : [a * a] --> a true : [] --> b Rules: times(x, 0) => 0 times(x, s(y)) => plus(times(x, y), x) plus(x, 0) => x plus(0, x) => x plus(x, s(y)) => s(plus(x, y)) plus(s(x), y) => s(plus(x, 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]): times(X, 0) >? 0 times(X, s(Y)) >? plus(times(X, Y), X) plus(X, 0) >? X plus(0, X) >? X plus(X, s(Y)) >? s(plus(X, Y)) plus(s(X), Y) >? s(plus(X, 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: [[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) [[nil]] = _|_ We choose Lex = {filter, filter2} and Mul = {0, @_{o -> o}, cons, false, map, plus, s, times, true}, and the following precedence: true > filter = filter2 > times > plus > s > map > @_{o -> o} > false > cons > 0 Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: times(X, 0) >= 0 times(X, s(Y)) > plus(times(X, Y), X) plus(X, 0) >= X plus(0, X) > X plus(X, s(Y)) > s(plus(X, Y)) plus(s(X), Y) >= s(plus(X, Y)) map(F, _|_) >= _|_ map(F, cons(X, Y)) > cons(@_{o -> o}(F, X), map(F, Y)) filter(F, _|_) > _|_ 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] times(X, 0) >= 0 because [2], by (Star) 2] times*(X, 0) >= 0 because times > 0, by (Copy) 3] times(X, s(Y)) > plus(times(X, Y), X) because [4], by definition 4] times*(X, s(Y)) >= plus(times(X, Y), X) because times > plus, [5] and [10], by (Copy) 5] times*(X, s(Y)) >= times(X, Y) because times in Mul, [6] and [7], by (Stat) 6] X >= X by (Meta) 7] s(Y) > Y because [8], by definition 8] s*(Y) >= Y because [9], by (Select) 9] Y >= Y by (Meta) 10] times*(X, s(Y)) >= X because [6], by (Select) 11] plus(X, 0) >= X because [12], by (Star) 12] plus*(X, 0) >= X because [13], by (Select) 13] X >= X by (Meta) 14] plus(0, X) > X because [15], by definition 15] plus*(0, X) >= X because [16], by (Select) 16] X >= X by (Meta) 17] plus(X, s(Y)) > s(plus(X, Y)) because [18], by definition 18] plus*(X, s(Y)) >= s(plus(X, Y)) because plus > s and [19], by (Copy) 19] plus*(X, s(Y)) >= plus(X, Y) because plus in Mul, [20] and [21], by (Stat) 20] X >= X by (Meta) 21] s(Y) > Y because [22], by definition 22] s*(Y) >= Y because [23], by (Select) 23] Y >= Y by (Meta) 24] plus(s(X), Y) >= s(plus(X, Y)) because [25], by (Star) 25] plus*(s(X), Y) >= s(plus(X, Y)) because plus > s and [26], by (Copy) 26] plus*(s(X), Y) >= plus(X, Y) because plus in Mul, [27] and [30], by (Stat) 27] s(X) > X because [28], by definition 28] s*(X) >= X because [29], by (Select) 29] X >= X by (Meta) 30] Y >= Y by (Meta) 31] map(F, _|_) >= _|_ by (Bot) 32] map(F, cons(X, Y)) > cons(@_{o -> o}(F, X), map(F, Y)) because [33], by definition 33] map*(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) because map > cons, [34] and [41], by (Copy) 34] map*(F, cons(X, Y)) >= @_{o -> o}(F, X) because map > @_{o -> o}, [35] and [37], by (Copy) 35] map*(F, cons(X, Y)) >= F because [36], by (Select) 36] F >= F by (Meta) 37] map*(F, cons(X, Y)) >= X because [38], by (Select) 38] cons(X, Y) >= X because [39], by (Star) 39] cons*(X, Y) >= X because [40], by (Select) 40] X >= X by (Meta) 41] map*(F, cons(X, Y)) >= map(F, Y) because map in Mul, [42] and [43], 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, _|_) > _|_ because [47], by definition 47] filter*(F, _|_) >= _|_ by (Bot) 48] filter(F, cons(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because [49], by (Star) 49] filter*(F, cons(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because filter = filter2, [50], [53], [54], [56] and [60], by (Stat) 50] cons(X, Y) > Y because [51], by definition 51] cons*(X, Y) >= Y because [52], by (Select) 52] Y >= Y by (Meta) 53] filter*(F, cons(X, Y)) >= @_{o -> o}(F, X) because filter > @_{o -> o}, [54] and [56], by (Copy) 54] filter*(F, cons(X, Y)) >= F because [55], by (Select) 55] F >= F by (Meta) 56] filter*(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] filter*(F, cons(X, Y)) >= Y because [61], by (Select) 61] cons(X, Y) >= Y because [51], by (Star) 62] filter2(true, F, X, Y) > cons(X, filter(F, Y)) because [63], by definition 63] filter2*(true, F, X, Y) >= cons(X, filter(F, Y)) because filter2 > cons, [64] and [66], by (Copy) 64] filter2*(true, F, X, Y) >= X because [65], by (Select) 65] X >= X by (Meta) 66] filter2*(true, F, X, Y) >= filter(F, Y) because filter2 = filter, [67], [68], [69] and [70], by (Stat) 67] F >= F by (Meta) 68] Y >= Y by (Meta) 69] filter2*(true, F, X, Y) >= F because [67], by (Select) 70] filter2*(true, F, X, Y) >= Y because [68], by (Select) 71] filter2(false, F, X, Y) >= filter(F, Y) because [72], by (Star) 72] filter2*(false, F, X, Y) >= filter(F, Y) because filter2 = filter, [73], [74], [75] and [76], by (Stat) 73] F >= F by (Meta) 74] Y >= Y by (Meta) 75] filter2*(false, F, X, Y) >= F because [73], by (Select) 76] filter2*(false, F, X, Y) >= Y because [74], by (Select) We can thus remove the following rules: times(X, s(Y)) => plus(times(X, Y), X) plus(0, X) => X plus(X, s(Y)) => s(plus(X, Y)) 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]): times(X, 0) >? 0 plus(X, 0) >? X plus(s(X), Y) >? s(plus(X, Y)) map(F, nil) >? nil 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: [[0]] = _|_ [[filter2(x_1, x_2, x_3, x_4)]] = filter2(x_2, x_4, x_3, x_1) [[nil]] = _|_ We choose Lex = {filter, filter2} and Mul = {@_{o -> o}, cons, false, map, plus, s, times}, and the following precedence: false > cons > times > plus > s > filter = filter2 > map > @_{o -> o} Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: times(X, _|_) >= _|_ plus(X, _|_) >= X plus(s(X), Y) >= s(plus(X, Y)) map(F, _|_) >= _|_ 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] times(X, _|_) >= _|_ by (Bot) 2] plus(X, _|_) >= X because [3], by (Star) 3] plus*(X, _|_) >= X because [4], by (Select) 4] X >= X by (Meta) 5] plus(s(X), Y) >= s(plus(X, Y)) because [6], by (Star) 6] plus*(s(X), Y) >= s(plus(X, Y)) because plus > s and [7], by (Copy) 7] plus*(s(X), Y) >= plus(X, Y) because plus in Mul, [8] and [11], by (Stat) 8] s(X) > X because [9], by definition 9] s*(X) >= X because [10], by (Select) 10] X >= X by (Meta) 11] Y >= Y by (Meta) 12] map(F, _|_) >= _|_ by (Bot) 13] filter(F, cons(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because [14], by (Star) 14] filter*(F, cons(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because filter = filter2, [15], [16], [19], [20], [21] and [25], by (Stat) 15] F >= F by (Meta) 16] cons(X, Y) > Y because [17], by definition 17] cons*(X, Y) >= Y because [18], by (Select) 18] Y >= Y by (Meta) 19] filter*(F, cons(X, Y)) >= @_{o -> o}(F, X) because filter > @_{o -> o}, [20] and [21], by (Copy) 20] filter*(F, cons(X, Y)) >= F because [15], by (Select) 21] filter*(F, cons(X, Y)) >= X because [22], by (Select) 22] cons(X, Y) >= X because [23], by (Star) 23] cons*(X, Y) >= X because [24], by (Select) 24] X >= X by (Meta) 25] filter*(F, cons(X, Y)) >= Y because [26], by (Select) 26] cons(X, Y) >= Y because [17], by (Star) 27] filter2(false, F, X, Y) > filter(F, Y) because [28], by definition 28] filter2*(false, F, X, Y) >= filter(F, Y) because filter2 = filter, [29], [30], [31] and [32], by (Stat) 29] F >= F by (Meta) 30] Y >= Y by (Meta) 31] filter2*(false, F, X, Y) >= F because [29], by (Select) 32] filter2*(false, F, X, Y) >= Y because [30], by (Select) We can thus remove the following rules: 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]): times(X, 0) >? 0 plus(X, 0) >? X plus(s(X), Y) >? s(plus(X, Y)) map(F, nil) >? nil filter(F, cons(X, Y)) >? filter2(F X, F, X, Y) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[nil]] = _|_ We choose Lex = {} and Mul = {@_{o -> o}, cons, filter, filter2, map, plus, s, times}, and the following precedence: filter > cons > @_{o -> o} > plus > filter2 > s > map > times Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: times(X, _|_) >= _|_ plus(X, _|_) > X plus(s(X), Y) >= s(plus(X, Y)) map(F, _|_) >= _|_ filter(F, cons(X, Y)) > filter2(@_{o -> o}(F, X), F, X, Y) With these choices, we have: 1] times(X, _|_) >= _|_ by (Bot) 2] plus(X, _|_) > X because [3], by definition 3] plus*(X, _|_) >= X because [4], by (Select) 4] X >= X by (Meta) 5] plus(s(X), Y) >= s(plus(X, Y)) because [6], by (Star) 6] plus*(s(X), Y) >= s(plus(X, Y)) because plus > s and [7], by (Copy) 7] plus*(s(X), Y) >= plus(X, Y) because plus in Mul, [8] and [11], by (Stat) 8] s(X) > X because [9], by definition 9] s*(X) >= X because [10], by (Select) 10] X >= X by (Meta) 11] Y >= Y by (Meta) 12] map(F, _|_) >= _|_ by (Bot) 13] filter(F, cons(X, Y)) > filter2(@_{o -> o}(F, X), F, X, Y) because [14], by definition 14] filter*(F, cons(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because filter > filter2, [15], [16], [18] and [22], by (Copy) 15] filter*(F, cons(X, Y)) >= @_{o -> o}(F, X) because filter > @_{o -> o}, [16] and [18], by (Copy) 16] filter*(F, cons(X, Y)) >= F because [17], by (Select) 17] F >= F by (Meta) 18] filter*(F, cons(X, Y)) >= X because [19], by (Select) 19] cons(X, Y) >= X because [20], by (Star) 20] cons*(X, Y) >= X because [21], by (Select) 21] X >= X by (Meta) 22] filter*(F, cons(X, Y)) >= Y because [23], by (Select) 23] cons(X, Y) >= Y because [24], by (Star) 24] cons*(X, Y) >= Y because [25], by (Select) 25] Y >= Y by (Meta) We can thus remove the following rules: plus(X, 0) => X filter(F, cons(X, Y)) => filter2(F X, F, 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]): times(X, 0) >? 0 plus(s(X), Y) >? s(plus(X, Y)) map(F, nil) >? nil We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[nil]] = _|_ We choose Lex = {} and Mul = {0, map, plus, s, times}, and the following precedence: map > plus > s > times > 0 Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: times(X, 0) > 0 plus(s(X), Y) >= s(plus(X, Y)) map(F, _|_) >= _|_ With these choices, we have: 1] times(X, 0) > 0 because [2], by definition 2] times*(X, 0) >= 0 because times > 0, by (Copy) 3] plus(s(X), Y) >= s(plus(X, Y)) because [4], by (Star) 4] plus*(s(X), Y) >= s(plus(X, Y)) because plus > s and [5], by (Copy) 5] plus*(s(X), Y) >= plus(X, Y) because plus in Mul, [6] and [9], by (Stat) 6] s(X) > X because [7], by definition 7] s*(X) >= X because [8], by (Select) 8] X >= X by (Meta) 9] Y >= Y by (Meta) 10] map(F, _|_) >= _|_ by (Bot) We can thus remove the following rules: times(X, 0) => 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)) map(F, nil) >? nil We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[nil]] = _|_ We choose Lex = {} and Mul = {map, plus, s}, and the following precedence: map > plus > s Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: plus(s(X), Y) > s(plus(X, Y)) map(F, _|_) >= _|_ With these choices, we have: 1] plus(s(X), Y) > s(plus(X, Y)) because [2], by definition 2] plus*(s(X), Y) >= s(plus(X, Y)) because plus > s and [3], by (Copy) 3] plus*(s(X), Y) >= plus(X, Y) because plus in Mul, [4] and [7], by (Stat) 4] s(X) > X because [5], by definition 5] s*(X) >= X because [6], by (Select) 6] X >= X by (Meta) 7] Y >= Y by (Meta) 8] map(F, _|_) >= _|_ by (Bot) 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]): map(F, nil) >? nil We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[nil]] = _|_ We choose Lex = {} and Mul = {map}, and the following precedence: map Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: map(F, _|_) > _|_ With these choices, we have: 1] map(F, _|_) > _|_ because [2], by definition 2] map*(F, _|_) >= _|_ by (Bot) We can thus remove the following rules: map(F, nil) => nil 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.