We consider the system Applicative_05__TreeSize. Alphabet: 0 : [] --> c cons : [c * b] --> b map : [c -> c * b] --> b nil : [] --> b node : [a * b] --> c plus : [c * c] --> c s : [c] --> c size : [] --> c -> c sum : [b] --> c Rules: map(f, nil) => nil map(f, cons(x, y)) => cons(f x, map(f, y)) sum(cons(x, y)) => plus(x, sum(y)) size node(x, y) => s(sum(map(size, y))) plus(0, x) => 0 plus(s(x), y) => s(plus(x, 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]): map(F, nil) >? nil map(F, cons(X, Y)) >? cons(F X, map(F, Y)) sum(cons(X, Y)) >? plus(X, sum(Y)) size node(X, Y) >? s(sum(map(size, Y))) plus(0, X) >? 0 plus(s(X), Y) >? s(plus(X, Y)) We use a recursive path ordering as defined in [Kop12, Chapter 5]. We choose Lex = {} and Mul = {0, @_{o -> o}, cons, map, nil, node, plus, s, size, sum}, and the following precedence: node > size > sum > plus > s > map > 0 > @_{o -> o} > cons > nil With these choices, we have: 1] map(F, nil) > nil because [2], by definition 2] map*(F, nil) >= nil because map > nil, by (Copy) 3] map(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) because [4], by (Star) 4] map*(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) because map > cons, [5] and [12], by (Copy) 5] map*(F, cons(X, Y)) >= @_{o -> o}(F, X) because map > @_{o -> o}, [6] and [8], by (Copy) 6] map*(F, cons(X, Y)) >= F because [7], by (Select) 7] F >= F by (Meta) 8] map*(F, cons(X, Y)) >= X because [9], by (Select) 9] cons(X, Y) >= X because [10], by (Star) 10] cons*(X, Y) >= X because [11], by (Select) 11] X >= X by (Meta) 12] map*(F, cons(X, Y)) >= map(F, Y) because map in Mul, [13] and [14], by (Stat) 13] F >= F by (Meta) 14] cons(X, Y) > Y because [15], by definition 15] cons*(X, Y) >= Y because [16], by (Select) 16] Y >= Y by (Meta) 17] sum(cons(X, Y)) >= plus(X, sum(Y)) because [18], by (Star) 18] sum*(cons(X, Y)) >= plus(X, sum(Y)) because sum > plus, [19] and [23], by (Copy) 19] sum*(cons(X, Y)) >= X because [20], by (Select) 20] cons(X, Y) >= X because [21], by (Star) 21] cons*(X, Y) >= X because [22], by (Select) 22] X >= X by (Meta) 23] sum*(cons(X, Y)) >= sum(Y) because sum in Mul and [24], by (Stat) 24] cons(X, Y) > Y because [25], by definition 25] cons*(X, Y) >= Y because [26], by (Select) 26] Y >= Y by (Meta) 27] @_{o -> o}(size, node(X, Y)) >= s(sum(map(size, Y))) because [28], by (Star) 28] @_{o -> o}*(size, node(X, Y)) >= s(sum(map(size, Y))) because [29], by (Select) 29] node(X, Y) >= s(sum(map(size, Y))) because [30], by (Star) 30] node*(X, Y) >= s(sum(map(size, Y))) because node > s and [31], by (Copy) 31] node*(X, Y) >= sum(map(size, Y)) because node > sum and [32], by (Copy) 32] node*(X, Y) >= map(size, Y) because node > map, [33] and [34], by (Copy) 33] node*(X, Y) >= size because node > size, by (Copy) 34] node*(X, Y) >= Y because [35], by (Select) 35] Y >= Y by (Meta) 36] plus(0, X) >= 0 because [37], by (Star) 37] plus*(0, X) >= 0 because plus > 0, by (Copy) 38] plus(s(X), Y) >= s(plus(X, Y)) because [39], by (Star) 39] plus*(s(X), Y) >= s(plus(X, Y)) because plus > s and [40], by (Copy) 40] plus*(s(X), Y) >= plus(X, Y) because plus in Mul, [41] and [44], by (Stat) 41] s(X) > X because [42], by definition 42] s*(X) >= X because [43], by (Select) 43] X >= X by (Meta) 44] Y >= Y 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]): map(F, cons(X, Y)) >? cons(F X, map(F, Y)) sum(cons(X, Y)) >? plus(X, sum(Y)) size node(X, Y) >? s(sum(map(size, Y))) plus(0, X) >? 0 plus(s(X), Y) >? s(plus(X, Y)) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[size]] = _|_ [[sum(x_1)]] = x_1 We choose Lex = {} and Mul = {@_{o -> o}, cons, map, node, plus, s}, and the following precedence: node > map > @_{o -> o} > cons = plus > s Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: map(F, cons(X, Y)) > cons(@_{o -> o}(F, X), map(F, Y)) cons(X, Y) >= plus(X, Y) @_{o -> o}(_|_, node(X, Y)) >= s(map(_|_, Y)) plus(_|_, X) >= _|_ plus(s(X), Y) >= s(plus(X, Y)) With these choices, we have: 1] map(F, cons(X, Y)) > cons(@_{o -> o}(F, X), map(F, Y)) because [2], by definition 2] map*(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) because map > cons, [3] and [10], by (Copy) 3] map*(F, cons(X, Y)) >= @_{o -> o}(F, X) because map > @_{o -> o}, [4] and [6], by (Copy) 4] map*(F, cons(X, Y)) >= F because [5], by (Select) 5] F >= F by (Meta) 6] map*(F, cons(X, Y)) >= X because [7], by (Select) 7] cons(X, Y) >= X because [8], by (Star) 8] cons*(X, Y) >= X because [9], by (Select) 9] X >= X by (Meta) 10] map*(F, cons(X, Y)) >= map(F, Y) because map in Mul, [11] and [12], by (Stat) 11] F >= F by (Meta) 12] cons(X, Y) > Y because [13], by definition 13] cons*(X, Y) >= Y because [14], by (Select) 14] Y >= Y by (Meta) 15] cons(X, Y) >= plus(X, Y) because cons = plus, cons in Mul, [16] and [17], by (Fun) 16] X >= X by (Meta) 17] Y >= Y by (Meta) 18] @_{o -> o}(_|_, node(X, Y)) >= s(map(_|_, Y)) because [19], by (Star) 19] @_{o -> o}*(_|_, node(X, Y)) >= s(map(_|_, Y)) because [20], by (Select) 20] node(X, Y) >= s(map(_|_, Y)) because [21], by (Star) 21] node*(X, Y) >= s(map(_|_, Y)) because node > s and [22], by (Copy) 22] node*(X, Y) >= map(_|_, Y) because node > map, [23] and [24], by (Copy) 23] node*(X, Y) >= _|_ by (Bot) 24] node*(X, Y) >= Y because [25], by (Select) 25] Y >= Y by (Meta) 26] plus(_|_, X) >= _|_ by (Bot) 27] plus(s(X), Y) >= s(plus(X, Y)) because [28], by (Star) 28] plus*(s(X), Y) >= s(plus(X, Y)) because plus > s and [29], by (Copy) 29] plus*(s(X), Y) >= plus(X, Y) because plus in Mul, [30] and [33], by (Stat) 30] s(X) > X because [31], by definition 31] s*(X) >= X because [32], by (Select) 32] X >= X by (Meta) 33] Y >= Y by (Meta) We can thus remove the following rules: 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]): sum(cons(X, Y)) >? plus(X, sum(Y)) size node(X, Y) >? s(sum(map(size, Y))) plus(0, X) >? 0 plus(s(X), Y) >? s(plus(X, Y)) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[sum(x_1)]] = x_1 We choose Lex = {} and Mul = {@_{o -> o}, cons, map, node, plus, s, size}, and the following precedence: cons > plus > @_{o -> o} > node > map > s > size Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: cons(X, Y) > plus(X, Y) @_{o -> o}(size, node(X, Y)) >= s(map(size, Y)) plus(_|_, X) >= _|_ plus(s(X), Y) >= s(plus(X, Y)) With these choices, we have: 1] cons(X, Y) > plus(X, Y) because [2], by definition 2] cons*(X, Y) >= plus(X, Y) because cons > plus, [3] and [5], by (Copy) 3] cons*(X, Y) >= X because [4], by (Select) 4] X >= X by (Meta) 5] cons*(X, Y) >= Y because [6], by (Select) 6] Y >= Y by (Meta) 7] @_{o -> o}(size, node(X, Y)) >= s(map(size, Y)) because [8], by (Star) 8] @_{o -> o}*(size, node(X, Y)) >= s(map(size, Y)) because [9], by (Select) 9] node(X, Y) >= s(map(size, Y)) because [10], by (Star) 10] node*(X, Y) >= s(map(size, Y)) because node > s and [11], by (Copy) 11] node*(X, Y) >= map(size, Y) because node > map, [12] and [13], by (Copy) 12] node*(X, Y) >= size because node > size, by (Copy) 13] node*(X, Y) >= Y because [14], by (Select) 14] Y >= Y by (Meta) 15] plus(_|_, X) >= _|_ by (Bot) 16] plus(s(X), Y) >= s(plus(X, Y)) because [17], by (Star) 17] plus*(s(X), Y) >= s(plus(X, Y)) because plus > s and [18], by (Copy) 18] plus*(s(X), Y) >= plus(X, Y) because plus in Mul, [19] and [22], by (Stat) 19] s(X) > X because [20], by definition 20] s*(X) >= X because [21], by (Select) 21] X >= X by (Meta) 22] Y >= Y by (Meta) We can thus remove the following rules: sum(cons(X, Y)) => plus(X, sum(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]): size node(X, Y) >? s(sum(map(size, Y))) plus(0, X) >? 0 plus(s(X), Y) >? s(plus(X, Y)) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ We choose Lex = {} and Mul = {@_{o -> o}, map, node, plus, s, size, sum}, and the following precedence: plus > node > size > sum > map > s > @_{o -> o} Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: @_{o -> o}(size, node(X, Y)) >= s(sum(map(size, Y))) plus(_|_, X) > _|_ plus(s(X), Y) >= s(plus(X, Y)) With these choices, we have: 1] @_{o -> o}(size, node(X, Y)) >= s(sum(map(size, Y))) because [2], by (Star) 2] @_{o -> o}*(size, node(X, Y)) >= s(sum(map(size, Y))) because [3], by (Select) 3] node(X, Y) >= s(sum(map(size, Y))) because [4], by (Star) 4] node*(X, Y) >= s(sum(map(size, Y))) because node > s and [5], by (Copy) 5] node*(X, Y) >= sum(map(size, Y)) because node > sum and [6], by (Copy) 6] node*(X, Y) >= map(size, Y) because node > map, [7] and [8], by (Copy) 7] node*(X, Y) >= size because node > size, by (Copy) 8] node*(X, Y) >= Y because [9], by (Select) 9] Y >= Y by (Meta) 10] plus(_|_, X) > _|_ because [11], by definition 11] plus*(_|_, X) >= _|_ by (Bot) 12] plus(s(X), Y) >= s(plus(X, Y)) because [13], by (Star) 13] plus*(s(X), Y) >= s(plus(X, Y)) because plus > s and [14], by (Copy) 14] plus*(s(X), Y) >= plus(X, Y) because plus in Mul, [15] and [18], by (Stat) 15] s(X) > X because [16], by definition 16] s*(X) >= X because [17], by (Select) 17] X >= X by (Meta) 18] Y >= Y by (Meta) We can thus remove the following rules: plus(0, X) => 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]): size node(X, Y) >? s(sum(map(size, Y))) plus(s(X), Y) >? s(plus(X, Y)) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[s(x_1)]] = x_1 [[sum(x_1)]] = x_1 We choose Lex = {} and Mul = {@_{o -> o}, map, node, plus, size}, and the following precedence: @_{o -> o} > map > node > size > plus Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: @_{o -> o}(size, node(X, Y)) > map(size, Y) plus(X, Y) >= plus(X, Y) With these choices, we have: 1] @_{o -> o}(size, node(X, Y)) > map(size, Y) because [2], by definition 2] @_{o -> o}*(size, node(X, Y)) >= map(size, Y) because @_{o -> o} > map, [3] and [4], by (Copy) 3] @_{o -> o}*(size, node(X, Y)) >= size because @_{o -> o} > size, by (Copy) 4] @_{o -> o}*(size, node(X, Y)) >= Y because [5], by (Select) 5] node(X, Y) >= Y because [6], by (Star) 6] node*(X, Y) >= Y because [7], by (Select) 7] Y >= Y by (Meta) 8] plus(X, Y) >= plus(X, Y) because plus in Mul, [9] and [10], by (Fun) 9] X >= X by (Meta) 10] Y >= Y by (Meta) We can thus remove the following rules: size node(X, Y) => s(sum(map(size, 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(s(X), Y) >? s(plus(X, Y)) We use a recursive path ordering as defined in [Kop12, Chapter 5]. We choose Lex = {} and Mul = {plus, s}, and the following precedence: plus > s 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) We can thus remove the following rules: plus(s(X), Y) => s(plus(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.