We consider the system h50. Alphabet: 0 : [] --> nat plus : [nat * nat] --> nat rec : [nat * nat * nat -> nat -> nat] --> nat s : [nat] --> nat succ : [] --> 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))) succ x y => s(y) plus(x, y) => rec(x, y, succ) 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 plus : [nat * nat] --> nat rec : [nat * nat * nat -> nat -> nat] --> nat s : [nat] --> nat succ : [] --> 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))) succ X Y => s(Y) plus(X, Y) => rec(X, Y, succ) yap(F, X) => F X We observe that the rules contain a first-order subset: succ 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: || || succ(%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(succ(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: || || succ(%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, succ) 6] plus#(X, Y) =#> succ# 7] 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))) succ X Y => s(Y) plus(X, Y) => rec(X, Y, succ) 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 : 7 * 1 : 0, 1, 2, 3, 4, 5, 6, 7 * 2 : 0, 1, 2, 3, 4 * 3 : * 4 : 0, 1, 2, 3, 4, 5, 6, 7 * 5 : * 6 : * 7 : 0, 1, 2, 3, 4, 5, 6, 7 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) 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 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))) succ X Y >= s(Y) plus(X, Y) >= rec(X, Y, succ) 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: [[~c0]] = _|_ [[~c1]] = _|_ [[~c2]] = _|_ We choose Lex = {} and Mul = {#argfun-yap##, 0, @_{o -> o -> o}, @_{o -> o}, plus, rec, rec#, s, succ, yap, yap#}, and the following precedence: @_{o -> o -> o} > yap# > yap > plus = succ > rec = rec# > #argfun-yap## > @_{o -> o} > s > 0 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)) > @_{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-yap##(@_{o -> o}(F, X)) >= @_{o -> o}(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, /\x./\y.yap(F(x), y))) @_{o -> o}(@_{o -> o -> o}(succ, X), Y) >= s(Y) plus(X, Y) >= rec(X, Y, succ) 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 rec# > #argfun-yap## and [3], by (Copy) 3] 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}, [4] and [11], by (Copy) 4] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= F(X) because [5], by (Select) 5] /\x.yap(F(rec#*(s(X), Y, /\y./\z.yap(F(y), z))), x) >= F(X) because [6], by (Eta)[Kop13:2] 6] F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(X) because [7], by (Meta) 7] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= X because [8], by (Select) 8] s(X) >= X because [9], by (Star) 9] s*(X) >= X because [10], by (Select) 10] X >= X by (Meta) 11] 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, [12], [14] and [15], by (Stat) 12] s(X) > X because [13], by definition 13] s*(X) >= X because [10], by (Select) 14] Y >= Y by (Meta) 15] /\x./\z.yap(F(x), z) >= /\x./\z.yap(F(x), z) because [16], by (Abs) 16] /\z.yap(F(y), z) >= /\z.yap(F(y), z) because [17], by (Abs) 17] yap(F(y), x) >= yap(F(y), x) because yap in Mul, [18] and [20], by (Fun) 18] F(y) >= F(y) because [19], by (Meta) 19] y >= y by (Var) 20] x >= x by (Var) 21] rec#(s(X), Y, /\x./\y.yap(F(x), y)) > @_{o -> o}(F(X), _|_) because [22], by definition 22] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= @_{o -> o}(F(X), _|_) because rec# > @_{o -> o}, [4] and [23], by (Copy) 23] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= _|_ by (Bot) 24] rec#(s(X), Y, /\x./\y.yap(F(x), y)) >= rec#(X, Y, /\x./\y.yap(F(x), y)) because rec# in Mul, [25], [14] and [15], by (Fun) 25] s(X) >= X because [13], by (Star) 26] rec#(s(X), Y, /\x./\y.yap(F(x), y)) > @_{o -> o}(F(_|_), _|_) because [27], by definition 27] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= @_{o -> o}(F(_|_), _|_) because [28], by (Select) 28] 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 [29], by (Star) 29] 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}, [30] and [33], by (Copy) 30] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= F(_|_) because [31], by (Select) 31] F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(_|_) because [32], by (Meta) 32] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= _|_ by (Bot) 33] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= _|_ by (Bot) 34] #argfun-yap##(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) because [35], by (Star) 35] #argfun-yap##*(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) because [36], by (Select) 36] @_{o -> o}(F, X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [37] and [38], by (Fun) 37] F >= F by (Meta) 38] X >= X by (Meta) 39] rec(0, X, /\x./\y.yap(F(x), y)) >= X because [40], by (Star) 40] rec*(0, X, /\x./\y.yap(F(x), y)) >= X because [41], by (Select) 41] X >= X by (Meta) 42] rec(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) because [43], by (Star) 43] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) because [44], by (Select) 44] 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, [45] and [47], by (Fun) 45] F(rec*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(X) because [46], by (Meta) 46] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= X because [25], by (Select) 47] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= rec(X, Y, /\x./\y.yap(F(x), y)) because rec in Mul, [12], [14] and [15], by (Stat) 48] @_{o -> o}(@_{o -> o -> o}(succ, X), Y) >= s(Y) because [49], by (Star) 49] @_{o -> o}*(@_{o -> o -> o}(succ, X), Y) >= s(Y) because [50], by (Select) 50] @_{o -> o -> o}(succ, X) @_{o -> o}*(@_{o -> o -> o}(succ, X), Y) >= s(Y) because [51] 51] @_{o -> o -> o}*(succ, X, @_{o -> o}*(@_{o -> o -> o}(succ, X), Y)) >= s(Y) because [52], by (Select) 52] succ @_{o -> o -> o}*(succ, X, @_{o -> o}*(@_{o -> o -> o}(succ, X), Y)) @_{o -> o -> o}*(succ, X, @_{o -> o}*(@_{o -> o -> o}(succ, X), Y)) >= s(Y) because [53] 53] succ*(@_{o -> o -> o}*(succ, X, @_{o -> o}*(@_{o -> o -> o}(succ, X), Y)), @_{o -> o -> o}*(succ, X, @_{o -> o}*(@_{o -> o -> o}(succ, X), Y))) >= s(Y) because succ > s and [54], by (Copy) 54] succ*(@_{o -> o -> o}*(succ, X, @_{o -> o}*(@_{o -> o -> o}(succ, X), Y)), @_{o -> o -> o}*(succ, X, @_{o -> o}*(@_{o -> o -> o}(succ, X), Y))) >= Y because [55], by (Select) 55] @_{o -> o -> o}*(succ, X, @_{o -> o}*(@_{o -> o -> o}(succ, X), Y)) >= Y because [56], by (Select) 56] @_{o -> o}*(@_{o -> o -> o}(succ, X), Y) >= Y because [57], by (Select) 57] Y >= Y by (Meta) 58] plus(X, Y) >= rec(X, Y, succ) because [59], by (Star) 59] plus*(X, Y) >= rec(X, Y, succ) because plus > rec, [60], [62] and [64], by (Copy) 60] plus*(X, Y) >= X because [61], by (Select) 61] X >= X by (Meta) 62] plus*(X, Y) >= Y because [63], by (Select) 63] Y >= Y by (Meta) 64] plus*(X, Y) >= succ because plus = succ and plus in Mul, by (Stat) 65] yap(F, X) >= @_{o -> o}(F, X) because [66], by (Star) 66] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [67] and [68], by (Copy) 67] yap*(F, X) >= F because [37], by (Select) 68] yap*(F, X) >= X because [38], by (Select) 69] rec(X, Y, F) >= rec#(X, Y, F) because rec = rec#, rec in Mul, [70], [71] and [72], by (Fun) 70] X >= X by (Meta) 71] Y >= Y by (Meta) 72] F >= F by (Meta) 73] yap(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) because [74], by (Star) 74] yap*(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) because yap > #argfun-yap## and [75], by (Copy) 75] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [76] and [78], by (Copy) 76] yap*(F, X) >= F because [77], by (Select) 77] F >= F by (Meta) 78] yap*(F, X) >= X because [79], by (Select) 79] 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)) =#> rec#(X, Y, /\z./\u.yap(F(z), u)) 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 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_3: rec#(s(X), Y, /\x./\y.yap(F(x), y)) =#> rec#(X, Y, /\z./\u.yap(F(z), u)) P_4: yap#(F, X) =#> F(X) By [Kop12, Thm. 7.31], we may replace any dependency pair problem (P_2, R_0, m, f) by (P_3, R_0, m, f) and (P_4, R_0, m, f). Thus, the original system is terminating if each of (P_3, R_0, minimal, all) and (P_4, R_0, minimal, all) is finite. We consider the dependency pair problem (P_4, 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))) succ X Y >= s(Y) plus(X, Y) >= rec(X, Y, succ) 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: [[succ]] = _|_ We choose Lex = {} and Mul = {#argfun-yap##, 0, @_{o -> o -> o}, @_{o -> o}, plus, rec, s, yap, yap#}, and the following precedence: 0 > @_{o -> o -> o} > s > plus > rec > yap > #argfun-yap## > @_{o -> o} > 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(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, /\x./\y.yap(F(x), y))) @_{o -> o}(@_{o -> o -> o}(_|_, X), Y) >= s(Y) plus(X, Y) >= rec(X, 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(0, X, /\x./\y.yap(F(x), y)) >= X because [7], by (Star) 7] rec*(0, 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}(_|_, X), Y) >= s(Y) because [29], by (Star) 29] @_{o -> o}*(@_{o -> o -> o}(_|_, X), Y) >= s(Y) because [30], by (Select) 30] @_{o -> o -> o}(_|_, X) @_{o -> o}*(@_{o -> o -> o}(_|_, X), Y) >= s(Y) because [31] 31] @_{o -> o -> o}*(_|_, X, @_{o -> o}*(@_{o -> o -> o}(_|_, X), Y)) >= s(Y) because @_{o -> o -> o} > s and [32], by (Copy) 32] @_{o -> o -> o}*(_|_, X, @_{o -> o}*(@_{o -> o -> o}(_|_, X), Y)) >= Y because [33], by (Select) 33] @_{o -> o}*(@_{o -> o -> o}(_|_, X), Y) >= Y because [34], by (Select) 34] Y >= Y by (Meta) 35] plus(X, Y) >= rec(X, Y, _|_) because [36], by (Star) 36] plus*(X, Y) >= rec(X, Y, _|_) because plus > rec, [37], [39] and [41], by (Copy) 37] plus*(X, Y) >= X because [38], by (Select) 38] X >= X by (Meta) 39] plus*(X, Y) >= Y because [40], by (Select) 40] Y >= Y by (Meta) 41] plus*(X, Y) >= _|_ by (Bot) 42] yap(F, X) >= @_{o -> o}(F, X) because [43], by (Star) 43] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [44] and [45], by (Copy) 44] yap*(F, X) >= F because [4], by (Select) 45] yap*(F, X) >= X because [5], by (Select) 46] yap(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) because [47], by (Star) 47] yap*(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) because yap > #argfun-yap## and [48], by (Copy) 48] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [49] and [51], by (Copy) 49] yap*(F, X) >= F because [50], by (Select) 50] F >= F by (Meta) 51] yap*(F, X) >= X because [52], by (Select) 52] 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_4, 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_3, R_0, minimal, all) is finite. We consider the dependency pair problem (P_3, 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_3, 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.