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