We consider the system h47. Alphabet: 0 : [] --> nat rec : [nat * nat * nat -> nat -> nat] --> nat s : [nat] --> nat xap : [nat -> nat -> nat * nat] --> nat -> nat xplus : [nat * nat] --> nat xtimes : [nat * nat] --> nat yap : [nat -> nat * nat] --> nat Rules: xplus(x, 0) => x xplus(x, s(y)) => s(xplus(x, y)) 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))) xtimes(x, y) => rec(y, 0, /\z./\u.xplus(x, u)) 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 rec : [nat * nat * nat -> nat -> nat] --> nat s : [nat] --> nat xplus : [nat * nat] --> nat xtimes : [nat * nat] --> nat yap : [nat -> nat * nat] --> nat Rules: xplus(X, 0) => X xplus(X, s(Y)) => s(xplus(X, Y)) 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))) xtimes(X, Y) => rec(Y, 0, /\x./\y.xplus(X, y)) yap(F, X) => F X We observe that the rules contain a first-order subset: xplus(X, 0) => X xplus(X, s(Y)) => s(xplus(X, 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: || || xplus(%X, 0) -> %X || xplus(%X, s(%Y)) -> s(xplus(%X, %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 > xplus_2 > s_1 > 0 || || and weight map: || || 0=1 || s_1=1 || xplus_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: || || xplus(%X, 0) -> %X || xplus(%X, s(%Y)) -> s(xplus(%X, %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] xtimes#(X, Y) =#> rec#(Y, 0, /\x./\y.xplus(X, y)) 6] xtimes#(X, Y) =#> xplus#(X, x) 7] yap#(F, X) =#> F(X) Rules R_0: xplus(X, 0) => X xplus(X, s(Y)) => s(xplus(X, Y)) 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))) xtimes(X, Y) => rec(Y, 0, /\x./\y.xplus(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 : 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 : 0, 1, 2, 3, 4 * 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) xtimes#(X, Y) =#> rec#(Y, 0, /\x./\y.xplus(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#(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 xtimes#(X, Y) >? rec#(Y, 0, /\x./\y.xplus(X, y)) yap#(F, X) >? F(X) xplus(X, 0) >= X xplus(X, s(Y)) >= s(xplus(X, Y)) 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))) xtimes(X, Y) >= rec(Y, 0, /\x./\y.xplus(X, y)) yap(F, X) >= F X rec(X, Y, F) >= rec#(X, Y, F) xtimes(X, Y) >= xtimes#(X, Y) yap(F, X) >= yap#(F, X) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( xtimes#(X, Y) ) = #argfun-xtimes##(rec#(Y, 0, /\x./\y.xplus(X, 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: [[0]] = _|_ [[~c0]] = _|_ [[~c1]] = _|_ [[~c2]] = _|_ We choose Lex = {} and Mul = {#argfun-xtimes##, #argfun-yap##, @_{o -> o}, rec, rec#, s, xplus, xtimes, xtimes#, yap, yap#}, and the following precedence: yap > yap# > xtimes > xplus > s > #argfun-xtimes## > xtimes# > rec = rec# > @_{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#(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-xtimes##(rec#(X, _|_, /\x./\y.xplus(Y, y))) >= rec#(X, _|_, /\x./\y.xplus(Y, y)) #argfun-yap##(@_{o -> o}(F, X)) > @_{o -> o}(F, X) xplus(X, _|_) >= X xplus(X, s(Y)) >= s(xplus(X, Y)) 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))) xtimes(X, Y) >= rec(Y, _|_, /\x./\y.xplus(X, y)) yap(F, X) >= @_{o -> o}(F, X) rec(X, Y, F) >= rec#(X, Y, F) xtimes(X, Y) >= #argfun-xtimes##(rec#(Y, _|_, /\x./\y.xplus(X, y))) 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)) > @_{o -> o}(F(X), _|_) because [24], by definition 24] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= @_{o -> o}(F(X), _|_) because rec# > @_{o -> o}, [25] and [27], by (Copy) 25] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= F(X) because [26], by (Select) 26] /\x.yap(F(rec#*(s(X), Y, /\y./\z.yap(F(y), z))), x) >= F(X) because [7], by (Eta)[Kop13:2] 27] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= _|_ by (Bot) 28] rec#(s(X), Y, /\x./\y.yap(F(x), y)) >= rec#(X, Y, /\x./\y.yap(F(x), y)) because rec# in Mul, [29], [16] and [17], by (Fun) 29] s(X) >= X because [15], by (Star) 30] rec#(s(X), Y, /\x./\y.yap(F(x), y)) > @_{o -> o}(F(_|_), _|_) because [31], by definition 31] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= @_{o -> o}(F(_|_), _|_) because [32], by (Select) 32] 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 [33], by (Star) 33] 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}, [34] and [37], by (Copy) 34] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= F(_|_) because [35], by (Select) 35] F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(_|_) because [36], by (Meta) 36] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= _|_ by (Bot) 37] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= _|_ by (Bot) 38] #argfun-xtimes##(rec#(X, _|_, /\x./\y.xplus(Y, y))) >= rec#(X, _|_, /\x./\y.xplus(Y, y)) because [39], by (Star) 39] #argfun-xtimes##*(rec#(X, _|_, /\x./\y.xplus(Y, y))) >= rec#(X, _|_, /\x./\y.xplus(Y, y)) because [40], by (Select) 40] rec#(X, _|_, /\x./\y.xplus(Y, y)) >= rec#(X, _|_, /\x./\y.xplus(Y, y)) because rec# in Mul, [41], [42] and [43], by (Fun) 41] X >= X by (Meta) 42] _|_ >= _|_ by (Bot) 43] /\x./\y.xplus(Y, y) >= /\x./\y.xplus(Y, y) because [44], by (Abs) 44] /\y.xplus(Y, y) >= /\y.xplus(Y, y) because [45], by (Abs) 45] xplus(Y, x) >= xplus(Y, x) because xplus in Mul, [46] and [47], by (Fun) 46] Y >= Y by (Meta) 47] x >= x by (Var) 48] #argfun-yap##(@_{o -> o}(F, X)) > @_{o -> o}(F, X) because [49], by definition 49] #argfun-yap##*(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) because [50], by (Select) 50] @_{o -> o}(F, X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [51] and [52], by (Fun) 51] F >= F by (Meta) 52] X >= X by (Meta) 53] xplus(X, _|_) >= X because [54], by (Star) 54] xplus*(X, _|_) >= X because [55], by (Select) 55] X >= X by (Meta) 56] xplus(X, s(Y)) >= s(xplus(X, Y)) because [57], by (Star) 57] xplus*(X, s(Y)) >= s(xplus(X, Y)) because xplus > s and [58], by (Copy) 58] xplus*(X, s(Y)) >= xplus(X, Y) because xplus in Mul, [59] and [60], by (Stat) 59] X >= X by (Meta) 60] s(Y) > Y because [61], by definition 61] s*(Y) >= Y because [62], by (Select) 62] Y >= Y by (Meta) 63] rec(_|_, X, /\x./\y.yap(F(x), y)) >= X because [64], by (Star) 64] rec*(_|_, X, /\x./\y.yap(F(x), y)) >= X because [65], by (Select) 65] X >= X by (Meta) 66] rec(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) because [67], by (Star) 67] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) because [68], by (Select) 68] 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, [69] and [71], by (Fun) 69] F(rec*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(X) because [70], by (Meta) 70] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= X because [29], by (Select) 71] 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) 72] xtimes(X, Y) >= rec(Y, _|_, /\x./\y.xplus(X, y)) because [73], by (Star) 73] xtimes*(X, Y) >= rec(Y, _|_, /\x./\y.xplus(X, y)) because xtimes > rec, [74], [75] and [76], by (Copy) 74] xtimes*(X, Y) >= Y because [41], by (Select) 75] xtimes*(X, Y) >= _|_ by (Bot) 76] xtimes*(X, Y) >= /\y./\z.xplus(X, z) because [77], by (F-Abs) 77] xtimes*(X, Y, x) >= /\z.xplus(X, z) because [78], by (F-Abs) 78] xtimes*(X, Y, x, y) >= xplus(X, y) because xtimes > xplus, [79] and [80], by (Copy) 79] xtimes*(X, Y, x, y) >= X because [46], by (Select) 80] xtimes*(X, Y, x, y) >= y because [81], by (Select) 81] y >= y by (Var) 82] yap(F, X) >= @_{o -> o}(F, X) because [83], by (Star) 83] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [84] and [85], by (Copy) 84] yap*(F, X) >= F because [51], by (Select) 85] yap*(F, X) >= X because [52], by (Select) 86] rec(X, Y, F) >= rec#(X, Y, F) because rec = rec#, rec in Mul, [87], [88] and [89], by (Fun) 87] X >= X by (Meta) 88] Y >= Y by (Meta) 89] F >= F by (Meta) 90] xtimes(X, Y) >= #argfun-xtimes##(rec#(Y, _|_, /\x./\y.xplus(X, y))) because [91], by (Star) 91] xtimes*(X, Y) >= #argfun-xtimes##(rec#(Y, _|_, /\x./\y.xplus(X, y))) because xtimes > #argfun-xtimes## and [92], by (Copy) 92] xtimes*(X, Y) >= rec#(Y, _|_, /\x./\y.xplus(X, y)) because xtimes > rec#, [93], [95] and [96], by (Copy) 93] xtimes*(X, Y) >= Y because [94], by (Select) 94] Y >= Y by (Meta) 95] xtimes*(X, Y) >= _|_ by (Bot) 96] xtimes*(X, Y) >= /\y./\z.xplus(X, z) because [97], by (F-Abs) 97] xtimes*(X, Y, x) >= /\z.xplus(X, z) because [98], by (F-Abs) 98] xtimes*(X, Y, x, y) >= xplus(X, y) because xtimes > xplus, [99] and [101], by (Copy) 99] xtimes*(X, Y, x, y) >= X because [100], by (Select) 100] X >= X by (Meta) 101] xtimes*(X, Y, x, y) >= y because [102], by (Select) 102] y >= y by (Var) 103] yap(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) because [104], by (Star) 104] yap*(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) because yap > #argfun-yap## and [105], by (Copy) 105] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [106] and [108], by (Copy) 106] yap*(F, X) >= F because [107], by (Select) 107] F >= F by (Meta) 108] yap*(F, X) >= X because [109], by (Select) 109] 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)) xtimes#(X, Y) =#> rec#(Y, 0, /\x./\y.xplus(X, y)) 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 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)) 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). 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.