We consider the system 468. Alphabet: 0 : [] --> nat add : [nat * nat] --> nat rec : [nat -> nat -> nat * nat * nat] --> nat s : [nat] --> nat Rules: rec(/\x./\y.X(x, y), Y, 0) => Y rec(/\x./\y.X(x, y), Y, s(Z)) => X(Z, rec(/\z./\u.X(z, u), Y, Z)) add(X, Y) => rec(/\x./\y.s(y), X, Y) add(X, 0) => X add(X, s(Y)) => s(add(X, Y)) We use the dependency pair framework as described in [Kop12, Ch. 6/7], with dynamic dependency pairs. We thus obtain the following dependency pair problem (P_0, R_0, minimal, formative): Dependency Pairs P_0: 0] rec#(/\x./\y.X(x, y), Y, s(Z)) =#> X(Z, rec(/\z./\u.X(z, u), Y, Z)) 1] rec#(/\x./\y.X(x, y), Y, s(Z)) =#> rec#(/\z./\u.X(z, u), Y, Z) {X : 2} 2] rec#(/\x./\y.X(x, y), Y, s(Z)) =#> X(z, u) {X : 2} 3] add#(X, Y) =#> rec#(/\x./\y.s(y), X, Y) 4] add#(X, s(Y)) =#> add#(X, Y) Rules R_0: rec(/\x./\y.X(x, y), Y, 0) => Y rec(/\x./\y.X(x, y), Y, s(Z)) => X(Z, rec(/\z./\u.X(z, u), Y, Z)) add(X, Y) => rec(/\x./\y.s(y), X, Y) add(X, 0) => X add(X, s(Y)) => s(add(X, Y)) Thus, the original system is terminating if (P_0, R_0, minimal, formative) is finite. We consider the dependency pair problem (P_0, R_0, minimal, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. As the system is abstraction-simple and the formative flag is set, it suffices to find a tagged reduction pair [Kop12, Def. 6.70]. Thus, we must orient: rec#(/\x./\y.X(x, y), Y, s(Z)) >? X(Z, rec(/\z./\u.X(z, u), Y, Z)) rec#(/\x./\y.X(x, y), Y, s(Z)) >? rec#(/\z./\u.X(z, u), Y, Z) rec#(/\x./\y.X(x, y), Y, s(Z)) >? X(~c0, ~c1) add#(X, Y) >? rec#(/\x./\y.s-(y), X, Y) add#(X, s(Y)) >? add#(X, Y) rec(/\x./\y.X(x, y), Y, 0) >= Y rec(/\x./\y.X(x, y), Y, s(Z)) >= X(Z, rec(/\z./\u.X(z, u), Y, Z)) add(X, Y) >= rec(/\x./\y.s-(y), X, Y) add(X, 0) >= X add(X, s(Y)) >= s(add(X, Y)) s-(X) >= s(X) Since this representation is not advantageous for the higher-order recursive path ordering, we present the strict requirements in their unextended form, which is not problematic since for any F, s and substituion gamma: (F s)gamma beta-reduces to F(s)gamma.) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[~c0]] = _|_ [[~c1]] = _|_ We choose Lex = {} and Mul = {0, add, add#, rec, rec#, s, s-}, and the following precedence: add > add# > rec# > rec > s- > s > 0 Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: rec#(/\x./\y.X(x, y), Y, s(Z)) >= X(Z, rec(/\x./\y.X(x, y), Y, Z)) rec#(/\x./\y.X(x, y), Y, s(Z)) >= rec#(/\x./\y.X(x, y), Y, Z) rec#(/\x./\y.X(x, y), Y, s(Z)) > X(_|_, _|_) add#(X, Y) >= rec#(/\x./\y.s-(y), X, Y) add#(X, s(Y)) > add#(X, Y) rec(/\x./\y.X(x, y), Y, 0) >= Y rec(/\x./\y.X(x, y), Y, s(Z)) >= X(Z, rec(/\x./\y.X(x, y), Y, Z)) add(X, Y) >= rec(/\x./\y.s-(y), X, Y) add(X, 0) >= X add(X, s(Y)) >= s(add(X, Y)) s-(X) >= s(X) With these choices, we have: 1] rec#(/\x./\y.X(x, y), Y, s(Z)) >= X(Z, rec(/\x./\y.X(x, y), Y, Z)) because [2], by (Star) 2] rec#*(/\x./\y.X(x, y), Y, s(Z)) >= X(Z, rec(/\x./\y.X(x, y), Y, Z)) because [3], by (Select) 3] X(rec#*(/\x./\y.X(x, y), Y, s(Z)), rec#*(/\z./\u.X(z, u), Y, s(Z))) >= X(Z, rec(/\x./\y.X(x, y), Y, Z)) because [4] and [8], by (Meta) 4] rec#*(/\x./\y.X(x, y), Y, s(Z)) >= Z because [5], by (Select) 5] s(Z) >= Z because [6], by (Star) 6] s*(Z) >= Z because [7], by (Select) 7] Z >= Z by (Meta) 8] rec#*(/\x./\y.X(x, y), Y, s(Z)) >= rec(/\x./\y.X(x, y), Y, Z) because rec# > rec, [9], [15] and [4], by (Copy) 9] rec#*(/\x./\y.X(x, y), Y, s(Z)) >= /\x./\y.X(x, y) because [10], by (Select) 10] /\x./\z.X(x, z) >= /\x./\z.X(x, z) because [11], by (Abs) 11] /\z.X(y, z) >= /\z.X(y, z) because [12], by (Abs) 12] X(y, x) >= X(y, x) because [13] and [14], by (Meta) 13] y >= y by (Var) 14] x >= x by (Var) 15] rec#*(/\z./\u.X(z, u), Y, s(Z)) >= Y because [16], by (Select) 16] Y >= Y by (Meta) 17] rec#(/\x./\y.X(x, y), Y, s(Z)) >= rec#(/\x./\y.X(x, y), Y, Z) because rec# in Mul, [18], [19] and [20], by (Fun) 18] /\x./\z.X(x, z) >= /\x./\z.X(x, z) because [11], by (Abs) 19] Y >= Y by (Meta) 20] s(Z) >= Z because [6], by (Star) 21] rec#(/\x./\y.X(x, y), Y, s(Z)) > X(_|_, _|_) because [22], by definition 22] rec#*(/\x./\y.X(x, y), Y, s(Z)) >= X(_|_, _|_) because [23], by (Select) 23] X(rec#*(/\x./\y.X(x, y), Y, s(Z)), rec#*(/\z./\u.X(z, u), Y, s(Z))) >= X(_|_, _|_) because [24] and [25], by (Meta) 24] rec#*(/\x./\y.X(x, y), Y, s(Z)) >= _|_ by (Bot) 25] rec#*(/\x./\y.X(x, y), Y, s(Z)) >= _|_ by (Bot) 26] add#(X, Y) >= rec#(/\x./\y.s-(y), X, Y) because [27], by (Star) 27] add#*(X, Y) >= rec#(/\x./\y.s-(y), X, Y) because add# > rec#, [28], [33] and [35], by (Copy) 28] add#*(X, Y) >= /\y./\z.s-(z) because [29], by (F-Abs) 29] add#*(X, Y, x) >= /\z.s-(z) because [30], by (F-Abs) 30] add#*(X, Y, x, y) >= s-(y) because add# > s- and [31], by (Copy) 31] add#*(X, Y, x, y) >= y because [32], by (Select) 32] y >= y by (Var) 33] add#*(X, Y) >= X because [34], by (Select) 34] X >= X by (Meta) 35] add#*(X, Y) >= Y because [36], by (Select) 36] Y >= Y by (Meta) 37] add#(X, s(Y)) > add#(X, Y) because [38], by definition 38] add#*(X, s(Y)) >= add#(X, Y) because add# in Mul, [39] and [40], by (Stat) 39] X >= X by (Meta) 40] s(Y) > Y because [41], by definition 41] s*(Y) >= Y because [42], by (Select) 42] Y >= Y by (Meta) 43] rec(/\x./\y.X(x, y), Y, 0) >= Y because [44], by (Star) 44] rec*(/\x./\y.X(x, y), Y, 0) >= Y because [45], by (Select) 45] Y >= Y by (Meta) 46] rec(/\x./\y.X(x, y), Y, s(Z)) >= X(Z, rec(/\x./\y.X(x, y), Y, Z)) because [47], by (Star) 47] rec*(/\x./\y.X(x, y), Y, s(Z)) >= X(Z, rec(/\x./\y.X(x, y), Y, Z)) because [48], by (Select) 48] X(rec*(/\x./\y.X(x, y), Y, s(Z)), rec*(/\z./\u.X(z, u), Y, s(Z))) >= X(Z, rec(/\x./\y.X(x, y), Y, Z)) because [49] and [50], by (Meta) 49] rec*(/\x./\y.X(x, y), Y, s(Z)) >= Z because [20], by (Select) 50] rec*(/\x./\y.X(x, y), Y, s(Z)) >= rec(/\x./\y.X(x, y), Y, Z) because rec in Mul, [18], [19] and [51], by (Stat) 51] s(Z) > Z because [52], by definition 52] s*(Z) >= Z because [7], by (Select) 53] add(X, Y) >= rec(/\x./\y.s-(y), X, Y) because [54], by (Star) 54] add*(X, Y) >= rec(/\x./\y.s-(y), X, Y) because add > rec, [55], [60] and [61], by (Copy) 55] add*(X, Y) >= /\y./\z.s-(z) because [56], by (F-Abs) 56] add*(X, Y, x) >= /\z.s-(z) because [57], by (F-Abs) 57] add*(X, Y, x, y) >= s-(y) because add > s- and [58], by (Copy) 58] add*(X, Y, x, y) >= y because [59], by (Select) 59] y >= y by (Var) 60] add*(X, Y) >= X because [34], by (Select) 61] add*(X, Y) >= Y because [36], by (Select) 62] add(X, 0) >= X because [63], by (Star) 63] add*(X, 0) >= X because [64], by (Select) 64] X >= X by (Meta) 65] add(X, s(Y)) >= s(add(X, Y)) because [66], by (Star) 66] add*(X, s(Y)) >= s(add(X, Y)) because add > s and [67], by (Copy) 67] add*(X, s(Y)) >= add(X, Y) because add in Mul, [39] and [40], by (Stat) 68] s-(X) >= s(X) because [69], by (Star) 69] s-*(X) >= s(X) because s- > s and [70], by (Copy) 70] s-*(X) >= X because [71], by (Select) 71] X >= X by (Meta) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_0, R_0, minimal, formative) by (P_1, R_0, minimal, formative), where P_1 consists of: rec#(/\x./\y.X(x, y), Y, s(Z)) =#> X(Z, rec(/\z./\u.X(z, u), Y, Z)) rec#(/\x./\y.X(x, y), Y, s(Z)) =#> rec#(/\z./\u.X(z, u), Y, Z) add#(X, Y) =#> rec#(/\x./\y.s(y), X, Y) Thus, the original system is terminating if (P_1, R_0, minimal, formative) is finite. We consider the dependency pair problem (P_1, R_0, minimal, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. As the system is abstraction-simple and the formative flag is set, it suffices to find a tagged reduction pair [Kop12, Def. 6.70]. Thus, we must orient: rec#(/\x./\y.X(x, y), Y, s(Z)) >? X(Z, rec(/\z./\u.X(z, u), Y, Z)) rec#(/\x./\y.X(x, y), Y, s(Z)) >? rec#(/\z./\u.X(z, u), Y, Z) add#(X, Y) >? rec#(/\x./\y.s-(y), X, Y) rec(/\x./\y.X(x, y), Y, 0) >= Y rec(/\x./\y.X(x, y), Y, s(Z)) >= X(Z, rec(/\z./\u.X(z, u), Y, Z)) add(X, Y) >= rec(/\x./\y.s-(y), X, Y) add(X, 0) >= X add(X, s(Y)) >= s(add(X, Y)) s-(X) >= s(X) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( add#(X, Y) ) = #argfun-add##(rec#(/\x./\y.s-(y), X, Y)) Since this representation is not advantageous for the higher-order recursive path ordering, we present the strict requirements in their unextended form, which is not problematic since for any F, s and substituion gamma: (F s)gamma beta-reduces to F(s)gamma.) We use a recursive path ordering as defined in [Kop12, Chapter 5]. We choose Lex = {} and Mul = {#argfun-add##, 0, add, add#, rec, rec#, s, s-}, and the following precedence: 0 > add > add# > rec = rec# > s- > s > #argfun-add## With these choices, we have: 1] rec#(/\x./\y.X(x, y), Y, s(Z)) >= X(Z, rec(/\x./\y.X(x, y), Y, Z)) because [2], by (Star) 2] rec#*(/\x./\y.X(x, y), Y, s(Z)) >= X(Z, rec(/\x./\y.X(x, y), Y, Z)) because [3], by (Select) 3] X(rec#*(/\x./\y.X(x, y), Y, s(Z)), rec#*(/\z./\u.X(z, u), Y, s(Z))) >= X(Z, rec(/\x./\y.X(x, y), Y, Z)) because [4] and [8], by (Meta) 4] rec#*(/\x./\y.X(x, y), Y, s(Z)) >= Z because [5], by (Select) 5] s(Z) >= Z because [6], by (Star) 6] s*(Z) >= Z because [7], by (Select) 7] Z >= Z by (Meta) 8] rec#*(/\x./\y.X(x, y), Y, s(Z)) >= rec(/\x./\y.X(x, y), Y, Z) because rec# = rec, rec# in Mul, [9], [14] and [15], by (Stat) 9] /\x./\z.X(x, z) >= /\x./\z.X(x, z) because [10], by (Abs) 10] /\z.X(y, z) >= /\z.X(y, z) because [11], by (Abs) 11] X(y, x) >= X(y, x) because [12] and [13], by (Meta) 12] y >= y by (Var) 13] x >= x by (Var) 14] Y >= Y by (Meta) 15] s(Z) > Z because [16], by definition 16] s*(Z) >= Z because [7], by (Select) 17] rec#(/\x./\y.X(x, y), Y, s(Z)) > rec#(/\x./\y.X(x, y), Y, Z) because [18], by definition 18] rec#*(/\x./\y.X(x, y), Y, s(Z)) >= rec#(/\x./\y.X(x, y), Y, Z) because rec# in Mul, [9], [14] and [15], by (Stat) 19] #argfun-add##(rec#(/\x./\y.s-(y), X, Y)) >= rec#(/\x./\y.s-(y), X, Y) because [20], by (Star) 20] #argfun-add##*(rec#(/\x./\y.s-(y), X, Y)) >= rec#(/\x./\y.s-(y), X, Y) because [21], by (Select) 21] rec#(/\x./\y.s-(y), X, Y) >= rec#(/\x./\y.s-(y), X, Y) because rec# in Mul, [22], [26] and [27], by (Fun) 22] /\x./\y.s-(y) >= /\x./\y.s-(y) because [23], by (Abs) 23] /\y.s-(y) >= /\y.s-(y) because [24], by (Abs) 24] s-(x) >= s-(x) because s- in Mul and [25], by (Fun) 25] x >= x by (Var) 26] X >= X by (Meta) 27] Y >= Y by (Meta) 28] rec(/\x./\y.X(x, y), Y, 0) >= Y because [29], by (Star) 29] rec*(/\x./\y.X(x, y), Y, 0) >= Y because [30], by (Select) 30] Y >= Y by (Meta) 31] rec(/\x./\y.X(x, y), Y, s(Z)) >= X(Z, rec(/\x./\y.X(x, y), Y, Z)) because [32], by (Star) 32] rec*(/\x./\y.X(x, y), Y, s(Z)) >= X(Z, rec(/\x./\y.X(x, y), Y, Z)) because [33], by (Select) 33] X(rec*(/\x./\y.X(x, y), Y, s(Z)), rec*(/\z./\u.X(z, u), Y, s(Z))) >= X(Z, rec(/\x./\y.X(x, y), Y, Z)) because [34] and [35], by (Meta) 34] rec*(/\x./\y.X(x, y), Y, s(Z)) >= Z because [5], by (Select) 35] rec*(/\x./\y.X(x, y), Y, s(Z)) >= rec(/\x./\y.X(x, y), Y, Z) because rec in Mul, [9], [14] and [15], by (Stat) 36] add(X, Y) >= rec(/\x./\y.s-(y), X, Y) because [37], by (Star) 37] add*(X, Y) >= rec(/\x./\y.s-(y), X, Y) because add > rec, [38], [43] and [44], by (Copy) 38] add*(X, Y) >= /\y./\z.s-(z) because [39], by (F-Abs) 39] add*(X, Y, x) >= /\z.s-(z) because [40], by (F-Abs) 40] add*(X, Y, x, y) >= s-(y) because add > s- and [41], by (Copy) 41] add*(X, Y, x, y) >= y because [42], by (Select) 42] y >= y by (Var) 43] add*(X, Y) >= X because [26], by (Select) 44] add*(X, Y) >= Y because [27], by (Select) 45] add(X, 0) >= X because [46], by (Star) 46] add*(X, 0) >= X because [47], by (Select) 47] X >= X by (Meta) 48] add(X, s(Y)) >= s(add(X, Y)) because [49], by (Star) 49] add*(X, s(Y)) >= s(add(X, Y)) because add > s and [50], by (Copy) 50] add*(X, s(Y)) >= add(X, Y) because add in Mul, [51] and [52], by (Stat) 51] X >= X by (Meta) 52] s(Y) > Y because [53], by definition 53] s*(Y) >= Y because [54], by (Select) 54] Y >= Y by (Meta) 55] s-(X) >= s(X) because [56], by (Star) 56] s-*(X) >= s(X) because s- > s and [57], by (Copy) 57] s-*(X) >= X because [58], by (Select) 58] X >= X by (Meta) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_1, R_0, minimal, formative) by (P_2, R_0, minimal, formative), where P_2 consists of: rec#(/\x./\y.X(x, y), Y, s(Z)) =#> X(Z, rec(/\z./\u.X(z, u), Y, Z)) add#(X, Y) =#> rec#(/\x./\y.s(y), X, Y) Thus, the original system is terminating if (P_2, R_0, minimal, formative) is finite. We consider the dependency pair problem (P_2, R_0, minimal, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. As the system is abstraction-simple and the formative flag is set, it suffices to find a tagged reduction pair [Kop12, Def. 6.70]. Thus, we must orient: rec#(/\x./\y.X(x, y), Y, s(Z)) >? X(Z, rec(/\z./\u.X(z, u), Y, Z)) add#(X, Y) >? rec#(/\x./\y.s-(y), X, Y) rec(/\x./\y.X(x, y), Y, 0) >= Y rec(/\x./\y.X(x, y), Y, s(Z)) >= X(Z, rec(/\z./\u.X(z, u), Y, Z)) add(X, Y) >= rec(/\x./\y.s-(y), X, Y) add(X, 0) >= X add(X, s(Y)) >= s(add(X, Y)) s-(X) >= s(X) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( add#(X, Y) ) = #argfun-add##(rec#(/\x./\y.s-(y), X, Y)) Since this representation is not advantageous for the higher-order recursive path ordering, we present the strict requirements in their unextended form, which is not problematic since for any F, s and substituion gamma: (F s)gamma beta-reduces to F(s)gamma.) We use a recursive path ordering as defined in [Kop12, Chapter 5]. We choose Lex = {} and Mul = {#argfun-add##, 0, add, add#, rec, rec#, s, s-}, and the following precedence: #argfun-add## > add > add# > s- > s > 0 > rec# > rec With these choices, we have: 1] rec#(/\x./\y.X(x, y), Y, s(Z)) > X(Z, rec(/\x./\y.X(x, y), Y, Z)) because [2], by definition 2] rec#*(/\x./\y.X(x, y), Y, s(Z)) >= X(Z, rec(/\x./\y.X(x, y), Y, Z)) because [3], by (Select) 3] X(rec#*(/\x./\y.X(x, y), Y, s(Z)), rec#*(/\z./\u.X(z, u), Y, s(Z))) >= X(Z, rec(/\x./\y.X(x, y), Y, Z)) because [4] and [8], by (Meta) 4] rec#*(/\x./\y.X(x, y), Y, s(Z)) >= Z because [5], by (Select) 5] s(Z) >= Z because [6], by (Star) 6] s*(Z) >= Z because [7], by (Select) 7] Z >= Z by (Meta) 8] rec#*(/\x./\y.X(x, y), Y, s(Z)) >= rec(/\x./\y.X(x, y), Y, Z) because rec# > rec, [9], [15] and [4], by (Copy) 9] rec#*(/\x./\y.X(x, y), Y, s(Z)) >= /\x./\y.X(x, y) because [10], by (Select) 10] /\x./\z.X(x, z) >= /\x./\z.X(x, z) because [11], by (Abs) 11] /\z.X(y, z) >= /\z.X(y, z) because [12], by (Abs) 12] X(y, x) >= X(y, x) because [13] and [14], by (Meta) 13] y >= y by (Var) 14] x >= x by (Var) 15] rec#*(/\z./\u.X(z, u), Y, s(Z)) >= Y because [16], by (Select) 16] Y >= Y by (Meta) 17] #argfun-add##(rec#(/\x./\y.s-(y), X, Y)) >= rec#(/\x./\y.s-(y), X, Y) because [18], by (Star) 18] #argfun-add##*(rec#(/\x./\y.s-(y), X, Y)) >= rec#(/\x./\y.s-(y), X, Y) because [19], by (Select) 19] rec#(/\x./\y.s-(y), X, Y) >= rec#(/\x./\y.s-(y), X, Y) because rec# in Mul, [20], [24] and [25], by (Fun) 20] /\x./\y.s-(y) >= /\x./\y.s-(y) because [21], by (Abs) 21] /\y.s-(y) >= /\y.s-(y) because [22], by (Abs) 22] s-(x) >= s-(x) because s- in Mul and [23], by (Fun) 23] x >= x by (Var) 24] X >= X by (Meta) 25] Y >= Y by (Meta) 26] rec(/\x./\y.X(x, y), Y, 0) >= Y because [27], by (Star) 27] rec*(/\x./\y.X(x, y), Y, 0) >= Y because [28], by (Select) 28] Y >= Y by (Meta) 29] rec(/\x./\y.X(x, y), Y, s(Z)) >= X(Z, rec(/\x./\y.X(x, y), Y, Z)) because [30], by (Star) 30] rec*(/\x./\y.X(x, y), Y, s(Z)) >= X(Z, rec(/\x./\y.X(x, y), Y, Z)) because [31], by (Select) 31] X(rec*(/\x./\y.X(x, y), Y, s(Z)), rec*(/\z./\u.X(z, u), Y, s(Z))) >= X(Z, rec(/\x./\y.X(x, y), Y, Z)) because [32] and [33], by (Meta) 32] rec*(/\x./\y.X(x, y), Y, s(Z)) >= Z because [5], by (Select) 33] rec*(/\x./\y.X(x, y), Y, s(Z)) >= rec(/\x./\y.X(x, y), Y, Z) because rec in Mul, [34], [35] and [36], by (Stat) 34] /\x./\z.X(x, z) >= /\x./\z.X(x, z) because [11], by (Abs) 35] Y >= Y by (Meta) 36] s(Z) > Z because [37], by definition 37] s*(Z) >= Z because [7], by (Select) 38] add(X, Y) >= rec(/\x./\y.s-(y), X, Y) because [39], by (Star) 39] add*(X, Y) >= rec(/\x./\y.s-(y), X, Y) because add > rec, [40], [45] and [46], by (Copy) 40] add*(X, Y) >= /\y./\z.s-(z) because [41], by (F-Abs) 41] add*(X, Y, x) >= /\z.s-(z) because [42], by (F-Abs) 42] add*(X, Y, x, y) >= s-(y) because add > s- and [43], by (Copy) 43] add*(X, Y, x, y) >= y because [44], by (Select) 44] y >= y by (Var) 45] add*(X, Y) >= X because [24], by (Select) 46] add*(X, Y) >= Y because [25], by (Select) 47] add(X, 0) >= X because [48], by (Star) 48] add*(X, 0) >= X because [49], by (Select) 49] X >= X by (Meta) 50] add(X, s(Y)) >= s(add(X, Y)) because [51], by (Star) 51] add*(X, s(Y)) >= s(add(X, Y)) because add > s and [52], by (Copy) 52] add*(X, s(Y)) >= add(X, Y) because add in Mul, [53] and [54], by (Stat) 53] X >= X by (Meta) 54] s(Y) > Y because [55], by definition 55] s*(Y) >= Y because [56], by (Select) 56] Y >= Y by (Meta) 57] s-(X) >= s(X) because [58], by (Star) 58] s-*(X) >= s(X) because s- > s and [59], by (Copy) 59] s-*(X) >= X because [60], by (Select) 60] X >= X by (Meta) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_2, R_0, minimal, formative) by (P_3, R_0, minimal, formative), where P_3 consists of: add#(X, Y) =#> rec#(/\x./\y.s(y), X, Y) Thus, the original system is terminating if (P_3, R_0, minimal, formative) is finite. We consider the dependency pair problem (P_3, R_0, minimal, formative). We place the elements of P in a dependency graph approximation G (see e.g. [Kop12, Thm. 7.27, 7.29], as follows: * 0 : This graph has no strongly connected components. By [Kop12, Thm. 7.31], this implies finiteness of the dependency pair problem. As all dependency pair problems were succesfully simplified with sound (and complete) processors until nothing remained, we conclude termination. +++ Citations +++ [Kop12] C. Kop. Higher Order Termination. PhD Thesis, 2012.