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