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