We consider the system h58. Alphabet: 0 : [] --> nat cons : [nat * list] --> list foldr : [nat -> nat -> nat * nat * list] --> nat length : [list] --> nat nil : [] --> list s : [nat] --> nat succ : [] --> nat -> nat -> nat xap : [nat -> nat -> nat * nat] --> nat -> nat yap : [nat -> nat * nat] --> nat Rules: foldr(/\x./\y.yap(xap(f, x), y), z, nil) => z foldr(/\x./\y.yap(xap(f, x), y), z, cons(u, v)) => yap(xap(f, u), foldr(/\w./\x'.yap(xap(f, w), x'), z, v)) succ x y => s(y) length(x) => foldr(/\y./\z.yap(xap(succ, y), z), 0, x) 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 cons : [nat * list] --> list foldr : [nat -> nat -> nat * nat * list] --> nat length : [list] --> nat nil : [] --> list s : [nat] --> nat succ : [nat] --> nat -> nat yap : [nat -> nat * nat] --> nat Rules: foldr(/\x./\y.yap(F(x), y), X, nil) => X foldr(/\x./\y.yap(F(x), y), X, cons(Y, Z)) => yap(F(Y), foldr(/\z./\u.yap(F(z), u), X, Z)) succ(X) Y => s(Y) length(X) => foldr(/\x./\y.yap(succ(x), y), 0, X) 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] foldr#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) =#> yap#(F(Y), foldr(/\z./\u.yap(F(z), u), X, Z)) 1] foldr#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) =#> F(Y) 2] foldr#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) =#> foldr#(/\z./\u.yap(F(z), u), X, Z) 3] foldr#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) =#> yap#(F(z), u) 4] foldr#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) =#> F(z) 5] length#(X) =#> foldr#(/\x./\y.yap(succ(x), y), 0, X) 6] length#(X) =#> yap#(succ(x), y) 7] length#(X) =#> succ#(x) 8] yap#(F, X) =#> F(X) Rules R_0: foldr(/\x./\y.yap(F(x), y), X, nil) => X foldr(/\x./\y.yap(F(x), y), X, cons(Y, Z)) => yap(F(Y), foldr(/\z./\u.yap(F(z), u), X, Z)) succ(X) Y => s(Y) length(X) => foldr(/\x./\y.yap(succ(x), y), 0, X) 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 : 8 * 1 : 0, 1, 2, 3, 4, 5, 6, 7, 8 * 2 : 0, 1, 2, 3, 4 * 3 : * 4 : 0, 1, 2, 3, 4, 5, 6, 7, 8 * 5 : 0, 1, 2, 3, 4 * 6 : * 7 : * 8 : 0, 1, 2, 3, 4, 5, 6, 7, 8 This graph has the following strongly connected components: P_1: foldr#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) =#> yap#(F(Y), foldr(/\z./\u.yap(F(z), u), X, Z)) foldr#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) =#> F(Y) foldr#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) =#> foldr#(/\z./\u.yap(F(z), u), X, Z) foldr#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) =#> F(z) length#(X) =#> foldr#(/\x./\y.yap(succ(x), y), 0, X) 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: foldr#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >? yap#(F(Y), foldr(/\z./\u.yap(F(z), u), X, Z)) foldr#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >? F(Y) ~c0 foldr#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >? foldr#(/\z./\u.yap(F(z), u), X, Z) foldr#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >? F(~c2) ~c1 length#(X) >? foldr#(/\x./\y.yap(succ(x), y), 0, X) yap#(F, X) >? F(X) foldr(/\x./\y.yap(F(x), y), X, nil) >= X foldr(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= yap(F(Y), foldr(/\z./\u.yap(F(z), u), X, Z)) succ(X) Y >= s(Y) length(X) >= foldr(/\x./\y.yap(succ(x), y), 0, X) yap(F, X) >= F X foldr(F, X, Y) >= foldr#(F, X, Y) length(X) >= length#(X) yap(F, X) >= yap#(F, X) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( length#(X) ) = #argfun-length##(foldr#(/\x./\y.yap(succ(x), y), 0, X)) 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]] = _|_ [[s(x_1)]] = x_1 [[~c0]] = _|_ [[~c1]] = _|_ [[~c2]] = _|_ We choose Lex = {} and Mul = {#argfun-length##, #argfun-yap##, @_{o -> o}, cons, foldr, foldr#, length, length#, nil, succ, yap, yap#}, and the following precedence: length > length# > nil > yap# > #argfun-length## > foldr = foldr# > succ > yap > cons > @_{o -> o} > #argfun-yap## Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: foldr#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) > #argfun-yap##(@_{o -> o}(F(Y), foldr(/\x./\y.yap(F(x), y), X, Z))) foldr#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) > @_{o -> o}(F(Y), _|_) foldr#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= foldr#(/\x./\y.yap(F(x), y), X, Z) foldr#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) > @_{o -> o}(F(_|_), _|_) #argfun-length##(foldr#(/\x./\y.yap(succ(x), y), _|_, X)) > foldr#(/\x./\y.yap(succ(x), y), _|_, X) #argfun-yap##(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) foldr(/\x./\y.yap(F(x), y), X, nil) >= X foldr(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= yap(F(Y), foldr(/\x./\y.yap(F(x), y), X, Z)) @_{o -> o}(succ(X), Y) >= Y length(X) >= foldr(/\x./\y.yap(succ(x), y), _|_, X) yap(F, X) >= @_{o -> o}(F, X) foldr(F, X, Y) >= foldr#(F, X, Y) length(X) >= #argfun-length##(foldr#(/\x./\y.yap(succ(x), y), _|_, X)) yap(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) With these choices, we have: 1] foldr#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) > #argfun-yap##(@_{o -> o}(F(Y), foldr(/\x./\y.yap(F(x), y), X, Z))) because [2], by definition 2] foldr#*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= #argfun-yap##(@_{o -> o}(F(Y), foldr(/\x./\y.yap(F(x), y), X, Z))) because [3], by (Select) 3] yap(F(foldr#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldr#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= #argfun-yap##(@_{o -> o}(F(Y), foldr(/\x./\y.yap(F(x), y), X, Z))) because [4], by (Star) 4] yap*(F(foldr#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldr#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= #argfun-yap##(@_{o -> o}(F(Y), foldr(/\x./\y.yap(F(x), y), X, Z))) because yap > #argfun-yap## and [5], by (Copy) 5] yap*(F(foldr#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldr#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= @_{o -> o}(F(Y), foldr(/\x./\y.yap(F(x), y), X, Z)) because yap > @_{o -> o}, [6] and [12], by (Copy) 6] yap*(F(foldr#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldr#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= F(Y) because [7], by (Select) 7] F(foldr#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))) >= F(Y) because [8], by (Meta) 8] foldr#*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= Y because [9], by (Select) 9] cons(Y, Z) >= Y because [10], by (Star) 10] cons*(Y, Z) >= Y because [11], by (Select) 11] Y >= Y by (Meta) 12] yap*(F(foldr#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldr#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= foldr(/\x./\y.yap(F(x), y), X, Z) because [13], by (Select) 13] foldr#*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= foldr(/\x./\y.yap(F(x), y), X, Z) because foldr# = foldr, foldr# 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] cons(Y, Z) > Z because [22], by definition 22] cons*(Y, Z) >= Z because [23], by (Select) 23] Z >= Z by (Meta) 24] foldr#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) > @_{o -> o}(F(Y), _|_) because [25], by definition 25] foldr#*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= @_{o -> o}(F(Y), _|_) because [26], by (Select) 26] yap(F(foldr#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldr#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= @_{o -> o}(F(Y), _|_) because [27], by (Star) 27] yap*(F(foldr#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldr#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= @_{o -> o}(F(Y), _|_) because yap > @_{o -> o}, [6] and [28], by (Copy) 28] yap*(F(foldr#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldr#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= _|_ by (Bot) 29] foldr#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= foldr#(/\x./\y.yap(F(x), y), X, Z) because foldr# in Mul, [14], [20] and [30], by (Fun) 30] cons(Y, Z) >= Z because [22], by (Star) 31] foldr#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) > @_{o -> o}(F(_|_), _|_) because [32], by definition 32] foldr#*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= @_{o -> o}(F(_|_), _|_) because [33], by (Select) 33] yap(F(foldr#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldr#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= @_{o -> o}(F(_|_), _|_) because [34], by (Star) 34] yap*(F(foldr#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldr#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= @_{o -> o}(F(_|_), _|_) because yap > @_{o -> o}, [35] and [38], by (Copy) 35] yap*(F(foldr#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldr#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= F(_|_) because [36], by (Select) 36] F(foldr#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))) >= F(_|_) because [37], by (Meta) 37] foldr#*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= _|_ by (Bot) 38] yap*(F(foldr#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldr#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= _|_ by (Bot) 39] #argfun-length##(foldr#(/\x./\y.yap(succ(x), y), _|_, X)) > foldr#(/\x./\y.yap(succ(x), y), _|_, X) because [40], by definition 40] #argfun-length##*(foldr#(/\x./\y.yap(succ(x), y), _|_, X)) >= foldr#(/\x./\y.yap(succ(x), y), _|_, X) because #argfun-length## > foldr#, [41], [49] and [50], by (Copy) 41] #argfun-length##*(foldr#(/\x./\y.yap(succ(x), y), _|_, X)) >= /\x./\y.yap(succ(x), y) because [42], by (F-Abs) 42] #argfun-length##*(foldr#(/\x./\y.yap(succ(x), y), _|_, X), z) >= /\x.yap(succ(z), x) because [43], by (F-Abs) 43] #argfun-length##*(foldr#(/\x./\y.yap(succ(x), y), _|_, X), z, u) >= yap(succ(z), u) because #argfun-length## > yap, [44] and [47], by (Copy) 44] #argfun-length##*(foldr#(/\x./\y.yap(succ(x), y), _|_, X), z, u) >= succ(z) because #argfun-length## > succ and [45], by (Copy) 45] #argfun-length##*(foldr#(/\x./\y.yap(succ(x), y), _|_, X), z, u) >= z because [46], by (Select) 46] z >= z by (Var) 47] #argfun-length##*(foldr#(/\x./\y.yap(succ(x), y), _|_, X), z, u) >= u because [48], by (Select) 48] u >= u by (Var) 49] #argfun-length##*(foldr#(/\x./\y.yap(succ(x), y), _|_, X)) >= _|_ by (Bot) 50] #argfun-length##*(foldr#(/\x./\y.yap(succ(x), y), _|_, X)) >= X because [51], by (Select) 51] foldr#(/\x./\y.yap(succ(x), y), _|_, X) >= X because [52], by (Star) 52] foldr#*(/\x./\y.yap(succ(x), y), _|_, X) >= X because [53], by (Select) 53] X >= X by (Meta) 54] #argfun-yap##(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) because [55], by (Star) 55] #argfun-yap##*(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) because [56], by (Select) 56] @_{o -> o}(F, X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [57] and [58], by (Fun) 57] F >= F by (Meta) 58] X >= X by (Meta) 59] foldr(/\x./\y.yap(F(x), y), X, nil) >= X because [60], by (Star) 60] foldr*(/\x./\y.yap(F(x), y), X, nil) >= X because [61], by (Select) 61] X >= X by (Meta) 62] foldr(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= yap(F(Y), foldr(/\x./\y.yap(F(x), y), X, Z)) because [63], by (Star) 63] foldr*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= yap(F(Y), foldr(/\x./\y.yap(F(x), y), X, Z)) because foldr > yap, [64] and [68], by (Copy) 64] foldr*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= F(Y) because [65], by (Select) 65] /\x.yap(F(foldr*(/\y./\z.yap(F(y), z), X, cons(Y, Z))), x) >= F(Y) because [66], by (Eta)[Kop13:2] 66] F(foldr*(/\x./\y.yap(F(x), y), X, cons(Y, Z))) >= F(Y) because [67], by (Meta) 67] foldr*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= Y because [9], by (Select) 68] foldr*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= foldr(/\x./\y.yap(F(x), y), X, Z) because foldr in Mul, [14], [20] and [21], by (Stat) 69] @_{o -> o}(succ(X), Y) >= Y because [70], by (Star) 70] @_{o -> o}*(succ(X), Y) >= Y because [71], by (Select) 71] Y >= Y by (Meta) 72] length(X) >= foldr(/\x./\y.yap(succ(x), y), _|_, X) because [73], by (Star) 73] length*(X) >= foldr(/\x./\y.yap(succ(x), y), _|_, X) because length > foldr, [74], [82] and [83], by (Copy) 74] length*(X) >= /\y./\z.yap(succ(y), z) because [75], by (F-Abs) 75] length*(X, x) >= /\z.yap(succ(x), z) because [76], by (F-Abs) 76] length*(X, x, y) >= yap(succ(x), y) because length > yap, [77] and [80], by (Copy) 77] length*(X, x, y) >= succ(x) because length > succ and [78], by (Copy) 78] length*(X, x, y) >= x because [79], by (Select) 79] x >= x by (Var) 80] length*(X, x, y) >= y because [81], by (Select) 81] y >= y by (Var) 82] length*(X) >= _|_ by (Bot) 83] length*(X) >= X because [53], by (Select) 84] yap(F, X) >= @_{o -> o}(F, X) because [85], by (Star) 85] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [86] and [87], by (Copy) 86] yap*(F, X) >= F because [57], by (Select) 87] yap*(F, X) >= X because [58], by (Select) 88] foldr(F, X, Y) >= foldr#(F, X, Y) because foldr = foldr#, foldr in Mul, [89], [90] and [91], by (Fun) 89] F >= F by (Meta) 90] X >= X by (Meta) 91] Y >= Y by (Meta) 92] length(X) >= #argfun-length##(foldr#(/\x./\y.yap(succ(x), y), _|_, X)) because [93], by (Star) 93] length*(X) >= #argfun-length##(foldr#(/\x./\y.yap(succ(x), y), _|_, X)) because length > #argfun-length## and [94], by (Copy) 94] length*(X) >= foldr#(/\x./\y.yap(succ(x), y), _|_, X) because length > foldr#, [95], [103] and [104], by (Copy) 95] length*(X) >= /\y./\z.yap(succ(y), z) because [96], by (F-Abs) 96] length*(X, x) >= /\z.yap(succ(x), z) because [97], by (F-Abs) 97] length*(X, x, y) >= yap(succ(x), y) because length > yap, [98] and [101], by (Copy) 98] length*(X, x, y) >= succ(x) because length > succ and [99], by (Copy) 99] length*(X, x, y) >= x because [100], by (Select) 100] x >= x by (Var) 101] length*(X, x, y) >= y because [102], by (Select) 102] y >= y by (Var) 103] length*(X) >= _|_ by (Bot) 104] length*(X) >= X because [105], by (Select) 105] X >= X by (Meta) 106] yap(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) because [107], by (Star) 107] yap*(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) because yap > #argfun-yap## and [108], by (Copy) 108] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [109] and [111], by (Copy) 109] yap*(F, X) >= F because [110], by (Select) 110] F >= F by (Meta) 111] yap*(F, X) >= X because [112], by (Select) 112] 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: foldr#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) =#> foldr#(/\z./\u.yap(F(z), u), X, 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 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: foldr#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) =#> foldr#(/\z./\u.yap(F(z), u), X, Z) 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) foldr(/\x./\y.yap(F(x), y), X, nil) >= X foldr(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= yap(F(Y), foldr(/\z./\u.yap(F(z), u), X, Z)) succ(X) Y >= s(Y) length(X) >= foldr(/\x./\y.yap(succ(x), y), 0, X) 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]] = _|_ [[s(x_1)]] = x_1 We choose Lex = {} and Mul = {#argfun-yap##, @_{o -> o}, cons, foldr, length, nil, succ, yap, yap#}, and the following precedence: cons > length > nil > succ > foldr > 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) foldr(/\x./\y.yap(F(x), y), X, nil) >= X foldr(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= yap(F(Y), foldr(/\x./\y.yap(F(x), y), X, Z)) @_{o -> o}(succ(X), Y) >= Y length(X) >= foldr(/\x./\y.yap(succ(x), y), _|_, X) 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] foldr(/\x./\y.yap(F(x), y), X, nil) >= X because [7], by (Star) 7] foldr*(/\x./\y.yap(F(x), y), X, nil) >= X because [8], by (Select) 8] X >= X by (Meta) 9] foldr(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= yap(F(Y), foldr(/\x./\y.yap(F(x), y), X, Z)) because [10], by (Star) 10] foldr*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= yap(F(Y), foldr(/\x./\y.yap(F(x), y), X, Z)) because [11], by (Select) 11] yap(F(foldr*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldr*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= yap(F(Y), foldr(/\x./\y.yap(F(x), y), X, Z)) because yap in Mul, [12] and [17], by (Fun) 12] F(foldr*(/\x./\y.yap(F(x), y), X, cons(Y, Z))) >= F(Y) because [13], by (Meta) 13] foldr*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= Y because [14], by (Select) 14] cons(Y, Z) >= Y because [15], by (Star) 15] cons*(Y, Z) >= Y because [16], by (Select) 16] Y >= Y by (Meta) 17] foldr*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= foldr(/\x./\y.yap(F(x), y), X, Z) because foldr in Mul, [18], [24] and [25], by (Stat) 18] /\x./\z.yap(F(x), z) >= /\x./\z.yap(F(x), z) because [19], by (Abs) 19] /\z.yap(F(y), z) >= /\z.yap(F(y), z) because [20], by (Abs) 20] yap(F(y), x) >= yap(F(y), x) because yap in Mul, [21] and [23], by (Fun) 21] F(y) >= F(y) because [22], by (Meta) 22] y >= y by (Var) 23] x >= x by (Var) 24] X >= X by (Meta) 25] cons(Y, Z) > Z because [26], by definition 26] cons*(Y, Z) >= Z because [27], by (Select) 27] Z >= Z by (Meta) 28] @_{o -> o}(succ(X), Y) >= Y because [29], by (Star) 29] @_{o -> o}*(succ(X), Y) >= Y because [30], by (Select) 30] Y >= Y by (Meta) 31] length(X) >= foldr(/\x./\y.yap(succ(x), y), _|_, X) because [32], by (Star) 32] length*(X) >= foldr(/\x./\y.yap(succ(x), y), _|_, X) because length > foldr, [33], [41] and [42], by (Copy) 33] length*(X) >= /\y./\z.yap(succ(y), z) because [34], by (F-Abs) 34] length*(X, x) >= /\z.yap(succ(x), z) because [35], by (F-Abs) 35] length*(X, x, y) >= yap(succ(x), y) because length > yap, [36] and [39], by (Copy) 36] length*(X, x, y) >= succ(x) because length > succ and [37], by (Copy) 37] length*(X, x, y) >= x because [38], by (Select) 38] x >= x by (Var) 39] length*(X, x, y) >= y because [40], by (Select) 40] y >= y by (Var) 41] length*(X) >= _|_ by (Bot) 42] length*(X) >= X because [43], by (Select) 43] X >= X by (Meta) 44] yap(F, X) >= @_{o -> o}(F, X) because [45], by (Star) 45] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [46] and [47], by (Copy) 46] yap*(F, X) >= F because [4], by (Select) 47] yap*(F, X) >= X because [5], by (Select) 48] yap(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) because [49], by (Star) 49] yap*(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) because yap > #argfun-yap## and [50], by (Copy) 50] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [51] and [53], by (Copy) 51] yap*(F, X) >= F because [52], by (Select) 52] F >= F by (Meta) 53] yap*(F, X) >= X because [54], by (Select) 54] 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(foldr#) = 3 Thus, we can orient the dependency pairs as follows: nu(foldr#(/\x./\y.yap(F(x), y), X, cons(Y, Z))) = cons(Y, Z) |> Z = nu(foldr#(/\z./\u.yap(F(z), u), X, Z)) 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.