We consider the system h49. Alphabet: 0 : [] --> nat mult : [nat * nat] --> nat plus : [nat * nat] --> nat plus3 : [nat] --> nat -> nat -> nat rec : [nat * nat * nat -> nat -> nat] --> nat s : [nat] --> nat succ2 : [] --> nat -> nat -> nat xap : [nat -> nat -> nat * nat] --> nat -> nat yap : [nat -> nat * nat] --> nat Rules: rec(0, x, /\y./\z.yap(xap(f, y), z)) => x rec(s(x), y, /\z./\u.yap(xap(f, z), u)) => yap(xap(f, x), rec(x, y, /\v./\w.yap(xap(f, v), w))) succ2 x y => s(y) plus(x, y) => rec(x, y, succ2) plus3(x) y z => plus(x, plus(y, z)) mult(x, y) => rec(x, 0, plus3(y)) xap(f, x) => f x yap(f, x) => f x This AFS is converted to an AFSM simply by replacing all free variables by meta-variables (with arity 0). Symbol xap is an encoding for application that is only used in innocuous ways. We can simplify the program (without losing non-termination) by removing it. This gives: Alphabet: 0 : [] --> nat mult : [nat * nat] --> nat plus : [nat * nat] --> nat plus3 : [nat] --> nat -> nat -> nat rec : [nat * nat * nat -> nat -> nat] --> nat s : [nat] --> nat succ2 : [] --> nat -> nat -> nat yap : [nat -> nat * nat] --> nat Rules: rec(0, X, /\x./\y.yap(F(x), y)) => X rec(s(X), Y, /\x./\y.yap(F(x), y)) => yap(F(X), rec(X, Y, /\z./\u.yap(F(z), u))) succ2 X Y => s(Y) plus(X, Y) => rec(X, Y, succ2) plus3(X) Y Z => plus(X, plus(Y, Z)) mult(X, Y) => rec(X, 0, plus3(Y)) yap(F, X) => F X We observe that the rules contain a first-order subset: succ2 X Y => s(Y) Moreover, the system is finitely branching. Thus, by [Kop12, Thm. 7.55], we may omit all first-order dependency pairs from the dependency pair problem (DP(R), R) if this first-order part is Ce-terminating when seen as a many-sorted first-order TRS. According to the external first-order termination prover, this system is indeed Ce-terminating: || proof of resources/system.trs || # AProVE Commit ID: d84c10301d352dfd14de2104819581f4682260f5 fuhs 20130616 || || || Termination w.r.t. Q of the given QTRS could be proven: || || (0) QTRS || (1) QTRSRRRProof [EQUIVALENT] || (2) QTRS || (3) RisEmptyProof [EQUIVALENT] || (4) YES || || || ---------------------------------------- || || (0) || Obligation: || Q restricted rewrite system: || The TRS R consists of the following rules: || || succ2(%X, %Y) -> s(%Y) || ~PAIR(%X, %Y) -> %X || ~PAIR(%X, %Y) -> %Y || || Q is empty. || || ---------------------------------------- || || (1) QTRSRRRProof (EQUIVALENT) || Used ordering: || Polynomial interpretation [POLO]: || || POL(s(x_1)) = 1 + x_1 || POL(succ2(x_1, x_2)) = 2 + x_1 + 2*x_2 || POL(~PAIR(x_1, x_2)) = 2 + x_1 + x_2 || With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly: || || succ2(%X, %Y) -> s(%Y) || ~PAIR(%X, %Y) -> %X || ~PAIR(%X, %Y) -> %Y || || || || || ---------------------------------------- || || (2) || Obligation: || Q restricted rewrite system: || R is empty. || Q is empty. || || ---------------------------------------- || || (3) RisEmptyProof (EQUIVALENT) || The TRS R is empty. Hence, termination is trivially proven. || ---------------------------------------- || || (4) || YES || We use the dependency pair framework as described in [Kop12, Ch. 6/7], with dynamic dependency pairs. After applying [Kop12, Thm. 7.22] to denote collapsing dependency pairs in an extended form, we thus obtain the following dependency pair problem (P_0, R_0, minimal, all): Dependency Pairs P_0: 0] rec#(s(X), Y, /\x./\y.yap(F(x), y)) =#> yap#(F(X), rec(X, Y, /\z./\u.yap(F(z), u))) 1] rec#(s(X), Y, /\x./\y.yap(F(x), y)) =#> F(X) 2] rec#(s(X), Y, /\x./\y.yap(F(x), y)) =#> rec#(X, Y, /\z./\u.yap(F(z), u)) 3] rec#(s(X), Y, /\x./\y.yap(F(x), y)) =#> yap#(F(z), u) 4] rec#(s(X), Y, /\x./\y.yap(F(x), y)) =#> F(z) 5] plus#(X, Y) =#> rec#(X, Y, succ2) 6] plus#(X, Y) =#> succ2# 7] plus3(X) Y Z =#> plus#(X, plus(Y, Z)) 8] plus3(X) Y Z =#> plus#(Y, Z) 9] mult#(X, Y) =#> rec#(X, 0, plus3(Y)) 10] mult#(X, Y) =#> plus3#(Y) 11] yap#(F, X) =#> F(X) Rules R_0: rec(0, X, /\x./\y.yap(F(x), y)) => X rec(s(X), Y, /\x./\y.yap(F(x), y)) => yap(F(X), rec(X, Y, /\z./\u.yap(F(z), u))) succ2 X Y => s(Y) plus(X, Y) => rec(X, Y, succ2) plus3(X) Y Z => plus(X, plus(Y, Z)) mult(X, Y) => rec(X, 0, plus3(Y)) yap(F, X) => F X Thus, the original system is terminating if (P_0, R_0, minimal, all) is finite. We consider the dependency pair problem (P_0, R_0, minimal, all). We place the elements of P in a dependency graph approximation G (see e.g. [Kop12, Thm. 7.27, 7.29], as follows: * 0 : 11 * 1 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 * 2 : 0, 1, 2, 3, 4 * 3 : * 4 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 * 5 : * 6 : * 7 : 5, 6 * 8 : 5, 6 * 9 : 0, 1, 2, 3, 4 * 10 : * 11 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11 This graph has the following strongly connected components: P_1: rec#(s(X), Y, /\x./\y.yap(F(x), y)) =#> yap#(F(X), rec(X, Y, /\z./\u.yap(F(z), u))) rec#(s(X), Y, /\x./\y.yap(F(x), y)) =#> F(X) rec#(s(X), Y, /\x./\y.yap(F(x), y)) =#> rec#(X, Y, /\z./\u.yap(F(z), u)) rec#(s(X), Y, /\x./\y.yap(F(x), y)) =#> F(z) mult#(X, Y) =#> rec#(X, 0, plus3(Y)) yap#(F, X) =#> F(X) By [Kop12, Thm. 7.31], we may replace any dependency pair problem (P_0, R_0, m, f) by (P_1, R_0, m, f). Thus, the original system is terminating if (P_1, R_0, minimal, all) is finite. We consider the dependency pair problem (P_1, R_0, minimal, all). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: rec#(s(X), Y, /\x./\y.yap(F(x), y)) >? yap#(F(X), rec(X, Y, /\z./\u.yap(F(z), u))) rec#(s(X), Y, /\x./\y.yap(F(x), y)) >? F(X) ~c0 rec#(s(X), Y, /\x./\y.yap(F(x), y)) >? rec#(X, Y, /\z./\u.yap(F(z), u)) rec#(s(X), Y, /\x./\y.yap(F(x), y)) >? F(~c2) ~c1 mult#(X, Y) >? rec#(X, 0, plus3(Y)) yap#(F, X) >? F(X) rec(0, X, /\x./\y.yap(F(x), y)) >= X rec(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\z./\u.yap(F(z), u))) succ2 X Y >= s(Y) plus(X, Y) >= rec(X, Y, succ2) plus3(X) Y Z >= plus(X, plus(Y, Z)) mult(X, Y) >= rec(X, 0, plus3(Y)) yap(F, X) >= F X mult(X, Y) >= mult#(X, Y) rec(X, Y, F) >= rec#(X, Y, F) yap(F, X) >= yap#(F, X) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( mult#(X, Y) ) = #argfun-mult##(rec#(X, 0, plus3(Y))) pi( yap#(F, X) ) = #argfun-yap##(F 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: [[#argfun-yap##(x_1)]] = x_1 [[0]] = _|_ [[succ2]] = _|_ [[~c0]] = _|_ [[~c1]] = _|_ [[~c2]] = _|_ We choose Lex = {} and Mul = {#argfun-mult##, @_{o -> o -> o}, @_{o -> o}, mult, mult#, plus, plus3, rec, rec#, s, yap, yap#}, and the following precedence: mult > mult# > #argfun-mult## = plus3 > @_{o -> o -> o} > s > yap > plus > yap# > rec = rec# > @_{o -> o} Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: rec#(s(X), Y, /\x./\y.yap(F(x), y)) >= @_{o -> o}(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) rec#(s(X), Y, /\x./\y.yap(F(x), y)) > @_{o -> o}(F(X), _|_) rec#(s(X), Y, /\x./\y.yap(F(x), y)) >= rec#(X, Y, /\x./\y.yap(F(x), y)) rec#(s(X), Y, /\x./\y.yap(F(x), y)) >= @_{o -> o}(F(_|_), _|_) #argfun-mult##(rec#(X, _|_, plus3(Y))) > rec#(X, _|_, plus3(Y)) @_{o -> o}(F, X) >= @_{o -> o}(F, X) rec(_|_, X, /\x./\y.yap(F(x), y)) >= X rec(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) @_{o -> o}(@_{o -> o -> o}(_|_, X), Y) >= s(Y) plus(X, Y) >= rec(X, Y, _|_) @_{o -> o}(@_{o -> o -> o}(plus3(X), Y), Z) >= plus(X, plus(Y, Z)) mult(X, Y) >= rec(X, _|_, plus3(Y)) yap(F, X) >= @_{o -> o}(F, X) mult(X, Y) >= #argfun-mult##(rec#(X, _|_, plus3(Y))) rec(X, Y, F) >= rec#(X, Y, F) yap(F, X) >= @_{o -> o}(F, X) With these choices, we have: 1] rec#(s(X), Y, /\x./\y.yap(F(x), y)) >= @_{o -> o}(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) because [2], by (Star) 2] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= @_{o -> o}(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) because rec# > @_{o -> o}, [3] and [10], by (Copy) 3] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= F(X) because [4], by (Select) 4] /\x.yap(F(rec#*(s(X), Y, /\y./\z.yap(F(y), z))), x) >= F(X) because [5], by (Eta)[Kop13:2] 5] F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(X) because [6], by (Meta) 6] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= X because [7], by (Select) 7] s(X) >= X because [8], by (Star) 8] s*(X) >= X because [9], by (Select) 9] X >= X by (Meta) 10] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= rec(X, Y, /\x./\y.yap(F(x), y)) because rec# = rec, rec# in Mul, [11], [13] and [14], by (Stat) 11] s(X) > X because [12], by definition 12] s*(X) >= X because [9], by (Select) 13] Y >= Y by (Meta) 14] /\x./\z.yap(F(x), z) >= /\x./\z.yap(F(x), z) because [15], by (Abs) 15] /\z.yap(F(y), z) >= /\z.yap(F(y), z) because [16], by (Abs) 16] yap(F(y), x) >= yap(F(y), x) because yap in Mul, [17] and [19], by (Fun) 17] F(y) >= F(y) because [18], by (Meta) 18] y >= y by (Var) 19] x >= x by (Var) 20] rec#(s(X), Y, /\x./\y.yap(F(x), y)) > @_{o -> o}(F(X), _|_) because [21], by definition 21] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= @_{o -> o}(F(X), _|_) because [22], by (Select) 22] yap(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= @_{o -> o}(F(X), _|_) because [23], by (Star) 23] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= @_{o -> o}(F(X), _|_) because yap > @_{o -> o}, [24] and [25], by (Copy) 24] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= F(X) because [5], by (Select) 25] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= _|_ by (Bot) 26] rec#(s(X), Y, /\x./\y.yap(F(x), y)) >= rec#(X, Y, /\x./\y.yap(F(x), y)) because rec# in Mul, [27], [13] and [14], by (Fun) 27] s(X) >= X because [12], by (Star) 28] rec#(s(X), Y, /\x./\y.yap(F(x), y)) >= @_{o -> o}(F(_|_), _|_) because [29], by (Star) 29] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= @_{o -> o}(F(_|_), _|_) because [30], by (Select) 30] yap(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= @_{o -> o}(F(_|_), _|_) because [31], by (Star) 31] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= @_{o -> o}(F(_|_), _|_) because yap > @_{o -> o}, [32] and [35], by (Copy) 32] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= F(_|_) because [33], by (Select) 33] F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(_|_) because [34], by (Meta) 34] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= _|_ by (Bot) 35] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= _|_ by (Bot) 36] #argfun-mult##(rec#(X, _|_, plus3(Y))) > rec#(X, _|_, plus3(Y)) because [37], by definition 37] #argfun-mult##*(rec#(X, _|_, plus3(Y))) >= rec#(X, _|_, plus3(Y)) because #argfun-mult## > rec#, [38], [42] and [43], by (Copy) 38] #argfun-mult##*(rec#(X, _|_, plus3(Y))) >= X because [39], by (Select) 39] rec#(X, _|_, plus3(Y)) >= X because [40], by (Star) 40] rec#*(X, _|_, plus3(Y)) >= X because [41], by (Select) 41] X >= X by (Meta) 42] #argfun-mult##*(rec#(X, _|_, plus3(Y))) >= _|_ by (Bot) 43] #argfun-mult##*(rec#(X, _|_, plus3(Y))) >= plus3(Y) because #argfun-mult## = plus3, #argfun-mult## in Mul and [44], by (Stat) 44] rec#(X, _|_, plus3(Y)) > Y because [45], by definition 45] rec#*(X, _|_, plus3(Y)) >= Y because [46], by (Select) 46] plus3(Y) rec#*(X, _|_, plus3(Y)) rec#*(X, _|_, plus3(Y)) >= Y because [47] 47] plus3*(Y, rec#*(X, _|_, plus3(Y)), rec#*(X, _|_, plus3(Y))) >= Y because [48], by (Select) 48] Y >= Y by (Meta) 49] @_{o -> o}(F, X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [50] and [51], by (Fun) 50] F >= F by (Meta) 51] X >= X by (Meta) 52] rec(_|_, X, /\x./\y.yap(F(x), y)) >= X because [53], by (Star) 53] rec*(_|_, X, /\x./\y.yap(F(x), y)) >= X because [54], by (Select) 54] X >= X by (Meta) 55] rec(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) because [56], by (Star) 56] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) because [57], by (Select) 57] yap(F(rec*(s(X), Y, /\x./\y.yap(F(x), y))), rec*(s(X), Y, /\z./\u.yap(F(z), u))) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) because yap in Mul, [58] and [64], by (Fun) 58] F(rec*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(X) because [59], by (Meta) 59] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= X because [60], by (Select) 60] yap(F(rec*(s(X), Y, /\x./\y.yap(F(x), y))), rec*(s(X), Y, /\z./\u.yap(F(z), u))) >= X because [61], by (Star) 61] yap*(F(rec*(s(X), Y, /\x./\y.yap(F(x), y))), rec*(s(X), Y, /\z./\u.yap(F(z), u))) >= X because [62], by (Select) 62] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= X because [63], by (Select) 63] s(X) >= X because [12], by (Star) 64] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= rec(X, Y, /\x./\y.yap(F(x), y)) because rec in Mul, [11], [13] and [14], by (Stat) 65] @_{o -> o}(@_{o -> o -> o}(_|_, X), Y) >= s(Y) because [66], by (Star) 66] @_{o -> o}*(@_{o -> o -> o}(_|_, X), Y) >= s(Y) because [67], by (Select) 67] @_{o -> o -> o}(_|_, X) @_{o -> o}*(@_{o -> o -> o}(_|_, X), Y) >= s(Y) because [68] 68] @_{o -> o -> o}*(_|_, X, @_{o -> o}*(@_{o -> o -> o}(_|_, X), Y)) >= s(Y) because @_{o -> o -> o} > s and [69], by (Copy) 69] @_{o -> o -> o}*(_|_, X, @_{o -> o}*(@_{o -> o -> o}(_|_, X), Y)) >= Y because [70], by (Select) 70] @_{o -> o}*(@_{o -> o -> o}(_|_, X), Y) >= Y because [71], by (Select) 71] Y >= Y by (Meta) 72] plus(X, Y) >= rec(X, Y, _|_) because [73], by (Star) 73] plus*(X, Y) >= rec(X, Y, _|_) because plus > rec, [74], [76] and [78], by (Copy) 74] plus*(X, Y) >= X because [75], by (Select) 75] X >= X by (Meta) 76] plus*(X, Y) >= Y because [77], by (Select) 77] Y >= Y by (Meta) 78] plus*(X, Y) >= _|_ by (Bot) 79] @_{o -> o}(@_{o -> o -> o}(plus3(X), Y), Z) >= plus(X, plus(Y, Z)) because [80], by (Star) 80] @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= plus(X, plus(Y, Z)) because [81], by (Select) 81] @_{o -> o -> o}(plus3(X), Y) @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= plus(X, plus(Y, Z)) because [82] 82] @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= plus(X, plus(Y, Z)) because @_{o -> o -> o} > plus, [83] and [87], by (Copy) 83] @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= X because [84], by (Select) 84] plus3(X) @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= X because [85] 85] plus3*(X, @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)), @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z))) >= X because [86], by (Select) 86] X >= X by (Meta) 87] @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= plus(Y, Z) because [88], by (Select) 88] plus3(X) @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= plus(Y, Z) because [89] 89] plus3*(X, @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)), @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z))) >= plus(Y, Z) because plus3 > plus, [90] and [93], by (Copy) 90] plus3*(X, @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)), @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z))) >= Y because [91], by (Select) 91] @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= Y because [92], by (Select) 92] Y >= Y by (Meta) 93] plus3*(X, @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)), @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z))) >= Z because [94], by (Select) 94] @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= Z because [95], by (Select) 95] @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= Z because [96], by (Select) 96] Z >= Z by (Meta) 97] mult(X, Y) >= rec(X, _|_, plus3(Y)) because [98], by (Star) 98] mult*(X, Y) >= rec(X, _|_, plus3(Y)) because mult > rec, [99], [100] and [101], by (Copy) 99] mult*(X, Y) >= X because [41], by (Select) 100] mult*(X, Y) >= _|_ by (Bot) 101] mult*(X, Y) >= plus3(Y) because mult > plus3 and [102], by (Copy) 102] mult*(X, Y) >= Y because [48], by (Select) 103] yap(F, X) >= @_{o -> o}(F, X) because [104], by (Star) 104] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [105] and [106], by (Copy) 105] yap*(F, X) >= F because [50], by (Select) 106] yap*(F, X) >= X because [51], by (Select) 107] mult(X, Y) >= #argfun-mult##(rec#(X, _|_, plus3(Y))) because [108], by (Star) 108] mult*(X, Y) >= #argfun-mult##(rec#(X, _|_, plus3(Y))) because mult > #argfun-mult## and [109], by (Copy) 109] mult*(X, Y) >= rec#(X, _|_, plus3(Y)) because mult > rec#, [110], [112] and [113], by (Copy) 110] mult*(X, Y) >= X because [111], by (Select) 111] X >= X by (Meta) 112] mult*(X, Y) >= _|_ by (Bot) 113] mult*(X, Y) >= plus3(Y) because mult > plus3 and [114], by (Copy) 114] mult*(X, Y) >= Y because [115], by (Select) 115] Y >= Y by (Meta) 116] rec(X, Y, F) >= rec#(X, Y, F) because rec = rec#, rec in Mul, [117], [118] and [119], by (Fun) 117] X >= X by (Meta) 118] Y >= Y by (Meta) 119] F >= F by (Meta) 120] yap(F, X) >= @_{o -> o}(F, X) because [121], by (Star) 121] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [122] and [124], by (Copy) 122] yap*(F, X) >= F because [123], by (Select) 123] F >= F by (Meta) 124] yap*(F, X) >= X because [125], by (Select) 125] 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, all) by (P_2, R_0, minimal, all), where P_2 consists of: rec#(s(X), Y, /\x./\y.yap(F(x), y)) =#> yap#(F(X), rec(X, Y, /\z./\u.yap(F(z), u))) rec#(s(X), Y, /\x./\y.yap(F(x), y)) =#> rec#(X, Y, /\z./\u.yap(F(z), u)) rec#(s(X), Y, /\x./\y.yap(F(x), y)) =#> F(z) yap#(F, X) =#> F(X) Thus, the original system is terminating if (P_2, R_0, minimal, all) is finite. We consider the dependency pair problem (P_2, R_0, minimal, all). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: rec#(s(X), Y, /\x./\y.yap(F(x), y)) >? yap#(F(X), rec(X, Y, /\z./\u.yap(F(z), u))) rec#(s(X), Y, /\x./\y.yap(F(x), y)) >? rec#(X, Y, /\z./\u.yap(F(z), u)) rec#(s(X), Y, /\x./\y.yap(F(x), y)) >? F(~c1) ~c0 yap#(F, X) >? F(X) rec(0, X, /\x./\y.yap(F(x), y)) >= X rec(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\z./\u.yap(F(z), u))) succ2 X Y >= s(Y) plus(X, Y) >= rec(X, Y, succ2) plus3(X) Y Z >= plus(X, plus(Y, Z)) mult(X, Y) >= rec(X, 0, plus3(Y)) yap(F, X) >= F X rec(X, Y, F) >= rec#(X, Y, F) yap(F, X) >= yap#(F, X) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( yap#(F, X) ) = #argfun-yap##(F 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: [[0]] = _|_ [[succ2]] = _|_ [[~c0]] = _|_ [[~c1]] = _|_ We choose Lex = {} and Mul = {#argfun-yap##, @_{o -> o -> o}, @_{o -> o}, mult, plus, plus3, rec, rec#, s, yap, yap#}, and the following precedence: mult = plus3 > @_{o -> o -> o} > plus > yap > #argfun-yap## > rec = rec# > @_{o -> o} = s > yap# Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: rec#(s(X), Y, /\x./\y.yap(F(x), y)) > #argfun-yap##(@_{o -> o}(F(X), rec(X, Y, /\x./\y.yap(F(x), y)))) rec#(s(X), Y, /\x./\y.yap(F(x), y)) >= rec#(X, Y, /\x./\y.yap(F(x), y)) rec#(s(X), Y, /\x./\y.yap(F(x), y)) > @_{o -> o}(F(_|_), _|_) #argfun-yap##(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) rec(_|_, X, /\x./\y.yap(F(x), y)) >= X rec(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) @_{o -> o}(@_{o -> o -> o}(_|_, X), Y) >= s(Y) plus(X, Y) >= rec(X, Y, _|_) @_{o -> o}(@_{o -> o -> o}(plus3(X), Y), Z) >= plus(X, plus(Y, Z)) mult(X, Y) >= rec(X, _|_, plus3(Y)) yap(F, X) >= @_{o -> o}(F, X) rec(X, Y, F) >= rec#(X, Y, F) yap(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) With these choices, we have: 1] rec#(s(X), Y, /\x./\y.yap(F(x), y)) > #argfun-yap##(@_{o -> o}(F(X), rec(X, Y, /\x./\y.yap(F(x), y)))) because [2], by definition 2] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= #argfun-yap##(@_{o -> o}(F(X), rec(X, Y, /\x./\y.yap(F(x), y)))) because [3], by (Select) 3] yap(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= #argfun-yap##(@_{o -> o}(F(X), rec(X, Y, /\x./\y.yap(F(x), y)))) because [4], by (Star) 4] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= #argfun-yap##(@_{o -> o}(F(X), rec(X, Y, /\x./\y.yap(F(x), y)))) because yap > #argfun-yap## and [5], by (Copy) 5] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= @_{o -> o}(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) because yap > @_{o -> o}, [6] and [12], by (Copy) 6] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= F(X) because [7], by (Select) 7] F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(X) because [8], by (Meta) 8] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= X because [9], by (Select) 9] s(X) >= X because [10], by (Star) 10] s*(X) >= X because [11], by (Select) 11] X >= X by (Meta) 12] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= rec(X, Y, /\x./\y.yap(F(x), y)) because [13], by (Select) 13] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= rec(X, Y, /\x./\y.yap(F(x), y)) because rec# = rec, rec# in Mul, [14], [16] and [17], by (Stat) 14] s(X) > X because [15], by definition 15] s*(X) >= X because [11], by (Select) 16] Y >= Y by (Meta) 17] /\x./\z.yap(F(x), z) >= /\x./\z.yap(F(x), z) because [18], by (Abs) 18] /\z.yap(F(y), z) >= /\z.yap(F(y), z) because [19], by (Abs) 19] yap(F(y), x) >= yap(F(y), x) because yap in Mul, [20] and [22], by (Fun) 20] F(y) >= F(y) because [21], by (Meta) 21] y >= y by (Var) 22] x >= x by (Var) 23] rec#(s(X), Y, /\x./\y.yap(F(x), y)) >= rec#(X, Y, /\x./\y.yap(F(x), y)) because rec# in Mul, [24], [16] and [17], by (Fun) 24] s(X) >= X because [15], by (Star) 25] rec#(s(X), Y, /\x./\y.yap(F(x), y)) > @_{o -> o}(F(_|_), _|_) because [26], by definition 26] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= @_{o -> o}(F(_|_), _|_) because rec# > @_{o -> o}, [27] and [31], by (Copy) 27] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= F(_|_) because [28], by (Select) 28] /\x.yap(F(rec#*(s(X), Y, /\y./\z.yap(F(y), z))), x) >= F(_|_) because [29], by (Eta)[Kop13:2] 29] F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(_|_) because [30], by (Meta) 30] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= _|_ by (Bot) 31] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= _|_ by (Bot) 32] #argfun-yap##(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) because [33], by (Star) 33] #argfun-yap##*(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) because [34], by (Select) 34] @_{o -> o}(F, X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [35] and [36], by (Fun) 35] F >= F by (Meta) 36] X >= X by (Meta) 37] rec(_|_, X, /\x./\y.yap(F(x), y)) >= X because [38], by (Star) 38] rec*(_|_, X, /\x./\y.yap(F(x), y)) >= X because [39], by (Select) 39] X >= X by (Meta) 40] rec(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) because [41], by (Star) 41] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) because [42], by (Select) 42] yap(F(rec*(s(X), Y, /\x./\y.yap(F(x), y))), rec*(s(X), Y, /\z./\u.yap(F(z), u))) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) because yap in Mul, [43] and [45], by (Fun) 43] F(rec*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(X) because [44], by (Meta) 44] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= X because [24], by (Select) 45] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= rec(X, Y, /\x./\y.yap(F(x), y)) because rec in Mul, [14], [16] and [17], by (Stat) 46] @_{o -> o}(@_{o -> o -> o}(_|_, X), Y) >= s(Y) because [47], by (Star) 47] @_{o -> o}*(@_{o -> o -> o}(_|_, X), Y) >= s(Y) because @_{o -> o} = s, @_{o -> o} in Mul and [48], by (Stat) 48] Y >= Y by (Meta) 49] plus(X, Y) >= rec(X, Y, _|_) because [50], by (Star) 50] plus*(X, Y) >= rec(X, Y, _|_) because plus > rec, [51], [53] and [55], by (Copy) 51] plus*(X, Y) >= X because [52], by (Select) 52] X >= X by (Meta) 53] plus*(X, Y) >= Y because [54], by (Select) 54] Y >= Y by (Meta) 55] plus*(X, Y) >= _|_ by (Bot) 56] @_{o -> o}(@_{o -> o -> o}(plus3(X), Y), Z) >= plus(X, plus(Y, Z)) because [57], by (Star) 57] @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= plus(X, plus(Y, Z)) because [58], by (Select) 58] @_{o -> o -> o}(plus3(X), Y) @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= plus(X, plus(Y, Z)) because [59] 59] @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= plus(X, plus(Y, Z)) because [60], by (Select) 60] plus3(X) @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= plus(X, plus(Y, Z)) because [61] 61] plus3*(X, @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)), @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z))) >= plus(X, plus(Y, Z)) because plus3 > plus, [62] and [64], by (Copy) 62] plus3*(X, @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)), @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z))) >= X because [63], by (Select) 63] X >= X by (Meta) 64] plus3*(X, @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)), @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z))) >= plus(Y, Z) because plus3 > plus, [65] and [68], by (Copy) 65] plus3*(X, @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)), @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z))) >= Y because [66], by (Select) 66] @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= Y because [67], by (Select) 67] Y >= Y by (Meta) 68] plus3*(X, @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)), @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z))) >= Z because [69], by (Select) 69] @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= Z because [70], by (Select) 70] @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= Z because [71], by (Select) 71] Z >= Z by (Meta) 72] mult(X, Y) >= rec(X, _|_, plus3(Y)) because [73], by (Star) 73] mult*(X, Y) >= rec(X, _|_, plus3(Y)) because mult > rec, [74], [76] and [77], by (Copy) 74] mult*(X, Y) >= X because [75], by (Select) 75] X >= X by (Meta) 76] mult*(X, Y) >= _|_ by (Bot) 77] mult*(X, Y) >= plus3(Y) because mult = plus3, mult in Mul and [78], by (Stat) 78] Y >= Y by (Meta) 79] yap(F, X) >= @_{o -> o}(F, X) because [80], by (Star) 80] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [81] and [82], by (Copy) 81] yap*(F, X) >= F because [35], by (Select) 82] yap*(F, X) >= X because [36], by (Select) 83] rec(X, Y, F) >= rec#(X, Y, F) because rec = rec#, rec in Mul, [84], [85] and [86], by (Fun) 84] X >= X by (Meta) 85] Y >= Y by (Meta) 86] F >= F by (Meta) 87] yap(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) because [88], by (Star) 88] yap*(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) because yap > #argfun-yap## and [89], by (Copy) 89] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [90] and [92], by (Copy) 90] yap*(F, X) >= F because [91], by (Select) 91] F >= F by (Meta) 92] yap*(F, X) >= X because [93], by (Select) 93] 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, all) by (P_3, R_0, minimal, all), where P_3 consists of: rec#(s(X), Y, /\x./\y.yap(F(x), y)) =#> rec#(X, Y, /\z./\u.yap(F(z), u)) yap#(F, X) =#> F(X) Thus, the original system is terminating if (P_3, R_0, minimal, all) is finite. We consider the dependency pair problem (P_3, R_0, minimal, all). We place the elements of P in a dependency graph approximation G (see e.g. [Kop12, Thm. 7.27, 7.29], as follows: * 0 : 0 * 1 : 0, 1 This graph has the following strongly connected components: P_4: rec#(s(X), Y, /\x./\y.yap(F(x), y)) =#> rec#(X, Y, /\z./\u.yap(F(z), u)) P_5: yap#(F, X) =#> F(X) By [Kop12, Thm. 7.31], we may replace any dependency pair problem (P_3, R_0, m, f) by (P_4, R_0, m, f) and (P_5, R_0, m, f). Thus, the original system is terminating if each of (P_4, R_0, minimal, all) and (P_5, R_0, minimal, all) is finite. We consider the dependency pair problem (P_5, R_0, minimal, all). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: yap#(F, X) >? F(X) rec(0, X, /\x./\y.yap(F(x), y)) >= X rec(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\z./\u.yap(F(z), u))) succ2 X Y >= s(Y) plus(X, Y) >= rec(X, Y, succ2) plus3(X) Y Z >= plus(X, plus(Y, Z)) mult(X, Y) >= rec(X, 0, plus3(Y)) yap(F, X) >= F X yap(F, X) >= yap#(F, X) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( yap#(F, X) ) = #argfun-yap##(F 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: [[0]] = _|_ We choose Lex = {} and Mul = {#argfun-yap##, @_{o -> o -> o}, @_{o -> o}, mult, plus, plus3, rec, s, succ2, yap, yap#}, and the following precedence: mult > plus3 > @_{o -> o -> o} > plus > succ2 > rec > yap > #argfun-yap## > @_{o -> o} > s > yap# Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: #argfun-yap##(@_{o -> o}(F, X)) > @_{o -> o}(F, X) rec(_|_, X, /\x./\y.yap(F(x), y)) >= X rec(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) @_{o -> o}(@_{o -> o -> o}(succ2, X), Y) >= s(Y) plus(X, Y) >= rec(X, Y, succ2) @_{o -> o}(@_{o -> o -> o}(plus3(X), Y), Z) >= plus(X, plus(Y, Z)) mult(X, Y) >= rec(X, _|_, plus3(Y)) yap(F, X) >= @_{o -> o}(F, X) yap(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) With these choices, we have: 1] #argfun-yap##(@_{o -> o}(F, X)) > @_{o -> o}(F, X) because [2], by definition 2] #argfun-yap##*(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) because [3], by (Select) 3] @_{o -> o}(F, X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [4] and [5], by (Fun) 4] F >= F by (Meta) 5] X >= X by (Meta) 6] rec(_|_, X, /\x./\y.yap(F(x), y)) >= X because [7], by (Star) 7] rec*(_|_, X, /\x./\y.yap(F(x), y)) >= X because [8], by (Select) 8] X >= X by (Meta) 9] rec(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) because [10], by (Star) 10] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) because rec > yap, [11] and [18], by (Copy) 11] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= F(X) because [12], by (Select) 12] /\x.yap(F(rec*(s(X), Y, /\y./\z.yap(F(y), z))), x) >= F(X) because [13], by (Eta)[Kop13:2] 13] F(rec*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(X) because [14], by (Meta) 14] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= X because [15], by (Select) 15] s(X) >= X because [16], by (Star) 16] s*(X) >= X because [17], by (Select) 17] X >= X by (Meta) 18] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= rec(X, Y, /\x./\y.yap(F(x), y)) because rec in Mul, [19], [21] and [22], by (Stat) 19] s(X) > X because [20], by definition 20] s*(X) >= X because [17], by (Select) 21] Y >= Y by (Meta) 22] /\x./\z.yap(F(x), z) >= /\x./\z.yap(F(x), z) because [23], by (Abs) 23] /\z.yap(F(y), z) >= /\z.yap(F(y), z) because [24], by (Abs) 24] yap(F(y), x) >= yap(F(y), x) because yap in Mul, [25] and [27], by (Fun) 25] F(y) >= F(y) because [26], by (Meta) 26] y >= y by (Var) 27] x >= x by (Var) 28] @_{o -> o}(@_{o -> o -> o}(succ2, X), Y) >= s(Y) because [29], by (Star) 29] @_{o -> o}*(@_{o -> o -> o}(succ2, X), Y) >= s(Y) because [30], by (Select) 30] @_{o -> o -> o}(succ2, X) @_{o -> o}*(@_{o -> o -> o}(succ2, X), Y) >= s(Y) because [31] 31] @_{o -> o -> o}*(succ2, X, @_{o -> o}*(@_{o -> o -> o}(succ2, X), Y)) >= s(Y) because [32], by (Select) 32] succ2 @_{o -> o -> o}*(succ2, X, @_{o -> o}*(@_{o -> o -> o}(succ2, X), Y)) @_{o -> o -> o}*(succ2, X, @_{o -> o}*(@_{o -> o -> o}(succ2, X), Y)) >= s(Y) because [33] 33] succ2*(@_{o -> o -> o}*(succ2, X, @_{o -> o}*(@_{o -> o -> o}(succ2, X), Y)), @_{o -> o -> o}*(succ2, X, @_{o -> o}*(@_{o -> o -> o}(succ2, X), Y))) >= s(Y) because succ2 > s and [34], by (Copy) 34] succ2*(@_{o -> o -> o}*(succ2, X, @_{o -> o}*(@_{o -> o -> o}(succ2, X), Y)), @_{o -> o -> o}*(succ2, X, @_{o -> o}*(@_{o -> o -> o}(succ2, X), Y))) >= Y because [35], by (Select) 35] @_{o -> o -> o}*(succ2, X, @_{o -> o}*(@_{o -> o -> o}(succ2, X), Y)) >= Y because [36], by (Select) 36] @_{o -> o}*(@_{o -> o -> o}(succ2, X), Y) >= Y because [37], by (Select) 37] Y >= Y by (Meta) 38] plus(X, Y) >= rec(X, Y, succ2) because [39], by (Star) 39] plus*(X, Y) >= rec(X, Y, succ2) because plus > rec, [40], [42] and [44], by (Copy) 40] plus*(X, Y) >= X because [41], by (Select) 41] X >= X by (Meta) 42] plus*(X, Y) >= Y because [43], by (Select) 43] Y >= Y by (Meta) 44] plus*(X, Y) >= succ2 because plus > succ2, by (Copy) 45] @_{o -> o}(@_{o -> o -> o}(plus3(X), Y), Z) >= plus(X, plus(Y, Z)) because [46], by (Star) 46] @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= plus(X, plus(Y, Z)) because [47], by (Select) 47] @_{o -> o -> o}(plus3(X), Y) @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= plus(X, plus(Y, Z)) because [48] 48] @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= plus(X, plus(Y, Z)) because @_{o -> o -> o} > plus, [49] and [53], by (Copy) 49] @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= X because [50], by (Select) 50] plus3(X) @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= X because [51] 51] plus3*(X, @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)), @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z))) >= X because [52], by (Select) 52] X >= X by (Meta) 53] @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= plus(Y, Z) because [54], by (Select) 54] @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= plus(Y, Z) because [55], by (Select) 55] @_{o -> o -> o}(plus3(X), Y) @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= plus(Y, Z) because [56] 56] @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= plus(Y, Z) because [57], by (Select) 57] plus3(X) @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= plus(Y, Z) because [58] 58] plus3*(X, @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)), @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z))) >= plus(Y, Z) because plus3 > plus, [59] and [62], by (Copy) 59] plus3*(X, @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)), @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z))) >= Y because [60], by (Select) 60] @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= Y because [61], by (Select) 61] Y >= Y by (Meta) 62] plus3*(X, @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)), @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z))) >= Z because [63], by (Select) 63] @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= Z because [64], by (Select) 64] @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= Z because [65], by (Select) 65] Z >= Z by (Meta) 66] mult(X, Y) >= rec(X, _|_, plus3(Y)) because [67], by (Star) 67] mult*(X, Y) >= rec(X, _|_, plus3(Y)) because mult > rec, [68], [70] and [71], by (Copy) 68] mult*(X, Y) >= X because [69], by (Select) 69] X >= X by (Meta) 70] mult*(X, Y) >= _|_ by (Bot) 71] mult*(X, Y) >= plus3(Y) because mult > plus3 and [72], by (Copy) 72] mult*(X, Y) >= Y because [73], by (Select) 73] Y >= Y by (Meta) 74] yap(F, X) >= @_{o -> o}(F, X) because [75], by (Star) 75] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [76] and [77], by (Copy) 76] yap*(F, X) >= F because [4], by (Select) 77] yap*(F, X) >= X because [5], by (Select) 78] yap(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) because [79], by (Star) 79] yap*(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) because yap > #argfun-yap## and [80], by (Copy) 80] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [81] and [83], by (Copy) 81] yap*(F, X) >= F because [82], by (Select) 82] F >= F by (Meta) 83] yap*(F, X) >= X because [84], by (Select) 84] X >= X by (Meta) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_5, R_0) by ({}, R_0). By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed. Thus, the original system is terminating if (P_4, R_0, minimal, all) is finite. We consider the dependency pair problem (P_4, R_0, minimal, all). We apply the subterm criterion with the following projection function: nu(rec#) = 1 Thus, we can orient the dependency pairs as follows: nu(rec#(s(X), Y, /\x./\y.yap(F(x), y))) = s(X) |> X = nu(rec#(X, Y, /\z./\u.yap(F(z), u))) By [FuhKop19, Thm. 61], we may replace a dependency pair problem (P_4, R_0, minimal, f) by ({}, R_0, minimal, f). By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed. As all dependency pair problems were succesfully simplified with sound (and complete) processors until nothing remained, we conclude termination. +++ Citations +++ [FuhKop19] C. Fuhs, and C. Kop. A static higher-order dependency pair framework. In Proceedings of ESOP 2019, 2019. [Kop12] C. Kop. Higher Order Termination. PhD Thesis, 2012. [Kop13:2] C. Kop. StarHorpo with an Eta-Rule. Unpublished manuscript, http://cl-informatik.uibk.ac.at/users/kop/etahorpo.pdf, 2013.