We consider the system 519. Alphabet: 0 : [string] --> string 1 : [string] --> string false : [] --> bool fold : [bool -> bool * bool -> bool * bool * string] --> bool nil : [] --> string not : [bool] --> bool true : [] --> bool Rules: not(true) => false not(false) => true fold(/\x.X(x), /\y.Y(y), Z, nil) => Z fold(/\x.X(x), /\y.Y(y), Z, 0(U)) => fold(/\z.X(z), /\u.Y(u), X(Z), U) fold(/\x.X(x), /\y.Y(y), Z, 1(U)) => fold(/\z.X(z), /\u.Y(u), Y(Z), 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]): not(true) >? false not(false) >? true fold(/\x.X(x), /\y.Y(y), Z, nil) >? Z fold(/\x.X(x), /\y.Y(y), Z, 0(U)) >? fold(/\z.X(z), /\u.Y(u), X(Z), U) fold(/\x.X(x), /\y.Y(y), Z, 1(U)) >? fold(/\z.X(z), /\u.Y(u), Y(Z), U) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[false]] = _|_ [[fold(x_1, x_2, x_3, x_4)]] = fold(x_4, x_3, x_2, x_1) [[true]] = _|_ We choose Lex = {fold} and Mul = {0, 1, nil, not}, and the following precedence: 0 > 1 > fold > nil > not Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: not(_|_) >= _|_ not(_|_) >= _|_ fold(/\x.X(x), /\y.Y(y), Z, nil) >= Z fold(/\x.X(x), /\y.Y(y), Z, 0(U)) > fold(/\x.X(x), /\y.Y(y), X(Z), U) fold(/\x.X(x), /\y.Y(y), Z, 1(U)) >= fold(/\x.X(x), /\y.Y(y), Y(Z), U) With these choices, we have: 1] not(_|_) >= _|_ by (Bot) 2] not(_|_) >= _|_ by (Bot) 3] fold(/\x.X(x), /\y.Y(y), Z, nil) >= Z because [4], by (Star) 4] fold*(/\x.X(x), /\y.Y(y), Z, nil) >= Z because [5], by (Select) 5] Z >= Z by (Meta) 6] fold(/\x.X(x), /\y.Y(y), Z, 0(U)) > fold(/\x.X(x), /\y.Y(y), X(Z), U) because [7], by definition 7] fold*(/\x.X(x), /\y.Y(y), Z, 0(U)) >= fold(/\x.X(x), /\y.Y(y), X(Z), U) because [8], [11], [15], [19] and [23], by (Stat) 8] 0(U) > U because [9], by definition 9] 0*(U) >= U because [10], by (Select) 10] U >= U by (Meta) 11] fold*(/\x.X(x), /\y.Y(y), Z, 0(U)) >= /\x.X(x) because [12], by (Select) 12] /\y.X(y) >= /\y.X(y) because [13], by (Abs) 13] X(x) >= X(x) because [14], by (Meta) 14] x >= x by (Var) 15] fold*(/\y.X(y), /\z.Y(z), Z, 0(U)) >= /\y.Y(y) because [16], by (Select) 16] /\z.Y(z) >= /\z.Y(z) because [17], by (Abs) 17] Y(y) >= Y(y) because [18], by (Meta) 18] y >= y by (Var) 19] fold*(/\z.X(z), /\u.Y(u), Z, 0(U)) >= X(Z) because [20], by (Select) 20] X(fold*(/\z.X(z), /\u.Y(u), Z, 0(U))) >= X(Z) because [21], by (Meta) 21] fold*(/\z.X(z), /\u.Y(u), Z, 0(U)) >= Z because [22], by (Select) 22] Z >= Z by (Meta) 23] fold*(/\z.X(z), /\u.Y(u), Z, 0(U)) >= U because [24], by (Select) 24] 0(U) >= U because [9], by (Star) 25] fold(/\x.X(x), /\y.Y(y), Z, 1(U)) >= fold(/\x.X(x), /\y.Y(y), Y(Z), U) because [26], by (Star) 26] fold*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= fold(/\x.X(x), /\y.Y(y), Y(Z), U) because [27], [30], [35], [40] and [44], by (Stat) 27] 1(U) > U because [28], by definition 28] 1*(U) >= U because [29], by (Select) 29] U >= U by (Meta) 30] fold*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= /\x.X(x) because [31], by (F-Abs) 31] fold*(/\x.X(x), /\y.Y(y), Z, 1(U), z) >= X(z) because [32], by (Select) 32] X(fold*(/\x.X(x), /\y.Y(y), Z, 1(U), z)) >= X(z) because [33], by (Meta) 33] fold*(/\x.X(x), /\y.Y(y), Z, 1(U), z) >= z because [34], by (Select) 34] z >= z by (Var) 35] fold*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= /\x.Y(x) because [36], by (F-Abs) 36] fold*(/\x.X(x), /\y.Y(y), Z, 1(U), u) >= Y(u) because [37], by (Select) 37] Y(fold*(/\x.X(x), /\y.Y(y), Z, 1(U), u)) >= Y(u) because [38], by (Meta) 38] fold*(/\x.X(x), /\y.Y(y), Z, 1(U), u) >= u because [39], by (Select) 39] u >= u by (Var) 40] fold*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= Y(Z) because [41], by (Select) 41] Y(fold*(/\x.X(x), /\y.Y(y), Z, 1(U))) >= Y(Z) because [42], by (Meta) 42] fold*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= Z because [43], by (Select) 43] Z >= Z by (Meta) 44] fold*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= U because [45], by (Select) 45] 1(U) >= U because [28], by (Star) We can thus remove the following rules: fold(/\x.X(x), /\y.Y(y), Z, 0(U)) => fold(/\z.X(z), /\u.Y(u), X(Z), 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]): not(true) >? false not(false) >? true fold(/\x.X(x), /\y.Y(y), Z, nil) >? Z fold(/\x.X(x), /\y.Y(y), Z, 1(U)) >? fold(/\z.X(z), /\u.Y(u), Y(Z), U) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[false]] = _|_ [[fold(x_1, x_2, x_3, x_4)]] = fold(x_4, x_1, x_3, x_2) [[true]] = _|_ We choose Lex = {fold} and Mul = {1, nil, not}, and the following precedence: 1 > fold > nil > not Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: not(_|_) >= _|_ not(_|_) >= _|_ fold(/\x.X(x), /\y.Y(y), Z, nil) > Z fold(/\x.X(x), /\y.Y(y), Z, 1(U)) >= fold(/\x.X(x), /\y.Y(y), Y(Z), U) With these choices, we have: 1] not(_|_) >= _|_ by (Bot) 2] not(_|_) >= _|_ by (Bot) 3] fold(/\x.X(x), /\y.Y(y), Z, nil) > Z because [4], by definition 4] fold*(/\x.X(x), /\y.Y(y), Z, nil) >= Z because [5], by (Select) 5] Z >= Z by (Meta) 6] fold(/\x.X(x), /\y.Y(y), Z, 1(U)) >= fold(/\x.X(x), /\y.Y(y), Y(Z), U) because [7], by (Star) 7] fold*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= fold(/\x.X(x), /\y.Y(y), Y(Z), U) because [8], [11], [15], [19] and [23], by (Stat) 8] 1(U) > U because [9], by definition 9] 1*(U) >= U because [10], by (Select) 10] U >= U by (Meta) 11] fold*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= /\x.X(x) because [12], by (Select) 12] /\y.X(y) >= /\y.X(y) because [13], by (Abs) 13] X(x) >= X(x) because [14], by (Meta) 14] x >= x by (Var) 15] fold*(/\y.X(y), /\z.Y(z), Z, 1(U)) >= /\y.Y(y) because [16], by (Select) 16] /\z.Y(z) >= /\z.Y(z) because [17], by (Abs) 17] Y(y) >= Y(y) because [18], by (Meta) 18] y >= y by (Var) 19] fold*(/\z.X(z), /\u.Y(u), Z, 1(U)) >= Y(Z) because [20], by (Select) 20] Y(fold*(/\z.X(z), /\u.Y(u), Z, 1(U))) >= Y(Z) because [21], by (Meta) 21] fold*(/\z.X(z), /\u.Y(u), Z, 1(U)) >= Z because [22], by (Select) 22] Z >= Z by (Meta) 23] fold*(/\z.X(z), /\u.Y(u), Z, 1(U)) >= U because [24], by (Select) 24] 1(U) >= U because [9], by (Star) We can thus remove the following rules: fold(/\x.X(x), /\y.Y(y), Z, nil) => 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]): not(true) >? false not(false) >? true fold(/\x.X(x), /\y.Y(y), Z, 1(U)) >? fold(/\z.X(z), /\u.Y(u), Y(Z), U) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[false]] = _|_ [[fold(x_1, x_2, x_3, x_4)]] = fold(x_4, x_1, x_3, x_2) [[true]] = _|_ We choose Lex = {fold} and Mul = {1, not}, and the following precedence: 1 > fold > not Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: not(_|_) >= _|_ not(_|_) >= _|_ fold(/\x.X(x), /\y.Y(y), Z, 1(U)) > fold(/\x.X(x), /\y.Y(y), Y(Z), U) With these choices, we have: 1] not(_|_) >= _|_ by (Bot) 2] not(_|_) >= _|_ by (Bot) 3] fold(/\x.X(x), /\y.Y(y), Z, 1(U)) > fold(/\x.X(x), /\y.Y(y), Y(Z), U) because [4], by definition 4] fold*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= fold(/\x.X(x), /\y.Y(y), Y(Z), U) because [5], [8], [12], [16] and [20], by (Stat) 5] 1(U) > U because [6], by definition 6] 1*(U) >= U because [7], by (Select) 7] U >= U by (Meta) 8] fold*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= /\x.X(x) because [9], by (Select) 9] /\y.X(y) >= /\y.X(y) because [10], by (Abs) 10] X(x) >= X(x) because [11], by (Meta) 11] x >= x by (Var) 12] fold*(/\y.X(y), /\z.Y(z), Z, 1(U)) >= /\y.Y(y) because [13], by (Select) 13] /\z.Y(z) >= /\z.Y(z) because [14], by (Abs) 14] Y(y) >= Y(y) because [15], by (Meta) 15] y >= y by (Var) 16] fold*(/\z.X(z), /\u.Y(u), Z, 1(U)) >= Y(Z) because [17], by (Select) 17] Y(fold*(/\z.X(z), /\u.Y(u), Z, 1(U))) >= Y(Z) because [18], by (Meta) 18] fold*(/\z.X(z), /\u.Y(u), Z, 1(U)) >= Z because [19], by (Select) 19] Z >= Z by (Meta) 20] fold*(/\z.X(z), /\u.Y(u), Z, 1(U)) >= U because [21], by (Select) 21] 1(U) >= U because [6], by (Star) We can thus remove the following rules: fold(/\x.X(x), /\y.Y(y), Z, 1(U)) => fold(/\z.X(z), /\u.Y(u), Y(Z), 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]): not(true) >? false not(false) >? true We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: false = 0 not = \y0.3 + 3y0 true = 1 Using this interpretation, the requirements translate to: [[not(true)]] = 6 > 0 = [[false]] [[not(false)]] = 3 > 1 = [[true]] We can thus remove the following rules: not(true) => false not(false) => true 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.