We consider the system Applicative_05__TreeLevels. Alphabet: append : [a * a] --> a combine : [a * a] --> a cons : [a * a] --> a levels : [] --> a -> a map : [a -> a * a] --> a nil : [] --> a node : [a * a] --> a zip : [a * a] --> a Rules: map(f, nil) => nil map(f, cons(x, y)) => cons(f x, map(f, y)) append(x, nil) => x append(nil, x) => x append(cons(x, y), z) => cons(x, append(y, z)) zip(nil, x) => x zip(x, nil) => x zip(cons(x, y), cons(z, u)) => cons(append(x, z), zip(y, u)) combine(x, nil) => x combine(x, cons(y, z)) => combine(zip(x, y), z) levels node(x, y) => cons(cons(x, nil), combine(nil, map(levels, 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)) append(X, nil) >? X append(nil, X) >? X append(cons(X, Y), Z) >? cons(X, append(Y, Z)) zip(nil, X) >? X zip(X, nil) >? X zip(cons(X, Y), cons(Z, U)) >? cons(append(X, Z), zip(Y, U)) combine(X, nil) >? X combine(X, cons(Y, Z)) >? combine(zip(X, Y), Z) levels node(X, Y) >? cons(cons(X, nil), combine(nil, map(levels, Y))) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[combine(x_1, x_2)]] = combine(x_2, x_1) [[nil]] = _|_ We choose Lex = {combine} and Mul = {@_{o -> o}, append, cons, levels, map, node, zip}, and the following precedence: node > levels > combine > @_{o -> o} = map > append = zip > cons 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(@_{o -> o}(F, X), map(F, Y)) append(X, _|_) > X append(_|_, X) >= X append(cons(X, Y), Z) > cons(X, append(Y, Z)) zip(_|_, X) >= X zip(X, _|_) >= X zip(cons(X, Y), cons(Z, U)) > cons(append(X, Z), zip(Y, U)) combine(X, _|_) >= X combine(X, cons(Y, Z)) >= combine(zip(X, Y), Z) @_{o -> o}(levels, node(X, Y)) >= cons(cons(X, _|_), combine(_|_, map(levels, Y))) With these choices, we have: 1] map(F, _|_) > _|_ because [2], by definition 2] map*(F, _|_) >= _|_ by (Bot) 3] map(F, cons(X, Y)) > cons(@_{o -> o}(F, X), map(F, Y)) because [4], by definition 4] map*(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) because map > cons, [5] and [10], by (Copy) 5] map*(F, cons(X, Y)) >= @_{o -> o}(F, X) because map = @_{o -> o}, map in Mul, [6] and [7], by (Stat) 6] F >= F by (Meta) 7] cons(X, Y) > X because [8], by definition 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, [6] and [11], by (Stat) 11] cons(X, Y) > Y because [12], by definition 12] cons*(X, Y) >= Y because [13], by (Select) 13] Y >= Y by (Meta) 14] append(X, _|_) > X because [15], by definition 15] append*(X, _|_) >= X because [16], by (Select) 16] X >= X by (Meta) 17] append(_|_, X) >= X because [18], by (Star) 18] append*(_|_, X) >= X because [19], by (Select) 19] X >= X by (Meta) 20] append(cons(X, Y), Z) > cons(X, append(Y, Z)) because [21], by definition 21] append*(cons(X, Y), Z) >= cons(X, append(Y, Z)) because append > cons, [22] and [26], by (Copy) 22] append*(cons(X, Y), Z) >= X because [23], by (Select) 23] cons(X, Y) >= X because [24], by (Star) 24] cons*(X, Y) >= X because [25], by (Select) 25] X >= X by (Meta) 26] append*(cons(X, Y), Z) >= append(Y, Z) because append in Mul, [27] and [30], by (Stat) 27] cons(X, Y) > Y because [28], by definition 28] cons*(X, Y) >= Y because [29], by (Select) 29] Y >= Y by (Meta) 30] Z >= Z by (Meta) 31] zip(_|_, X) >= X because [32], by (Star) 32] zip*(_|_, X) >= X because [33], by (Select) 33] X >= X by (Meta) 34] zip(X, _|_) >= X because [35], by (Star) 35] zip*(X, _|_) >= X because [36], by (Select) 36] X >= X by (Meta) 37] zip(cons(X, Y), cons(Z, U)) > cons(append(X, Z), zip(Y, U)) because [38], by definition 38] zip*(cons(X, Y), cons(Z, U)) >= cons(append(X, Z), zip(Y, U)) because zip > cons, [39] and [46], by (Copy) 39] zip*(cons(X, Y), cons(Z, U)) >= append(X, Z) because zip = append, zip in Mul, [40] and [43], by (Stat) 40] cons(X, Y) >= X because [41], by (Star) 41] cons*(X, Y) >= X because [42], by (Select) 42] X >= X by (Meta) 43] cons(Z, U) > Z because [44], by definition 44] cons*(Z, U) >= Z because [45], by (Select) 45] Z >= Z by (Meta) 46] zip*(cons(X, Y), cons(Z, U)) >= zip(Y, U) because zip in Mul, [47] and [50], by (Stat) 47] cons(X, Y) >= Y because [48], by (Star) 48] cons*(X, Y) >= Y because [49], by (Select) 49] Y >= Y by (Meta) 50] cons(Z, U) > U because [51], by definition 51] cons*(Z, U) >= U because [52], by (Select) 52] U >= U by (Meta) 53] combine(X, _|_) >= X because [54], by (Star) 54] combine*(X, _|_) >= X because [55], by (Select) 55] X >= X by (Meta) 56] combine(X, cons(Y, Z)) >= combine(zip(X, Y), Z) because [57], by (Star) 57] combine*(X, cons(Y, Z)) >= combine(zip(X, Y), Z) because [58], [61] and [68], by (Stat) 58] cons(Y, Z) > Z because [59], by definition 59] cons*(Y, Z) >= Z because [60], by (Select) 60] Z >= Z by (Meta) 61] combine*(X, cons(Y, Z)) >= zip(X, Y) because combine > zip, [62] and [64], by (Copy) 62] combine*(X, cons(Y, Z)) >= X because [63], by (Select) 63] X >= X by (Meta) 64] combine*(X, cons(Y, Z)) >= Y because [65], by (Select) 65] cons(Y, Z) >= Y because [66], by (Star) 66] cons*(Y, Z) >= Y because [67], by (Select) 67] Y >= Y by (Meta) 68] combine*(X, cons(Y, Z)) >= Z because [69], by (Select) 69] cons(Y, Z) >= Z because [59], by (Star) 70] @_{o -> o}(levels, node(X, Y)) >= cons(cons(X, _|_), combine(_|_, map(levels, Y))) because [71], by (Star) 71] @_{o -> o}*(levels, node(X, Y)) >= cons(cons(X, _|_), combine(_|_, map(levels, Y))) because [72], by (Select) 72] node(X, Y) >= cons(cons(X, _|_), combine(_|_, map(levels, Y))) because [73], by (Star) 73] node*(X, Y) >= cons(cons(X, _|_), combine(_|_, map(levels, Y))) because node > cons, [74] and [78], by (Copy) 74] node*(X, Y) >= cons(X, _|_) because node > cons, [75] and [77], by (Copy) 75] node*(X, Y) >= X because [76], by (Select) 76] X >= X by (Meta) 77] node*(X, Y) >= _|_ by (Bot) 78] node*(X, Y) >= combine(_|_, map(levels, Y)) because node > combine, [77] and [79], by (Copy) 79] node*(X, Y) >= map(levels, Y) because node > map, [80] and [81], by (Copy) 80] node*(X, Y) >= levels because node > levels, by (Copy) 81] node*(X, Y) >= Y because [82], by (Select) 82] Y >= Y by (Meta) We can thus remove the following rules: map(F, nil) => nil map(F, cons(X, Y)) => cons(F X, map(F, Y)) append(X, nil) => X append(cons(X, Y), Z) => cons(X, append(Y, Z)) zip(cons(X, Y), cons(Z, U)) => cons(append(X, Z), zip(Y, U)) We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): append(nil, X) >? X zip(nil, X) >? X zip(X, nil) >? X combine(X, nil) >? X combine(X, cons(Y, Z)) >? combine(zip(X, Y), Z) levels node(X, Y) >? cons(cons(X, nil), combine(nil, map(levels, Y))) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[combine(x_1, x_2)]] = combine(x_2, x_1) [[nil]] = _|_ We choose Lex = {combine} and Mul = {@_{o -> o}, append, cons, levels, map, node, zip}, and the following precedence: append > @_{o -> o} > levels > combine > cons > node > map > zip Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: append(_|_, X) > X zip(_|_, X) > X zip(X, _|_) >= X combine(X, _|_) >= X combine(X, cons(Y, Z)) >= combine(zip(X, Y), Z) @_{o -> o}(levels, node(X, Y)) > cons(cons(X, _|_), combine(_|_, map(levels, Y))) With these choices, we have: 1] append(_|_, X) > X because [2], by definition 2] append*(_|_, X) >= X because [3], by (Select) 3] X >= X by (Meta) 4] zip(_|_, X) > X because [5], by definition 5] zip*(_|_, X) >= X because [6], by (Select) 6] X >= X by (Meta) 7] zip(X, _|_) >= X because [8], by (Star) 8] zip*(X, _|_) >= X because [9], by (Select) 9] X >= X by (Meta) 10] combine(X, _|_) >= X because [11], by (Star) 11] combine*(X, _|_) >= X because [12], by (Select) 12] X >= X by (Meta) 13] combine(X, cons(Y, Z)) >= combine(zip(X, Y), Z) because [14], by (Star) 14] combine*(X, cons(Y, Z)) >= combine(zip(X, Y), Z) because [15], [18] and [25], by (Stat) 15] cons(Y, Z) > Z because [16], by definition 16] cons*(Y, Z) >= Z because [17], by (Select) 17] Z >= Z by (Meta) 18] combine*(X, cons(Y, Z)) >= zip(X, Y) because combine > zip, [19] and [21], by (Copy) 19] combine*(X, cons(Y, Z)) >= X because [20], by (Select) 20] X >= X by (Meta) 21] combine*(X, cons(Y, Z)) >= Y because [22], by (Select) 22] cons(Y, Z) >= Y because [23], by (Star) 23] cons*(Y, Z) >= Y because [24], by (Select) 24] Y >= Y by (Meta) 25] combine*(X, cons(Y, Z)) >= Z because [26], by (Select) 26] cons(Y, Z) >= Z because [16], by (Star) 27] @_{o -> o}(levels, node(X, Y)) > cons(cons(X, _|_), combine(_|_, map(levels, Y))) because [28], by definition 28] @_{o -> o}*(levels, node(X, Y)) >= cons(cons(X, _|_), combine(_|_, map(levels, Y))) because [29], by (Select) 29] levels @_{o -> o}*(levels, node(X, Y)) >= cons(cons(X, _|_), combine(_|_, map(levels, Y))) because [30] 30] levels*(@_{o -> o}*(levels, node(X, Y))) >= cons(cons(X, _|_), combine(_|_, map(levels, Y))) because levels > cons, [31] and [38], by (Copy) 31] levels*(@_{o -> o}*(levels, node(X, Y))) >= cons(X, _|_) because levels > cons, [32] and [37], by (Copy) 32] levels*(@_{o -> o}*(levels, node(X, Y))) >= X because [33], by (Select) 33] @_{o -> o}*(levels, node(X, Y)) >= X because [34], by (Select) 34] node(X, Y) >= X because [35], by (Star) 35] node*(X, Y) >= X because [36], by (Select) 36] X >= X by (Meta) 37] levels*(@_{o -> o}*(levels, node(X, Y))) >= _|_ by (Bot) 38] levels*(@_{o -> o}*(levels, node(X, Y))) >= combine(_|_, map(levels, Y)) because levels > combine, [37] and [39], by (Copy) 39] levels*(@_{o -> o}*(levels, node(X, Y))) >= map(levels, Y) because [40], by (Select) 40] @_{o -> o}*(levels, node(X, Y)) >= map(levels, Y) because @_{o -> o} > map, [41] and [42], by (Copy) 41] @_{o -> o}*(levels, node(X, Y)) >= levels because @_{o -> o} > levels, by (Copy) 42] @_{o -> o}*(levels, node(X, Y)) >= Y because [43], by (Select) 43] node(X, Y) >= Y because [44], by (Star) 44] node*(X, Y) >= Y because [45], by (Select) 45] Y >= Y by (Meta) We can thus remove the following rules: append(nil, X) => X zip(nil, X) => X levels node(X, Y) => cons(cons(X, nil), combine(nil, map(levels, 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]): zip(X, nil) >? X combine(X, nil) >? X combine(X, cons(Y, Z)) >? combine(zip(X, Y), Z) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[combine(x_1, x_2)]] = combine(x_2, x_1) We choose Lex = {combine} and Mul = {cons, nil, zip}, and the following precedence: combine > zip > nil > cons Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: zip(X, nil) > X combine(X, nil) > X combine(X, cons(Y, Z)) >= combine(zip(X, Y), Z) With these choices, we have: 1] zip(X, nil) > X because [2], by definition 2] zip*(X, nil) >= X because [3], by (Select) 3] X >= X by (Meta) 4] combine(X, nil) > X because [5], by definition 5] combine*(X, nil) >= X because [6], by (Select) 6] X >= X by (Meta) 7] combine(X, cons(Y, Z)) >= combine(zip(X, Y), Z) because [8], by (Star) 8] combine*(X, cons(Y, Z)) >= combine(zip(X, Y), Z) because [9], [12] and [19], by (Stat) 9] cons(Y, Z) > Z because [10], by definition 10] cons*(Y, Z) >= Z because [11], by (Select) 11] Z >= Z by (Meta) 12] combine*(X, cons(Y, Z)) >= zip(X, Y) because combine > zip, [13] and [15], by (Copy) 13] combine*(X, cons(Y, Z)) >= X because [14], by (Select) 14] X >= X by (Meta) 15] combine*(X, cons(Y, Z)) >= Y because [16], by (Select) 16] cons(Y, Z) >= Y because [17], by (Star) 17] cons*(Y, Z) >= Y because [18], by (Select) 18] Y >= Y by (Meta) 19] combine*(X, cons(Y, Z)) >= Z because [20], by (Select) 20] cons(Y, Z) >= Z because [10], by (Star) We can thus remove the following rules: zip(X, nil) => X combine(X, nil) => 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]): combine(X, cons(Y, Z)) >? combine(zip(X, Y), Z) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[combine(x_1, x_2)]] = combine(x_2, x_1) We choose Lex = {combine} and Mul = {cons, zip}, and the following precedence: combine > zip > cons Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: combine(X, cons(Y, Z)) > combine(zip(X, Y), Z) With these choices, we have: 1] combine(X, cons(Y, Z)) > combine(zip(X, Y), Z) because [2], by definition 2] combine*(X, cons(Y, Z)) >= combine(zip(X, Y), Z) because [3], [6] and [13], by (Stat) 3] cons(Y, Z) > Z because [4], by definition 4] cons*(Y, Z) >= Z because [5], by (Select) 5] Z >= Z by (Meta) 6] combine*(X, cons(Y, Z)) >= zip(X, Y) because combine > zip, [7] and [9], by (Copy) 7] combine*(X, cons(Y, Z)) >= X because [8], by (Select) 8] X >= X by (Meta) 9] combine*(X, cons(Y, Z)) >= Y because [10], by (Select) 10] cons(Y, Z) >= Y because [11], by (Star) 11] cons*(Y, Z) >= Y because [12], by (Select) 12] Y >= Y by (Meta) 13] combine*(X, cons(Y, Z)) >= Z because [14], by (Select) 14] cons(Y, Z) >= Z because [4], by (Star) We can thus remove the following rules: combine(X, cons(Y, Z)) => combine(zip(X, Y), Z) 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.