We consider the system h48. Alphabet: 0 : [] --> nat add : [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(/\x./\y.yap(xap(f, x), y), z, 0) => z rec(/\x./\y.yap(xap(f, x), y), z, s(u)) => yap(xap(f, u), rec(/\v./\w.yap(xap(f, v), w), z, u)) succ x y => s(y) add(x, y) => rec(/\z./\u.yap(xap(succ, z), u), x, y) add(x, 0) => x add(x, s(y)) => s(add(x, 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 add : [nat * nat] --> nat rec : [nat -> nat -> nat * nat * nat] --> nat s : [nat] --> nat succ : [nat] --> nat -> nat yap : [nat -> nat * nat] --> nat Rules: rec(/\x./\y.yap(F(x), y), X, 0) => X rec(/\x./\y.yap(F(x), y), X, s(Y)) => yap(F(Y), rec(/\z./\u.yap(F(z), u), X, Y)) succ(X) Y => s(Y) add(X, Y) => rec(/\x./\y.yap(succ(x), y), X, Y) add(X, 0) => X add(X, s(Y)) => s(add(X, Y)) 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: || Knuth-Bendix order [KBO] with precedence:~PAIR_2 > succ_2 > s_1 || || and weight map: || || s_1=1 || succ_2=0 || ~PAIR_2=0 || || The variable weight is 1With 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#(/\x./\y.yap(F(x), y), X, s(Y)) =#> yap#(F(Y), rec(/\z./\u.yap(F(z), u), X, Y)) 1] rec#(/\x./\y.yap(F(x), y), X, s(Y)) =#> F(Y) 2] rec#(/\x./\y.yap(F(x), y), X, s(Y)) =#> rec#(/\z./\u.yap(F(z), u), X, Y) 3] rec#(/\x./\y.yap(F(x), y), X, s(Y)) =#> yap#(F(z), u) 4] rec#(/\x./\y.yap(F(x), y), X, s(Y)) =#> F(z) 5] add#(X, Y) =#> rec#(/\x./\y.yap(succ(x), y), X, Y) 6] add#(X, Y) =#> yap#(succ(x), y) 7] add#(X, Y) =#> succ#(x) 8] add#(X, s(Y)) =#> add#(X, Y) 9] yap#(F, X) =#> F(X) Rules R_0: rec(/\x./\y.yap(F(x), y), X, 0) => X rec(/\x./\y.yap(F(x), y), X, s(Y)) => yap(F(Y), rec(/\z./\u.yap(F(z), u), X, Y)) succ(X) Y => s(Y) add(X, Y) => rec(/\x./\y.yap(succ(x), y), X, Y) add(X, 0) => X add(X, s(Y)) => s(add(X, 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 : 9 * 1 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9 * 2 : 0, 1, 2, 3, 4 * 3 : * 4 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9 * 5 : 0, 1, 2, 3, 4 * 6 : * 7 : * 8 : 5, 6, 7, 8 * 9 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9 This graph has the following strongly connected components: P_1: rec#(/\x./\y.yap(F(x), y), X, s(Y)) =#> yap#(F(Y), rec(/\z./\u.yap(F(z), u), X, Y)) rec#(/\x./\y.yap(F(x), y), X, s(Y)) =#> F(Y) rec#(/\x./\y.yap(F(x), y), X, s(Y)) =#> rec#(/\z./\u.yap(F(z), u), X, Y) rec#(/\x./\y.yap(F(x), y), X, s(Y)) =#> F(z) add#(X, Y) =#> rec#(/\x./\y.yap(succ(x), y), X, Y) add#(X, s(Y)) =#> add#(X, 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#(/\x./\y.yap(F(x), y), X, s(Y)) >? yap#(F(Y), rec(/\z./\u.yap(F(z), u), X, Y)) rec#(/\x./\y.yap(F(x), y), X, s(Y)) >? F(Y) ~c0 rec#(/\x./\y.yap(F(x), y), X, s(Y)) >? rec#(/\z./\u.yap(F(z), u), X, Y) rec#(/\x./\y.yap(F(x), y), X, s(Y)) >? F(~c2) ~c1 add#(X, Y) >? rec#(/\x./\y.yap(succ(x), y), X, Y) add#(X, s(Y)) >? add#(X, Y) yap#(F, X) >? F(X) rec(/\x./\y.yap(F(x), y), X, 0) >= X rec(/\x./\y.yap(F(x), y), X, s(Y)) >= yap(F(Y), rec(/\z./\u.yap(F(z), u), X, Y)) succ(X) Y >= s(Y) add(X, Y) >= rec(/\x./\y.yap(succ(x), y), X, Y) add(X, 0) >= X add(X, s(Y)) >= s(add(X, Y)) yap(F, X) >= F X add(X, Y) >= add#(X, Y) rec(F, X, Y) >= rec#(F, X, Y) 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}, add, add#, rec, rec#, s, succ, yap, yap#}, and the following precedence: yap# > add = add# > succ > rec = rec# > s > 0 > yap > @_{o -> o} > #argfun-yap## Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: rec#(/\x./\y.yap(F(x), y), X, s(Y)) >= #argfun-yap##(@_{o -> o}(F(Y), rec(/\x./\y.yap(F(x), y), X, Y))) rec#(/\x./\y.yap(F(x), y), X, s(Y)) > @_{o -> o}(F(Y), _|_) rec#(/\x./\y.yap(F(x), y), X, s(Y)) >= rec#(/\x./\y.yap(F(x), y), X, Y) rec#(/\x./\y.yap(F(x), y), X, s(Y)) >= @_{o -> o}(F(_|_), _|_) add#(X, Y) > rec#(/\x./\y.yap(succ(x), y), X, Y) add#(X, s(Y)) >= add#(X, Y) #argfun-yap##(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) rec(/\x./\y.yap(F(x), y), X, 0) >= X rec(/\x./\y.yap(F(x), y), X, s(Y)) >= yap(F(Y), rec(/\x./\y.yap(F(x), y), X, Y)) @_{o -> o}(succ(X), Y) >= s(Y) add(X, Y) >= rec(/\x./\y.yap(succ(x), y), X, Y) add(X, 0) >= X add(X, s(Y)) >= s(add(X, Y)) yap(F, X) >= @_{o -> o}(F, X) add(X, Y) >= add#(X, Y) rec(F, X, Y) >= rec#(F, X, Y) yap(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) With these choices, we have: 1] rec#(/\x./\y.yap(F(x), y), X, s(Y)) >= #argfun-yap##(@_{o -> o}(F(Y), rec(/\x./\y.yap(F(x), y), X, Y))) because [2], by (Star) 2] rec#*(/\x./\y.yap(F(x), y), X, s(Y)) >= #argfun-yap##(@_{o -> o}(F(Y), rec(/\x./\y.yap(F(x), y), X, Y))) because [3], by (Select) 3] yap(F(rec#*(/\x./\y.yap(F(x), y), X, s(Y))), rec#*(/\z./\u.yap(F(z), u), X, s(Y))) >= #argfun-yap##(@_{o -> o}(F(Y), rec(/\x./\y.yap(F(x), y), X, Y))) because [4], by (Star) 4] yap*(F(rec#*(/\x./\y.yap(F(x), y), X, s(Y))), rec#*(/\z./\u.yap(F(z), u), X, s(Y))) >= #argfun-yap##(@_{o -> o}(F(Y), rec(/\x./\y.yap(F(x), y), X, Y))) because yap > #argfun-yap## and [5], by (Copy) 5] yap*(F(rec#*(/\x./\y.yap(F(x), y), X, s(Y))), rec#*(/\z./\u.yap(F(z), u), X, s(Y))) >= @_{o -> o}(F(Y), rec(/\x./\y.yap(F(x), y), X, Y)) because yap > @_{o -> o}, [6] and [12], by (Copy) 6] yap*(F(rec#*(/\x./\y.yap(F(x), y), X, s(Y))), rec#*(/\z./\u.yap(F(z), u), X, s(Y))) >= F(Y) because [7], by (Select) 7] F(rec#*(/\x./\y.yap(F(x), y), X, s(Y))) >= F(Y) because [8], by (Meta) 8] rec#*(/\x./\y.yap(F(x), y), X, s(Y)) >= Y because [9], by (Select) 9] s(Y) >= Y because [10], by (Star) 10] s*(Y) >= Y because [11], by (Select) 11] Y >= Y by (Meta) 12] yap*(F(rec#*(/\x./\y.yap(F(x), y), X, s(Y))), rec#*(/\z./\u.yap(F(z), u), X, s(Y))) >= rec(/\x./\y.yap(F(x), y), X, Y) because [13], by (Select) 13] rec#*(/\x./\y.yap(F(x), y), X, s(Y)) >= rec(/\x./\y.yap(F(x), y), X, Y) because rec# = rec, rec# in Mul, [14], [20] and [21], by (Stat) 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] X >= X by (Meta) 21] s(Y) > Y because [22], by definition 22] s*(Y) >= Y because [11], by (Select) 23] rec#(/\x./\y.yap(F(x), y), X, s(Y)) > @_{o -> o}(F(Y), _|_) because [24], by definition 24] rec#*(/\x./\y.yap(F(x), y), X, s(Y)) >= @_{o -> o}(F(Y), _|_) because [25], by (Select) 25] yap(F(rec#*(/\x./\y.yap(F(x), y), X, s(Y))), rec#*(/\z./\u.yap(F(z), u), X, s(Y))) >= @_{o -> o}(F(Y), _|_) because [26], by (Star) 26] yap*(F(rec#*(/\x./\y.yap(F(x), y), X, s(Y))), rec#*(/\z./\u.yap(F(z), u), X, s(Y))) >= @_{o -> o}(F(Y), _|_) because yap > @_{o -> o}, [6] and [27], by (Copy) 27] yap*(F(rec#*(/\x./\y.yap(F(x), y), X, s(Y))), rec#*(/\z./\u.yap(F(z), u), X, s(Y))) >= _|_ by (Bot) 28] rec#(/\x./\y.yap(F(x), y), X, s(Y)) >= rec#(/\x./\y.yap(F(x), y), X, Y) because [29], by (Star) 29] rec#*(/\x./\y.yap(F(x), y), X, s(Y)) >= rec#(/\x./\y.yap(F(x), y), X, Y) because rec# in Mul, [14], [20] and [21], by (Stat) 30] rec#(/\x./\y.yap(F(x), y), X, s(Y)) >= @_{o -> o}(F(_|_), _|_) because [31], by (Star) 31] rec#*(/\x./\y.yap(F(x), y), X, s(Y)) >= @_{o -> o}(F(_|_), _|_) because [32], by (Select) 32] yap(F(rec#*(/\x./\y.yap(F(x), y), X, s(Y))), rec#*(/\z./\u.yap(F(z), u), X, s(Y))) >= @_{o -> o}(F(_|_), _|_) because [33], by (Star) 33] yap*(F(rec#*(/\x./\y.yap(F(x), y), X, s(Y))), rec#*(/\z./\u.yap(F(z), u), X, s(Y))) >= @_{o -> o}(F(_|_), _|_) because yap > @_{o -> o}, [34] and [37], by (Copy) 34] yap*(F(rec#*(/\x./\y.yap(F(x), y), X, s(Y))), rec#*(/\z./\u.yap(F(z), u), X, s(Y))) >= F(_|_) because [35], by (Select) 35] F(rec#*(/\x./\y.yap(F(x), y), X, s(Y))) >= F(_|_) because [36], by (Meta) 36] rec#*(/\x./\y.yap(F(x), y), X, s(Y)) >= _|_ by (Bot) 37] yap*(F(rec#*(/\x./\y.yap(F(x), y), X, s(Y))), rec#*(/\z./\u.yap(F(z), u), X, s(Y))) >= _|_ by (Bot) 38] add#(X, Y) > rec#(/\x./\y.yap(succ(x), y), X, Y) because [39], by definition 39] add#*(X, Y) >= rec#(/\x./\y.yap(succ(x), y), X, Y) because add# > rec#, [40], [48] and [50], by (Copy) 40] add#*(X, Y) >= /\y./\z.yap(succ(y), z) because [41], by (F-Abs) 41] add#*(X, Y, x) >= /\z.yap(succ(x), z) because [42], by (F-Abs) 42] add#*(X, Y, x, y) >= yap(succ(x), y) because add# > yap, [43] and [46], by (Copy) 43] add#*(X, Y, x, y) >= succ(x) because add# > succ and [44], by (Copy) 44] add#*(X, Y, x, y) >= x because [45], by (Select) 45] x >= x by (Var) 46] add#*(X, Y, x, y) >= y because [47], by (Select) 47] y >= y by (Var) 48] add#*(X, Y) >= X because [49], by (Select) 49] X >= X by (Meta) 50] add#*(X, Y) >= Y because [51], by (Select) 51] Y >= Y by (Meta) 52] add#(X, s(Y)) >= add#(X, Y) because add# in Mul, [53] and [54], by (Fun) 53] X >= X by (Meta) 54] s(Y) >= Y because [55], by (Star) 55] s*(Y) >= Y because [56], by (Select) 56] Y >= Y by (Meta) 57] #argfun-yap##(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) because [58], by (Star) 58] #argfun-yap##*(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) because [59], by (Select) 59] @_{o -> o}(F, X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [60] and [61], by (Fun) 60] F >= F by (Meta) 61] X >= X by (Meta) 62] rec(/\x./\y.yap(F(x), y), X, 0) >= X because [63], by (Star) 63] rec*(/\x./\y.yap(F(x), y), X, 0) >= X because [64], by (Select) 64] X >= X by (Meta) 65] rec(/\x./\y.yap(F(x), y), X, s(Y)) >= yap(F(Y), rec(/\x./\y.yap(F(x), y), X, Y)) because [66], by (Star) 66] rec*(/\x./\y.yap(F(x), y), X, s(Y)) >= yap(F(Y), rec(/\x./\y.yap(F(x), y), X, Y)) because rec > yap, [67] and [71], by (Copy) 67] rec*(/\x./\y.yap(F(x), y), X, s(Y)) >= F(Y) because [68], by (Select) 68] /\x.yap(F(rec*(/\y./\z.yap(F(y), z), X, s(Y))), x) >= F(Y) because [69], by (Eta)[Kop13:2] 69] F(rec*(/\x./\y.yap(F(x), y), X, s(Y))) >= F(Y) because [70], by (Meta) 70] rec*(/\x./\y.yap(F(x), y), X, s(Y)) >= Y because [9], by (Select) 71] rec*(/\x./\y.yap(F(x), y), X, s(Y)) >= rec(/\x./\y.yap(F(x), y), X, Y) because rec in Mul, [14], [20] and [21], by (Stat) 72] @_{o -> o}(succ(X), Y) >= s(Y) because [73], by (Star) 73] @_{o -> o}*(succ(X), Y) >= s(Y) because [74], by (Select) 74] succ(X) @_{o -> o}*(succ(X), Y) >= s(Y) because [75] 75] succ*(X, @_{o -> o}*(succ(X), Y)) >= s(Y) because succ > s and [76], by (Copy) 76] succ*(X, @_{o -> o}*(succ(X), Y)) >= Y because [77], by (Select) 77] @_{o -> o}*(succ(X), Y) >= Y because [78], by (Select) 78] Y >= Y by (Meta) 79] add(X, Y) >= rec(/\x./\y.yap(succ(x), y), X, Y) because [80], by (Star) 80] add*(X, Y) >= rec(/\x./\y.yap(succ(x), y), X, Y) because add > rec, [81], [89] and [90], by (Copy) 81] add*(X, Y) >= /\y./\z.yap(succ(y), z) because [82], by (F-Abs) 82] add*(X, Y, x) >= /\z.yap(succ(x), z) because [83], by (F-Abs) 83] add*(X, Y, x, y) >= yap(succ(x), y) because add > yap, [84] and [87], by (Copy) 84] add*(X, Y, x, y) >= succ(x) because add > succ and [85], by (Copy) 85] add*(X, Y, x, y) >= x because [86], by (Select) 86] x >= x by (Var) 87] add*(X, Y, x, y) >= y because [88], by (Select) 88] y >= y by (Var) 89] add*(X, Y) >= X because [49], by (Select) 90] add*(X, Y) >= Y because [51], by (Select) 91] add(X, 0) >= X because [92], by (Star) 92] add*(X, 0) >= X because [93], by (Select) 93] X >= X by (Meta) 94] add(X, s(Y)) >= s(add(X, Y)) because [95], by (Star) 95] add*(X, s(Y)) >= s(add(X, Y)) because add > s and [96], by (Copy) 96] add*(X, s(Y)) >= add(X, Y) because add in Mul, [53] and [97], by (Stat) 97] s(Y) > Y because [98], by definition 98] s*(Y) >= Y because [56], by (Select) 99] yap(F, X) >= @_{o -> o}(F, X) because [100], by (Star) 100] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [101] and [102], by (Copy) 101] yap*(F, X) >= F because [60], by (Select) 102] yap*(F, X) >= X because [61], by (Select) 103] add(X, Y) >= add#(X, Y) because add = add#, add in Mul, [104] and [105], by (Fun) 104] X >= X by (Meta) 105] Y >= Y by (Meta) 106] rec(F, X, Y) >= rec#(F, X, Y) because rec = rec#, rec in Mul, [107], [108] and [109], by (Fun) 107] F >= F by (Meta) 108] X >= X by (Meta) 109] Y >= Y by (Meta) 110] yap(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) because [111], by (Star) 111] yap*(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) because yap > #argfun-yap## and [112], by (Copy) 112] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [113] and [115], by (Copy) 113] yap*(F, X) >= F because [114], by (Select) 114] F >= F by (Meta) 115] yap*(F, X) >= X because [116], by (Select) 116] 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#(/\x./\y.yap(F(x), y), X, s(Y)) =#> yap#(F(Y), rec(/\z./\u.yap(F(z), u), X, Y)) rec#(/\x./\y.yap(F(x), y), X, s(Y)) =#> rec#(/\z./\u.yap(F(z), u), X, Y) rec#(/\x./\y.yap(F(x), y), X, s(Y)) =#> F(z) add#(X, s(Y)) =#> add#(X, Y) 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 : 4 * 1 : 0, 1, 2 * 2 : 0, 1, 2, 3, 4 * 3 : 3 * 4 : 0, 1, 2, 3, 4 This graph has the following strongly connected components: P_3: rec#(/\x./\y.yap(F(x), y), X, s(Y)) =#> yap#(F(Y), rec(/\z./\u.yap(F(z), u), X, Y)) rec#(/\x./\y.yap(F(x), y), X, s(Y)) =#> rec#(/\z./\u.yap(F(z), u), X, Y) rec#(/\x./\y.yap(F(x), y), X, s(Y)) =#> F(z) yap#(F, X) =#> F(X) P_4: add#(X, s(Y)) =#> add#(X, Y) 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 apply the subterm criterion with the following projection function: nu(add#) = 2 Thus, we can orient the dependency pairs as follows: nu(add#(X, s(Y))) = s(Y) |> Y = nu(add#(X, Y)) 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. 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 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#(/\x./\y.yap(F(x), y), X, s(Y)) >? yap#(F(Y), rec(/\z./\u.yap(F(z), u), X, Y)) rec#(/\x./\y.yap(F(x), y), X, s(Y)) >? rec#(/\z./\u.yap(F(z), u), X, Y) rec#(/\x./\y.yap(F(x), y), X, s(Y)) >? F(~c1) ~c0 yap#(F, X) >? F(X) rec(/\x./\y.yap(F(x), y), X, 0) >= X rec(/\x./\y.yap(F(x), y), X, s(Y)) >= yap(F(Y), rec(/\z./\u.yap(F(z), u), X, Y)) succ(X) Y >= s(Y) add(X, Y) >= rec(/\x./\y.yap(succ(x), y), X, Y) add(X, 0) >= X add(X, s(Y)) >= s(add(X, Y)) yap(F, X) >= F X rec(F, X, Y) >= rec#(F, X, Y) 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]] = _|_ We choose Lex = {} and Mul = {#argfun-yap##, 0, @_{o -> o}, add, rec, rec#, s, succ, yap, yap#}, and the following precedence: 0 > add > succ > s > rec = 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: rec#(/\x./\y.yap(F(x), y), X, s(Y)) >= #argfun-yap##(@_{o -> o}(F(Y), rec(/\x./\y.yap(F(x), y), X, Y))) rec#(/\x./\y.yap(F(x), y), X, s(Y)) >= rec#(/\x./\y.yap(F(x), y), X, Y) rec#(/\x./\y.yap(F(x), y), X, s(Y)) >= @_{o -> o}(F(_|_), _|_) #argfun-yap##(@_{o -> o}(F, X)) > @_{o -> o}(F, X) rec(/\x./\y.yap(F(x), y), X, 0) >= X rec(/\x./\y.yap(F(x), y), X, s(Y)) >= yap(F(Y), rec(/\x./\y.yap(F(x), y), X, Y)) @_{o -> o}(succ(X), Y) >= s(Y) add(X, Y) >= rec(/\x./\y.yap(succ(x), y), X, Y) add(X, 0) >= X add(X, s(Y)) >= s(add(X, Y)) yap(F, X) >= @_{o -> o}(F, X) rec(F, X, Y) >= rec#(F, X, Y) yap(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) With these choices, we have: 1] rec#(/\x./\y.yap(F(x), y), X, s(Y)) >= #argfun-yap##(@_{o -> o}(F(Y), rec(/\x./\y.yap(F(x), y), X, Y))) because [2], by (Star) 2] rec#*(/\x./\y.yap(F(x), y), X, s(Y)) >= #argfun-yap##(@_{o -> o}(F(Y), rec(/\x./\y.yap(F(x), y), X, Y))) because [3], by (Select) 3] yap(F(rec#*(/\x./\y.yap(F(x), y), X, s(Y))), rec#*(/\z./\u.yap(F(z), u), X, s(Y))) >= #argfun-yap##(@_{o -> o}(F(Y), rec(/\x./\y.yap(F(x), y), X, Y))) because [4], by (Star) 4] yap*(F(rec#*(/\x./\y.yap(F(x), y), X, s(Y))), rec#*(/\z./\u.yap(F(z), u), X, s(Y))) >= #argfun-yap##(@_{o -> o}(F(Y), rec(/\x./\y.yap(F(x), y), X, Y))) because yap > #argfun-yap## and [5], by (Copy) 5] yap*(F(rec#*(/\x./\y.yap(F(x), y), X, s(Y))), rec#*(/\z./\u.yap(F(z), u), X, s(Y))) >= @_{o -> o}(F(Y), rec(/\x./\y.yap(F(x), y), X, Y)) because yap > @_{o -> o}, [6] and [12], by (Copy) 6] yap*(F(rec#*(/\x./\y.yap(F(x), y), X, s(Y))), rec#*(/\z./\u.yap(F(z), u), X, s(Y))) >= F(Y) because [7], by (Select) 7] F(rec#*(/\x./\y.yap(F(x), y), X, s(Y))) >= F(Y) because [8], by (Meta) 8] rec#*(/\x./\y.yap(F(x), y), X, s(Y)) >= Y because [9], by (Select) 9] s(Y) >= Y because [10], by (Star) 10] s*(Y) >= Y because [11], by (Select) 11] Y >= Y by (Meta) 12] yap*(F(rec#*(/\x./\y.yap(F(x), y), X, s(Y))), rec#*(/\z./\u.yap(F(z), u), X, s(Y))) >= rec(/\x./\y.yap(F(x), y), X, Y) because [13], by (Select) 13] rec#*(/\x./\y.yap(F(x), y), X, s(Y)) >= rec(/\x./\y.yap(F(x), y), X, Y) because rec# = rec, rec# in Mul, [14], [20] and [21], by (Stat) 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] X >= X by (Meta) 21] s(Y) > Y because [22], by definition 22] s*(Y) >= Y because [11], by (Select) 23] rec#(/\x./\y.yap(F(x), y), X, s(Y)) >= rec#(/\x./\y.yap(F(x), y), X, Y) because rec# in Mul, [14], [20] and [24], by (Fun) 24] s(Y) >= Y because [22], by (Star) 25] rec#(/\x./\y.yap(F(x), y), X, s(Y)) >= @_{o -> o}(F(_|_), _|_) because [26], by (Star) 26] rec#*(/\x./\y.yap(F(x), y), X, s(Y)) >= @_{o -> o}(F(_|_), _|_) because rec# > @_{o -> o}, [27] and [31], by (Copy) 27] rec#*(/\x./\y.yap(F(x), y), X, s(Y)) >= F(_|_) because [28], by (Select) 28] /\x.yap(F(rec#*(/\y./\z.yap(F(y), z), X, s(Y))), x) >= F(_|_) because [29], by (Eta)[Kop13:2] 29] F(rec#*(/\x./\y.yap(F(x), y), X, s(Y))) >= F(_|_) because [30], by (Meta) 30] rec#*(/\x./\y.yap(F(x), y), X, s(Y)) >= _|_ by (Bot) 31] rec#*(/\x./\y.yap(F(x), y), X, s(Y)) >= _|_ by (Bot) 32] #argfun-yap##(@_{o -> o}(F, X)) > @_{o -> o}(F, X) because [33], by definition 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./\y.yap(F(x), y), X, 0) >= X because [38], by (Star) 38] rec*(/\x./\y.yap(F(x), y), X, 0) >= X because [39], by (Select) 39] X >= X by (Meta) 40] rec(/\x./\y.yap(F(x), y), X, s(Y)) >= yap(F(Y), rec(/\x./\y.yap(F(x), y), X, Y)) because [41], by (Star) 41] rec*(/\x./\y.yap(F(x), y), X, s(Y)) >= yap(F(Y), rec(/\x./\y.yap(F(x), y), X, Y)) because [42], by (Select) 42] yap(F(rec*(/\x./\y.yap(F(x), y), X, s(Y))), rec*(/\z./\u.yap(F(z), u), X, s(Y))) >= yap(F(Y), rec(/\x./\y.yap(F(x), y), X, Y)) because yap in Mul, [43] and [45], by (Fun) 43] F(rec*(/\x./\y.yap(F(x), y), X, s(Y))) >= F(Y) because [44], by (Meta) 44] rec*(/\x./\y.yap(F(x), y), X, s(Y)) >= Y because [24], by (Select) 45] rec*(/\x./\y.yap(F(x), y), X, s(Y)) >= rec(/\x./\y.yap(F(x), y), X, Y) because rec in Mul, [14], [20] and [21], by (Stat) 46] @_{o -> o}(succ(X), Y) >= s(Y) because [47], by (Star) 47] @_{o -> o}*(succ(X), Y) >= s(Y) because [48], by (Select) 48] succ(X) @_{o -> o}*(succ(X), Y) >= s(Y) because [49] 49] succ*(X, @_{o -> o}*(succ(X), Y)) >= s(Y) because succ > s and [50], by (Copy) 50] succ*(X, @_{o -> o}*(succ(X), Y)) >= Y because [51], by (Select) 51] @_{o -> o}*(succ(X), Y) >= Y because [52], by (Select) 52] Y >= Y by (Meta) 53] add(X, Y) >= rec(/\x./\y.yap(succ(x), y), X, Y) because [54], by (Star) 54] add*(X, Y) >= rec(/\x./\y.yap(succ(x), y), X, Y) because add > rec, [55], [63] and [65], by (Copy) 55] add*(X, Y) >= /\y./\z.yap(succ(y), z) because [56], by (F-Abs) 56] add*(X, Y, x) >= /\z.yap(succ(x), z) because [57], by (F-Abs) 57] add*(X, Y, x, y) >= yap(succ(x), y) because add > yap, [58] and [61], by (Copy) 58] add*(X, Y, x, y) >= succ(x) because add > succ and [59], by (Copy) 59] add*(X, Y, x, y) >= x because [60], by (Select) 60] x >= x by (Var) 61] add*(X, Y, x, y) >= y because [62], by (Select) 62] y >= y by (Var) 63] add*(X, Y) >= X because [64], by (Select) 64] X >= X by (Meta) 65] add*(X, Y) >= Y because [66], by (Select) 66] Y >= Y by (Meta) 67] add(X, 0) >= X because [68], by (Star) 68] add*(X, 0) >= X because [69], by (Select) 69] X >= X by (Meta) 70] add(X, s(Y)) >= s(add(X, Y)) because [71], by (Star) 71] add*(X, s(Y)) >= s(add(X, Y)) because add > s and [72], by (Copy) 72] add*(X, s(Y)) >= add(X, Y) because add in Mul, [73] and [74], by (Stat) 73] X >= X by (Meta) 74] s(Y) > Y because [75], by definition 75] s*(Y) >= Y because [76], by (Select) 76] Y >= Y by (Meta) 77] yap(F, X) >= @_{o -> o}(F, X) because [78], by (Star) 78] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [79] and [80], by (Copy) 79] yap*(F, X) >= F because [35], by (Select) 80] yap*(F, X) >= X because [36], by (Select) 81] rec(F, X, Y) >= rec#(F, X, Y) because rec = rec#, rec in Mul, [82], [83] and [84], by (Fun) 82] F >= F by (Meta) 83] X >= X by (Meta) 84] Y >= Y by (Meta) 85] yap(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) because [86], by (Star) 86] yap*(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) because yap > #argfun-yap## and [87], by (Copy) 87] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [88] and [90], by (Copy) 88] yap*(F, X) >= F because [89], by (Select) 89] F >= F by (Meta) 90] yap*(F, X) >= X because [91], by (Select) 91] 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_3, R_0, minimal, all) by (P_5, R_0, minimal, all), where P_5 consists of: rec#(/\x./\y.yap(F(x), y), X, s(Y)) =#> yap#(F(Y), rec(/\z./\u.yap(F(z), u), X, Y)) rec#(/\x./\y.yap(F(x), y), X, s(Y)) =#> rec#(/\z./\u.yap(F(z), u), X, Y) rec#(/\x./\y.yap(F(x), y), X, s(Y)) =#> F(z) Thus, the original system is terminating if (P_5, R_0, minimal, all) is finite. We consider the dependency pair problem (P_5, 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 : * 1 : 0, 1, 2 * 2 : 0, 1, 2 This graph has the following strongly connected components: P_6: rec#(/\x./\y.yap(F(x), y), X, s(Y)) =#> rec#(/\z./\u.yap(F(z), u), X, Y) rec#(/\x./\y.yap(F(x), y), X, s(Y)) =#> F(z) By [Kop12, Thm. 7.31], we may replace any dependency pair problem (P_5, R_0, m, f) by (P_6, R_0, m, f). Thus, the original system is terminating if (P_6, R_0, minimal, all) is finite. We consider the dependency pair problem (P_6, 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#(/\x./\y.yap(F(x), y), X, s(Y)) >? rec#(/\z./\u.yap(F(z), u), X, Y) rec#(/\x./\y.yap(F(x), y), X, s(Y)) >? F(~c1) ~c0 rec(/\x./\y.yap(F(x), y), X, 0) >= X rec(/\x./\y.yap(F(x), y), X, s(Y)) >= yap(F(Y), rec(/\z./\u.yap(F(z), u), X, Y)) succ(X) Y >= s(Y) add(X, Y) >= rec(/\x./\y.yap(succ(x), y), X, Y) add(X, 0) >= X add(X, s(Y)) >= s(add(X, Y)) yap(F, X) >= F X rec(F, X, Y) >= rec#(F, 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]. Argument functions: [[~c0]] = _|_ [[~c1]] = _|_ We choose Lex = {} and Mul = {0, @_{o -> o}, add, rec, rec#, s, succ, yap}, and the following precedence: 0 > add > succ > s > @_{o -> o} = yap > rec > rec# Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: rec#(/\x./\y.yap(F(x), y), X, s(Y)) >= rec#(/\x./\y.yap(F(x), y), X, Y) rec#(/\x./\y.yap(F(x), y), X, s(Y)) > @_{o -> o}(F(_|_), _|_) rec(/\x./\y.yap(F(x), y), X, 0) >= X rec(/\x./\y.yap(F(x), y), X, s(Y)) >= yap(F(Y), rec(/\x./\y.yap(F(x), y), X, Y)) @_{o -> o}(succ(X), Y) >= s(Y) add(X, Y) >= rec(/\x./\y.yap(succ(x), y), X, Y) add(X, 0) >= X add(X, s(Y)) >= s(add(X, Y)) yap(F, X) >= @_{o -> o}(F, X) rec(F, X, Y) >= rec#(F, X, Y) With these choices, we have: 1] rec#(/\x./\y.yap(F(x), y), X, s(Y)) >= rec#(/\x./\y.yap(F(x), y), X, Y) because rec# in Mul, [2], [8] and [9], by (Fun) 2] /\x./\z.yap(F(x), z) >= /\x./\z.yap(F(x), z) because [3], by (Abs) 3] /\z.yap(F(y), z) >= /\z.yap(F(y), z) because [4], by (Abs) 4] yap(F(y), x) >= yap(F(y), x) because yap in Mul, [5] and [7], by (Fun) 5] F(y) >= F(y) because [6], by (Meta) 6] y >= y by (Var) 7] x >= x by (Var) 8] X >= X by (Meta) 9] s(Y) >= Y because [10], by (Star) 10] s*(Y) >= Y because [11], by (Select) 11] Y >= Y by (Meta) 12] rec#(/\x./\y.yap(F(x), y), X, s(Y)) > @_{o -> o}(F(_|_), _|_) because [13], by definition 13] rec#*(/\x./\y.yap(F(x), y), X, s(Y)) >= @_{o -> o}(F(_|_), _|_) because [14], by (Select) 14] yap(F(rec#*(/\x./\y.yap(F(x), y), X, s(Y))), rec#*(/\z./\u.yap(F(z), u), X, s(Y))) >= @_{o -> o}(F(_|_), _|_) because yap = @_{o -> o}, yap in Mul, [15] and [17], by (Fun) 15] F(rec#*(/\x./\y.yap(F(x), y), X, s(Y))) >= F(_|_) because [16], by (Meta) 16] rec#*(/\x./\y.yap(F(x), y), X, s(Y)) >= _|_ by (Bot) 17] rec#*(/\x./\y.yap(F(x), y), X, s(Y)) >= _|_ by (Bot) 18] rec(/\x./\y.yap(F(x), y), X, 0) >= X because [19], by (Star) 19] rec*(/\x./\y.yap(F(x), y), X, 0) >= X because [20], by (Select) 20] X >= X by (Meta) 21] rec(/\x./\y.yap(F(x), y), X, s(Y)) >= yap(F(Y), rec(/\x./\y.yap(F(x), y), X, Y)) because [22], by (Star) 22] rec*(/\x./\y.yap(F(x), y), X, s(Y)) >= yap(F(Y), rec(/\x./\y.yap(F(x), y), X, Y)) because [23], by (Select) 23] yap(F(rec*(/\x./\y.yap(F(x), y), X, s(Y))), rec*(/\z./\u.yap(F(z), u), X, s(Y))) >= yap(F(Y), rec(/\x./\y.yap(F(x), y), X, Y)) because yap in Mul, [24] and [26], by (Fun) 24] F(rec*(/\x./\y.yap(F(x), y), X, s(Y))) >= F(Y) because [25], by (Meta) 25] rec*(/\x./\y.yap(F(x), y), X, s(Y)) >= Y because [9], by (Select) 26] rec*(/\x./\y.yap(F(x), y), X, s(Y)) >= rec(/\x./\y.yap(F(x), y), X, Y) because rec in Mul, [2], [8] and [27], by (Stat) 27] s(Y) > Y because [28], by definition 28] s*(Y) >= Y because [11], by (Select) 29] @_{o -> o}(succ(X), Y) >= s(Y) because [30], by (Star) 30] @_{o -> o}*(succ(X), Y) >= s(Y) because [31], by (Select) 31] succ(X) @_{o -> o}*(succ(X), Y) >= s(Y) because [32] 32] succ*(X, @_{o -> o}*(succ(X), Y)) >= s(Y) because succ > s and [33], by (Copy) 33] succ*(X, @_{o -> o}*(succ(X), Y)) >= Y because [34], by (Select) 34] @_{o -> o}*(succ(X), Y) >= Y because [35], by (Select) 35] Y >= Y by (Meta) 36] add(X, Y) >= rec(/\x./\y.yap(succ(x), y), X, Y) because [37], by (Star) 37] add*(X, Y) >= rec(/\x./\y.yap(succ(x), y), X, Y) because add > rec, [38], [46] and [48], by (Copy) 38] add*(X, Y) >= /\y./\z.yap(succ(y), z) because [39], by (F-Abs) 39] add*(X, Y, x) >= /\z.yap(succ(x), z) because [40], by (F-Abs) 40] add*(X, Y, x, y) >= yap(succ(x), y) because add > yap, [41] and [44], by (Copy) 41] add*(X, Y, x, y) >= succ(x) because add > succ and [42], by (Copy) 42] add*(X, Y, x, y) >= x because [43], by (Select) 43] x >= x by (Var) 44] add*(X, Y, x, y) >= y because [45], by (Select) 45] y >= y by (Var) 46] add*(X, Y) >= X because [47], by (Select) 47] X >= X by (Meta) 48] add*(X, Y) >= Y because [49], by (Select) 49] Y >= Y by (Meta) 50] add(X, 0) >= X because [51], by (Star) 51] add*(X, 0) >= X because [52], by (Select) 52] X >= X by (Meta) 53] add(X, s(Y)) >= s(add(X, Y)) because [54], by (Star) 54] add*(X, s(Y)) >= s(add(X, Y)) because add > s and [55], by (Copy) 55] add*(X, s(Y)) >= add(X, Y) because add in Mul, [56] and [57], by (Stat) 56] X >= X by (Meta) 57] s(Y) > Y because [58], by definition 58] s*(Y) >= Y because [59], by (Select) 59] Y >= Y by (Meta) 60] yap(F, X) >= @_{o -> o}(F, X) because yap = @_{o -> o}, yap in Mul, [61] and [62], by (Fun) 61] F >= F by (Meta) 62] X >= X by (Meta) 63] rec(F, X, Y) >= rec#(F, X, Y) because [64], by (Star) 64] rec*(F, X, Y) >= rec#(F, X, Y) because rec > rec#, [65], [67] and [69], by (Copy) 65] rec*(F, X, Y) >= F because [66], by (Select) 66] F >= F by (Meta) 67] rec*(F, X, Y) >= X because [68], by (Select) 68] X >= X by (Meta) 69] rec*(F, X, Y) >= Y because [70], by (Select) 70] Y >= Y by (Meta) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_6, R_0, minimal, all) by (P_7, R_0, minimal, all), where P_7 consists of: rec#(/\x./\y.yap(F(x), y), X, s(Y)) =#> rec#(/\z./\u.yap(F(z), u), X, Y) Thus, the original system is terminating if (P_7, R_0, minimal, all) is finite. We consider the dependency pair problem (P_7, R_0, minimal, all). We apply the subterm criterion with the following projection function: nu(rec#) = 3 Thus, we can orient the dependency pairs as follows: nu(rec#(/\x./\y.yap(F(x), y), X, s(Y))) = s(Y) |> Y = nu(rec#(/\z./\u.yap(F(z), u), X, Y)) By [FuhKop19, Thm. 61], we may replace a dependency pair problem (P_7, 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.