We consider the system kop11cai1. Alphabet: 0 : [] --> nat cons : [nat * list] --> list map : [nat -> nat * list] --> list nil : [] --> list op : [nat -> nat * nat -> nat] --> nat -> nat pow : [nat -> nat * nat] --> nat -> nat s : [nat] --> nat Rules: map(f, nil) => nil map(f, cons(x, y)) => cons(f x, map(f, y)) pow(f, 0) => /\x.x pow(f, s(x)) => op(f, pow(f, x)) op(f, g) x => f (g x) /\x.f x => f Using the transformations described in [Kop11], this system can be brought in a form without leading free variables in the left-hand side, and where the left-hand side of a variable is always a functional term or application headed by a functional term. We now transform the resulting AFS into an AFSM by replacing all free variables by meta-variables (with arity 0). This leads to the following AFSM: Alphabet: 0 : [] --> nat cons : [nat * list] --> list map : [nat -> nat * list] --> list nil : [] --> list op : [nat -> nat * nat -> nat] --> nat -> nat pow : [nat -> nat * nat] --> nat -> nat s : [nat] --> nat ~AP1 : [nat -> nat * nat] --> nat ~L1 : [nat -> nat] --> nat -> nat Rules: map(F, nil) => nil map(F, cons(X, Y)) => cons(~AP1(F, X), map(F, Y)) pow(F, 0) => ~L1(/\x.x) pow(F, s(X)) => op(F, pow(F, X)) op(F, G) X => ~AP1(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) => F ~L1(/\x.op(F, G) x) => op(F, G) ~L1(/\x.pow(F, X) x) => pow(F, X) ~AP1(F, X) => F X ~L1(F) => F 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] map#(F, cons(X, Y)) =#> ~AP1#(F, X) 1] map#(F, cons(X, Y)) =#> map#(F, Y) 2] pow(F, 0) X =#> ~L1(/\x.x) X 3] pow#(F, 0) =#> ~L1#(/\x.x) 4] pow(F, s(X)) Y =#> op(F, pow(F, X)) Y 5] pow#(F, s(X)) =#> op#(F, pow(F, X)) 6] pow#(F, s(X)) =#> pow#(F, X) 7] op(F, G) X =#> ~AP1#(F, ~AP1(G, X)) 8] op(F, G) X =#> ~AP1#(G, X) 9] ~L1(/\x.~AP1(F, x)) X =#> F(X) 10] ~L1(/\x.op(F, G) x) X =#> op(F, G) X 11] ~L1#(/\x.op(F, G) x) =#> op#(F, G) 12] ~L1(/\x.pow(F, X) x) Y =#> pow(F, X) Y 13] ~L1#(/\x.pow(F, X) x) =#> pow#(F, X) 14] ~AP1#(F, X) =#> F(X) 15] ~L1(F) X =#> F(X) Rules R_0: map(F, nil) => nil map(F, cons(X, Y)) => cons(~AP1(F, X), map(F, Y)) pow(F, 0) => ~L1(/\x.x) pow(F, s(X)) => op(F, pow(F, X)) op(F, G) X => ~AP1(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) => F ~L1(/\x.op(F, G) x) => op(F, G) ~L1(/\x.pow(F, X) x) => pow(F, X) ~AP1(F, X) => F X ~L1(F) => F 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 : 14 * 1 : 0, 1 * 2 : 15 * 3 : * 4 : 7, 8 * 5 : * 6 : 3, 5, 6 * 7 : 14 * 8 : 14 * 9 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15 * 10 : 7, 8 * 11 : * 12 : 2, 4 * 13 : 3, 5, 6 * 14 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15 * 15 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15 This graph has the following strongly connected components: P_1: map#(F, cons(X, Y)) =#> ~AP1#(F, X) map#(F, cons(X, Y)) =#> map#(F, Y) pow(F, 0) X =#> ~L1(/\x.x) X pow(F, s(X)) Y =#> op(F, pow(F, X)) Y op(F, G) X =#> ~AP1#(F, ~AP1(G, X)) op(F, G) X =#> ~AP1#(G, X) ~L1(/\x.~AP1(F, x)) X =#> F(X) ~L1(/\x.op(F, G) x) X =#> op(F, G) X ~L1(/\x.pow(F, X) x) Y =#> pow(F, X) Y ~AP1#(F, X) =#> F(X) ~L1(F) X =#> F(X) P_2: pow#(F, s(X)) =#> pow#(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) and (P_2, R_0, m, f). Thus, the original system is terminating if each of (P_1, R_0, minimal, all) and (P_2, R_0, minimal, all) is finite. We consider the dependency pair problem (P_2, R_0, minimal, all). We apply the subterm criterion with the following projection function: nu(pow#) = 2 Thus, we can orient the dependency pairs as follows: nu(pow#(F, s(X))) = s(X) |> X = nu(pow#(F, X)) By [Kop12, Thm. 7.35], we may replace a dependency pair problem (P_2, 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_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: map#(F, cons(X, Y)) >? ~AP1#(F, X) map#(F, cons(X, Y)) >? map#(F, Y) pow(F, 0) X >? ~L1(/\x.x) X pow(F, s(X)) Y >? op(F, pow(F, X)) Y op(F, G) X >? ~AP1#(F, ~AP1(G, X)) op(F, G) X >? ~AP1#(G, X) ~L1(/\x.~AP1(F, x)) X >? F(X) ~L1(/\x.op(F, G) x) X >? op(F, G) X ~L1(/\x.pow(F, X) x) Y >? pow(F, X) Y ~AP1#(F, X) >? F(X) ~L1(F) X >? F(X) map(F, nil) >= nil map(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) pow(F, 0) >= ~L1(/\x.x) pow(F, s(X)) >= op(F, pow(F, X)) op(F, G) X >= ~AP1(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) >= F ~L1(/\x.op(F, G) x) >= op(F, G) ~L1(/\x.pow(F, X) x) >= pow(F, X) ~AP1(F, X) >= F X ~L1(F) >= F map(F, X) >= map#(F, X) ~AP1(F, X) >= ~AP1#(F, X) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( ~AP1#(F, X) ) = #argfun-~AP1##(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]. We choose Lex = {} and Mul = {#argfun-~AP1##, 0, @_{o -> o}, cons, map, map#, nil, op, pow, s, ~AP1, ~AP1#, ~L1}, and the following precedence: map > map# > ~AP1# > pow > op > ~AP1 > cons > s > #argfun-~AP1## > @_{o -> o} > ~L1 > nil > 0 With these choices, we have: 1] map#(F, cons(X, Y)) > #argfun-~AP1##(@_{o -> o}(F, X)) because [2], by definition 2] map#*(F, cons(X, Y)) >= #argfun-~AP1##(@_{o -> o}(F, X)) because map# > #argfun-~AP1## and [3], by (Copy) 3] map#*(F, cons(X, Y)) >= @_{o -> o}(F, X) because map# > @_{o -> o}, [4] and [6], by (Copy) 4] map#*(F, cons(X, Y)) >= F because [5], by (Select) 5] F >= F by (Meta) 6] map#*(F, cons(X, Y)) >= X because [7], by (Select) 7] cons(X, Y) >= X because [8], by (Star) 8] cons*(X, Y) >= X because [9], by (Select) 9] X >= X by (Meta) 10] map#(F, cons(X, Y)) >= map#(F, Y) because map# in Mul, [11] and [12], by (Fun) 11] F >= F by (Meta) 12] cons(X, Y) >= Y because [13], by (Star) 13] cons*(X, Y) >= Y because [14], by (Select) 14] Y >= Y by (Meta) 15] @_{o -> o}(pow(F, 0), X) >= @_{o -> o}(~L1(/\x.x), X) because @_{o -> o} in Mul, [16] and [21], by (Fun) 16] pow(F, 0) >= ~L1(/\x.x) because [17], by (Star) 17] pow*(F, 0) >= ~L1(/\x.x) because pow > ~L1 and [18], by (Copy) 18] pow*(F, 0) >= /\y.y because [19], by (F-Abs) 19] pow*(F, 0, x) >= x because [20], by (Select) 20] x >= x by (Var) 21] X >= X by (Meta) 22] @_{o -> o}(pow(F, s(X)), Y) >= @_{o -> o}(op(F, pow(F, X)), Y) because @_{o -> o} in Mul, [23] and [32], by (Fun) 23] pow(F, s(X)) >= op(F, pow(F, X)) because [24], by (Star) 24] pow*(F, s(X)) >= op(F, pow(F, X)) because pow > op, [25] and [27], by (Copy) 25] pow*(F, s(X)) >= F because [26], by (Select) 26] F >= F by (Meta) 27] pow*(F, s(X)) >= pow(F, X) because pow in Mul, [28] and [29], by (Stat) 28] F >= F by (Meta) 29] s(X) > X because [30], by definition 30] s*(X) >= X because [31], by (Select) 31] X >= X by (Meta) 32] Y >= Y by (Meta) 33] @_{o -> o}(op(F, G), X) >= #argfun-~AP1##(@_{o -> o}(F, ~AP1(G, X))) because [34], by (Star) 34] @_{o -> o}*(op(F, G), X) >= #argfun-~AP1##(@_{o -> o}(F, ~AP1(G, X))) because [35], by (Select) 35] op(F, G) @_{o -> o}*(op(F, G), X) >= #argfun-~AP1##(@_{o -> o}(F, ~AP1(G, X))) because [36] 36] op*(F, G, @_{o -> o}*(op(F, G), X)) >= #argfun-~AP1##(@_{o -> o}(F, ~AP1(G, X))) because op > #argfun-~AP1## and [37], by (Copy) 37] op*(F, G, @_{o -> o}*(op(F, G), X)) >= @_{o -> o}(F, ~AP1(G, X)) because op > @_{o -> o}, [38] and [40], by (Copy) 38] op*(F, G, @_{o -> o}*(op(F, G), X)) >= F because [39], by (Select) 39] F >= F by (Meta) 40] op*(F, G, @_{o -> o}*(op(F, G), X)) >= ~AP1(G, X) because op > ~AP1, [41] and [43], by (Copy) 41] op*(F, G, @_{o -> o}*(op(F, G), X)) >= G because [42], by (Select) 42] G >= G by (Meta) 43] op*(F, G, @_{o -> o}*(op(F, G), X)) >= X because [44], by (Select) 44] @_{o -> o}*(op(F, G), X) >= X because [45], by (Select) 45] X >= X by (Meta) 46] @_{o -> o}(op(F, G), X) > #argfun-~AP1##(@_{o -> o}(G, X)) because [47], by definition 47] @_{o -> o}*(op(F, G), X) >= #argfun-~AP1##(@_{o -> o}(G, X)) because [48], by (Select) 48] op(F, G) @_{o -> o}*(op(F, G), X) >= #argfun-~AP1##(@_{o -> o}(G, X)) because [49] 49] op*(F, G, @_{o -> o}*(op(F, G), X)) >= #argfun-~AP1##(@_{o -> o}(G, X)) because op > #argfun-~AP1## and [50], by (Copy) 50] op*(F, G, @_{o -> o}*(op(F, G), X)) >= @_{o -> o}(G, X) because op > @_{o -> o}, [41] and [43], by (Copy) 51] @_{o -> o}(~L1(/\x.~AP1(F, x)), X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [52] and [56], by (Fun) 52] ~L1(/\x.~AP1(F, x)) >= F because [53], by (Star) 53] ~L1*(/\x.~AP1(F, x)) >= F because [54], by (Select) 54] /\x.~AP1(F, x) >= F because [55], by (Eta)[Kop13:2] 55] F >= F by (Meta) 56] X >= X by (Meta) 57] @_{o -> o}(~L1(/\x.@_{o -> o}(op(F, G), x)), X) >= @_{o -> o}(op(F, G), X) because @_{o -> o} in Mul, [58] and [64], by (Fun) 58] ~L1(/\x.@_{o -> o}(op(F, G), x)) >= op(F, G) because [59], by (Star) 59] ~L1*(/\x.@_{o -> o}(op(F, G), x)) >= op(F, G) because [60], by (Select) 60] /\x.@_{o -> o}(op(F, G), x) >= op(F, G) because [61], by (Eta)[Kop13:2] 61] op(F, G) >= op(F, G) because op in Mul, [62] and [63], by (Fun) 62] F >= F by (Meta) 63] G >= G by (Meta) 64] X >= X by (Meta) 65] @_{o -> o}(~L1(/\x.@_{o -> o}(pow(F, X), x)), Y) >= @_{o -> o}(pow(F, X), Y) because @_{o -> o} in Mul, [66] and [72], by (Fun) 66] ~L1(/\x.@_{o -> o}(pow(F, X), x)) >= pow(F, X) because [67], by (Star) 67] ~L1*(/\x.@_{o -> o}(pow(F, X), x)) >= pow(F, X) because [68], by (Select) 68] /\x.@_{o -> o}(pow(F, X), x) >= pow(F, X) because [69], by (Eta)[Kop13:2] 69] pow(F, X) >= pow(F, X) because pow in Mul, [70] and [71], by (Fun) 70] F >= F by (Meta) 71] X >= X by (Meta) 72] Y >= Y by (Meta) 73] #argfun-~AP1##(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) because [74], by (Star) 74] #argfun-~AP1##*(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) because [75], by (Select) 75] @_{o -> o}(F, X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [76] and [77], by (Fun) 76] F >= F by (Meta) 77] X >= X by (Meta) 78] @_{o -> o}(~L1(F), X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [79] and [82], by (Fun) 79] ~L1(F) >= F because [80], by (Star) 80] ~L1*(F) >= F because [81], by (Select) 81] F >= F by (Meta) 82] X >= X by (Meta) 83] map(F, nil) >= nil because [84], by (Star) 84] map*(F, nil) >= nil because map > nil, by (Copy) 85] map(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) because [86], by (Star) 86] map*(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) because map > cons, [87] and [90], by (Copy) 87] map*(F, cons(X, Y)) >= ~AP1(F, X) because map > ~AP1, [88] and [89], by (Copy) 88] map*(F, cons(X, Y)) >= F because [11], by (Select) 89] map*(F, cons(X, Y)) >= X because [7], by (Select) 90] map*(F, cons(X, Y)) >= map(F, Y) because map in Mul, [11] and [91], by (Stat) 91] cons(X, Y) > Y because [92], by definition 92] cons*(X, Y) >= Y because [14], by (Select) 93] pow(F, 0) >= ~L1(/\x.x) because [17], by (Star) 94] pow(F, s(X)) >= op(F, pow(F, X)) because [24], by (Star) 95] @_{o -> o}(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [96], by (Star) 96] @_{o -> o}*(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [97], by (Select) 97] op(F, G) @_{o -> o}*(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [98] 98] op*(F, G, @_{o -> o}*(op(F, G), X)) >= ~AP1(F, ~AP1(G, X)) because op > ~AP1, [38] and [40], by (Copy) 99] ~L1(/\x.~AP1(F, x)) >= F because [53], by (Star) 100] ~L1(/\x.@_{o -> o}(op(F, G), x)) >= op(F, G) because [59], by (Star) 101] ~L1(/\x.@_{o -> o}(pow(F, X), x)) >= pow(F, X) because [67], by (Star) 102] ~AP1(F, X) >= @_{o -> o}(F, X) because [103], by (Star) 103] ~AP1*(F, X) >= @_{o -> o}(F, X) because ~AP1 > @_{o -> o}, [104] and [105], by (Copy) 104] ~AP1*(F, X) >= F because [76], by (Select) 105] ~AP1*(F, X) >= X because [77], by (Select) 106] ~L1(F) >= F because [80], by (Star) 107] map(F, X) >= map#(F, X) because [108], by (Star) 108] map*(F, X) >= map#(F, X) because map > map#, [109] and [111], by (Copy) 109] map*(F, X) >= F because [110], by (Select) 110] F >= F by (Meta) 111] map*(F, X) >= X because [112], by (Select) 112] X >= X by (Meta) 113] ~AP1(F, X) >= #argfun-~AP1##(@_{o -> o}(F, X)) because [114], by (Star) 114] ~AP1*(F, X) >= #argfun-~AP1##(@_{o -> o}(F, X)) because ~AP1 > #argfun-~AP1## and [115], by (Copy) 115] ~AP1*(F, X) >= @_{o -> o}(F, X) because ~AP1 > @_{o -> o}, [116] and [118], by (Copy) 116] ~AP1*(F, X) >= F because [117], by (Select) 117] F >= F by (Meta) 118] ~AP1*(F, X) >= X because [119], by (Select) 119] 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_3, R_0, minimal, all), where P_3 consists of: map#(F, cons(X, Y)) =#> map#(F, Y) pow(F, 0) X =#> ~L1(/\x.x) X pow(F, s(X)) Y =#> op(F, pow(F, X)) Y op(F, G) X =#> ~AP1#(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) X =#> F(X) ~L1(/\x.op(F, G) x) X =#> op(F, G) X ~L1(/\x.pow(F, X) x) Y =#> pow(F, X) Y ~AP1#(F, X) =#> F(X) ~L1(F) X =#> F(X) Thus, the original system is terminating if (P_3, R_0, minimal, all) is finite. We consider the dependency pair problem (P_3, R_0, minimal, all). We place the elements of P in a dependency graph approximation G (see e.g. [Kop12, Thm. 7.27, 7.29], as follows: * 0 : 0 * 1 : 8 * 2 : 3 * 3 : 7 * 4 : 0, 1, 2, 3, 4, 5, 6, 7, 8 * 5 : 3 * 6 : 1, 2 * 7 : 0, 1, 2, 3, 4, 5, 6, 7, 8 * 8 : 0, 1, 2, 3, 4, 5, 6, 7, 8 This graph has the following strongly connected components: P_4: map#(F, cons(X, Y)) =#> map#(F, Y) P_5: pow(F, 0) X =#> ~L1(/\x.x) X pow(F, s(X)) Y =#> op(F, pow(F, X)) Y op(F, G) X =#> ~AP1#(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) X =#> F(X) ~L1(/\x.op(F, G) x) X =#> op(F, G) X ~L1(/\x.pow(F, X) x) Y =#> pow(F, X) Y ~AP1#(F, X) =#> F(X) ~L1(F) X =#> F(X) By [Kop12, Thm. 7.31], we may replace any dependency pair problem (P_3, R_0, m, f) by (P_4, R_0, m, f) and (P_5, R_0, m, f). Thus, the original system is terminating if each of (P_4, R_0, minimal, all) and (P_5, R_0, minimal, all) is finite. We consider the dependency pair problem (P_5, R_0, minimal, all). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: pow(F, 0) X >? ~L1(/\x.x) X pow(F, s(X)) Y >? op(F, pow(F, X)) Y op(F, G) X >? ~AP1#(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) X >? F(X) ~L1(/\x.op(F, G) x) X >? op(F, G) X ~L1(/\x.pow(F, X) x) Y >? pow(F, X) Y ~AP1#(F, X) >? F(X) ~L1(F) X >? F(X) map(F, nil) >= nil map(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) pow(F, 0) >= ~L1(/\x.x) pow(F, s(X)) >= op(F, pow(F, X)) op(F, G) X >= ~AP1(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) >= F ~L1(/\x.op(F, G) x) >= op(F, G) ~L1(/\x.pow(F, X) x) >= pow(F, X) ~AP1(F, X) >= F X ~L1(F) >= F ~AP1(F, X) >= ~AP1#(F, X) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( ~AP1#(F, X) ) = #argfun-~AP1##(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: [[nil]] = _|_ [[pow(x_1, x_2)]] = pow(x_2, x_1) We choose Lex = {pow} and Mul = {#argfun-~AP1##, 0, @_{o -> o}, cons, map, op, s, ~AP1, ~AP1#, ~L1}, and the following precedence: 0 > pow > s > op > map = ~AP1 > cons > ~AP1# > @_{o -> o} > ~L1 > #argfun-~AP1## Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: @_{o -> o}(pow(F, 0), X) >= @_{o -> o}(~L1(/\x.x), X) @_{o -> o}(pow(F, s(X)), Y) >= @_{o -> o}(op(F, pow(F, X)), Y) @_{o -> o}(op(F, G), X) >= #argfun-~AP1##(@_{o -> o}(F, ~AP1(G, X))) @_{o -> o}(~L1(/\x.~AP1(F, x)), X) >= @_{o -> o}(F, X) @_{o -> o}(~L1(/\x.@_{o -> o}(op(F, G), x)), X) > @_{o -> o}(op(F, G), X) @_{o -> o}(~L1(/\x.@_{o -> o}(pow(F, X), x)), Y) >= @_{o -> o}(pow(F, X), Y) #argfun-~AP1##(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) @_{o -> o}(~L1(F), X) >= @_{o -> o}(F, X) map(F, _|_) >= _|_ map(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) pow(F, 0) >= ~L1(/\x.x) pow(F, s(X)) >= op(F, pow(F, X)) @_{o -> o}(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) >= F ~L1(/\x.@_{o -> o}(op(F, G), x)) >= op(F, G) ~L1(/\x.@_{o -> o}(pow(F, X), x)) >= pow(F, X) ~AP1(F, X) >= @_{o -> o}(F, X) ~L1(F) >= F ~AP1(F, X) >= #argfun-~AP1##(@_{o -> o}(F, X)) With these choices, we have: 1] @_{o -> o}(pow(F, 0), X) >= @_{o -> o}(~L1(/\x.x), X) because @_{o -> o} in Mul, [2] and [7], by (Fun) 2] pow(F, 0) >= ~L1(/\x.x) because [3], by (Star) 3] pow*(F, 0) >= ~L1(/\x.x) because pow > ~L1 and [4], by (Copy) 4] pow*(F, 0) >= /\y.y because [5], by (F-Abs) 5] pow*(F, 0, x) >= x because [6], by (Select) 6] x >= x by (Var) 7] X >= X by (Meta) 8] @_{o -> o}(pow(F, s(X)), Y) >= @_{o -> o}(op(F, pow(F, X)), Y) because @_{o -> o} in Mul, [9] and [19], by (Fun) 9] pow(F, s(X)) >= op(F, pow(F, X)) because [10], by (Star) 10] pow*(F, s(X)) >= op(F, pow(F, X)) because pow > op, [11] and [13], by (Copy) 11] pow*(F, s(X)) >= F because [12], by (Select) 12] F >= F by (Meta) 13] pow*(F, s(X)) >= pow(F, X) because [14], [11] and [17], by (Stat) 14] s(X) > X because [15], by definition 15] s*(X) >= X because [16], by (Select) 16] X >= X by (Meta) 17] pow*(F, s(X)) >= X because [18], by (Select) 18] s(X) >= X because [15], by (Star) 19] Y >= Y by (Meta) 20] @_{o -> o}(op(F, G), X) >= #argfun-~AP1##(@_{o -> o}(F, ~AP1(G, X))) because [21], by (Star) 21] @_{o -> o}*(op(F, G), X) >= #argfun-~AP1##(@_{o -> o}(F, ~AP1(G, X))) because @_{o -> o} > #argfun-~AP1## and [22], by (Copy) 22] @_{o -> o}*(op(F, G), X) >= @_{o -> o}(F, ~AP1(G, X)) because [23], by (Select) 23] op(F, G) @_{o -> o}*(op(F, G), X) >= @_{o -> o}(F, ~AP1(G, X)) because [24] 24] op*(F, G, @_{o -> o}*(op(F, G), X)) >= @_{o -> o}(F, ~AP1(G, X)) because op > @_{o -> o}, [25] and [27], by (Copy) 25] op*(F, G, @_{o -> o}*(op(F, G), X)) >= F because [26], by (Select) 26] F >= F by (Meta) 27] op*(F, G, @_{o -> o}*(op(F, G), X)) >= ~AP1(G, X) because op > ~AP1, [28] and [30], by (Copy) 28] op*(F, G, @_{o -> o}*(op(F, G), X)) >= G because [29], by (Select) 29] G >= G by (Meta) 30] op*(F, G, @_{o -> o}*(op(F, G), X)) >= X because [31], by (Select) 31] @_{o -> o}*(op(F, G), X) >= X because [32], by (Select) 32] X >= X by (Meta) 33] @_{o -> o}(~L1(/\x.~AP1(F, x)), X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [34] and [38], by (Fun) 34] ~L1(/\x.~AP1(F, x)) >= F because [35], by (Star) 35] ~L1*(/\x.~AP1(F, x)) >= F because [36], by (Select) 36] /\x.~AP1(F, x) >= F because [37], by (Eta)[Kop13:2] 37] F >= F by (Meta) 38] X >= X by (Meta) 39] @_{o -> o}(~L1(/\x.@_{o -> o}(op(F, G), x)), X) > @_{o -> o}(op(F, G), X) because [40], by definition 40] @_{o -> o}*(~L1(/\x.@_{o -> o}(op(F, G), x)), X) >= @_{o -> o}(op(F, G), X) because [41], by (Select) 41] ~L1(/\x.@_{o -> o}(op(F, G), x)) @_{o -> o}*(~L1(/\y.@_{o -> o}(op(F, G), y)), X) >= @_{o -> o}(op(F, G), X) because [42] 42] ~L1*(/\x.@_{o -> o}(op(F, G), x), @_{o -> o}*(~L1(/\y.@_{o -> o}(op(F, G), y)), X)) >= @_{o -> o}(op(F, G), X) because [43], by (Select) 43] @_{o -> o}(op(F, G), ~L1*(/\x.@_{o -> o}(op(F, G), x), @_{o -> o}*(~L1(/\y.@_{o -> o}(op(F, G), y)), X))) >= @_{o -> o}(op(F, G), X) because @_{o -> o} in Mul, [44] and [47], by (Fun) 44] op(F, G) >= op(F, G) because op in Mul, [45] and [46], by (Fun) 45] F >= F by (Meta) 46] G >= G by (Meta) 47] ~L1*(/\x.@_{o -> o}(op(F, G), x), @_{o -> o}*(~L1(/\y.@_{o -> o}(op(F, G), y)), X)) >= X because [48], by (Select) 48] @_{o -> o}*(~L1(/\x.@_{o -> o}(op(F, G), x)), X) >= X because [49], by (Select) 49] X >= X by (Meta) 50] @_{o -> o}(~L1(/\x.@_{o -> o}(pow(F, X), x)), Y) >= @_{o -> o}(pow(F, X), Y) because @_{o -> o} in Mul, [51] and [57], by (Fun) 51] ~L1(/\x.@_{o -> o}(pow(F, X), x)) >= pow(F, X) because [52], by (Star) 52] ~L1*(/\x.@_{o -> o}(pow(F, X), x)) >= pow(F, X) because [53], by (Select) 53] /\x.@_{o -> o}(pow(F, X), x) >= pow(F, X) because [54], by (Eta)[Kop13:2] 54] pow(F, X) >= pow(F, X) because [55] and [56], by (Fun) 55] F >= F by (Meta) 56] X >= X by (Meta) 57] Y >= Y by (Meta) 58] #argfun-~AP1##(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) because [59], by (Star) 59] #argfun-~AP1##*(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) because [60], by (Select) 60] @_{o -> o}(F, X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [61] and [62], by (Fun) 61] F >= F by (Meta) 62] X >= X by (Meta) 63] @_{o -> o}(~L1(F), X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [64] and [67], by (Fun) 64] ~L1(F) >= F because [65], by (Star) 65] ~L1*(F) >= F because [66], by (Select) 66] F >= F by (Meta) 67] X >= X by (Meta) 68] map(F, _|_) >= _|_ by (Bot) 69] map(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) because [70], by (Star) 70] map*(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) because map > cons, [71] and [76], by (Copy) 71] map*(F, cons(X, Y)) >= ~AP1(F, X) because map = ~AP1, map in Mul, [72] and [73], by (Stat) 72] F >= F by (Meta) 73] cons(X, Y) > X because [74], by definition 74] cons*(X, Y) >= X because [75], by (Select) 75] X >= X by (Meta) 76] map*(F, cons(X, Y)) >= map(F, Y) because map in Mul, [72] and [77], by (Stat) 77] cons(X, Y) > Y because [78], by definition 78] cons*(X, Y) >= Y because [79], by (Select) 79] Y >= Y by (Meta) 80] pow(F, 0) >= ~L1(/\x.x) because [3], by (Star) 81] pow(F, s(X)) >= op(F, pow(F, X)) because [10], by (Star) 82] @_{o -> o}(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [83], by (Star) 83] @_{o -> o}*(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [84], by (Select) 84] op(F, G) @_{o -> o}*(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [85] 85] op*(F, G, @_{o -> o}*(op(F, G), X)) >= ~AP1(F, ~AP1(G, X)) because op > ~AP1, [25] and [27], by (Copy) 86] ~L1(/\x.~AP1(F, x)) >= F because [35], by (Star) 87] ~L1(/\x.@_{o -> o}(op(F, G), x)) >= op(F, G) because [88], by (Star) 88] ~L1*(/\x.@_{o -> o}(op(F, G), x)) >= op(F, G) because [89], by (Select) 89] /\x.@_{o -> o}(op(F, G), x) >= op(F, G) because [44], by (Eta)[Kop13:2] 90] ~L1(/\x.@_{o -> o}(pow(F, X), x)) >= pow(F, X) because [52], by (Star) 91] ~AP1(F, X) >= @_{o -> o}(F, X) because [92], by (Star) 92] ~AP1*(F, X) >= @_{o -> o}(F, X) because ~AP1 > @_{o -> o}, [93] and [94], by (Copy) 93] ~AP1*(F, X) >= F because [61], by (Select) 94] ~AP1*(F, X) >= X because [62], by (Select) 95] ~L1(F) >= F because [65], by (Star) 96] ~AP1(F, X) >= #argfun-~AP1##(@_{o -> o}(F, X)) because [97], by (Star) 97] ~AP1*(F, X) >= #argfun-~AP1##(@_{o -> o}(F, X)) because ~AP1 > #argfun-~AP1## and [98], by (Copy) 98] ~AP1*(F, X) >= @_{o -> o}(F, X) because ~AP1 > @_{o -> o}, [99] and [101], by (Copy) 99] ~AP1*(F, X) >= F because [100], by (Select) 100] F >= F by (Meta) 101] ~AP1*(F, X) >= X because [102], by (Select) 102] 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_5, R_0, minimal, all) by (P_6, R_0, minimal, all), where P_6 consists of: pow(F, 0) X =#> ~L1(/\x.x) X pow(F, s(X)) Y =#> op(F, pow(F, X)) Y op(F, G) X =#> ~AP1#(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) X =#> F(X) ~L1(/\x.pow(F, X) x) Y =#> pow(F, X) Y ~AP1#(F, X) =#> F(X) ~L1(F) X =#> F(X) Thus, the original system is terminating if each of (P_4, R_0, minimal, all) and (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: pow(F, 0) X >? ~L1(/\x.x) X pow(F, s(X)) Y >? op(F, pow(F, X)) Y op(F, G) X >? ~AP1#(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) X >? F(X) ~L1(/\x.pow(F, X) x) Y >? pow(F, X) Y ~AP1#(F, X) >? F(X) ~L1(F) X >? F(X) map(F, nil) >= nil map(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) pow(F, 0) >= ~L1(/\x.x) pow(F, s(X)) >= op(F, pow(F, X)) op(F, G) X >= ~AP1(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) >= F ~L1(/\x.op(F, G) x) >= op(F, G) ~L1(/\x.pow(F, X) x) >= pow(F, X) ~AP1(F, X) >= F X ~L1(F) >= F ~AP1(F, X) >= ~AP1#(F, X) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( ~AP1#(F, X) ) = #argfun-~AP1##(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: [[nil]] = _|_ We choose Lex = {} and Mul = {#argfun-~AP1##, 0, @_{o -> o}, cons, map, op, pow, s, ~AP1, ~AP1#, ~L1}, and the following precedence: 0 > pow > op > s > map = ~AP1 > cons > #argfun-~AP1## > ~AP1# > ~L1 > @_{o -> o} Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: @_{o -> o}(pow(F, 0), X) >= @_{o -> o}(~L1(/\x.x), X) @_{o -> o}(pow(F, s(X)), Y) >= @_{o -> o}(op(F, pow(F, X)), Y) @_{o -> o}(op(F, G), X) >= #argfun-~AP1##(@_{o -> o}(F, ~AP1(G, X))) @_{o -> o}(~L1(/\x.~AP1(F, x)), X) >= @_{o -> o}(F, X) @_{o -> o}(~L1(/\x.@_{o -> o}(pow(F, X), x)), Y) >= @_{o -> o}(pow(F, X), Y) #argfun-~AP1##(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) @_{o -> o}(~L1(F), X) > @_{o -> o}(F, X) map(F, _|_) >= _|_ map(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) pow(F, 0) >= ~L1(/\x.x) pow(F, s(X)) >= op(F, pow(F, X)) @_{o -> o}(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) >= F ~L1(/\x.@_{o -> o}(op(F, G), x)) >= op(F, G) ~L1(/\x.@_{o -> o}(pow(F, X), x)) >= pow(F, X) ~AP1(F, X) >= @_{o -> o}(F, X) ~L1(F) >= F ~AP1(F, X) >= #argfun-~AP1##(@_{o -> o}(F, X)) With these choices, we have: 1] @_{o -> o}(pow(F, 0), X) >= @_{o -> o}(~L1(/\x.x), X) because @_{o -> o} in Mul, [2] and [7], by (Fun) 2] pow(F, 0) >= ~L1(/\x.x) because [3], by (Star) 3] pow*(F, 0) >= ~L1(/\x.x) because pow > ~L1 and [4], by (Copy) 4] pow*(F, 0) >= /\y.y because [5], by (F-Abs) 5] pow*(F, 0, x) >= x because [6], by (Select) 6] x >= x by (Var) 7] X >= X by (Meta) 8] @_{o -> o}(pow(F, s(X)), Y) >= @_{o -> o}(op(F, pow(F, X)), Y) because @_{o -> o} in Mul, [9] and [18], by (Fun) 9] pow(F, s(X)) >= op(F, pow(F, X)) because [10], by (Star) 10] pow*(F, s(X)) >= op(F, pow(F, X)) because pow > op, [11] and [13], by (Copy) 11] pow*(F, s(X)) >= F because [12], by (Select) 12] F >= F by (Meta) 13] pow*(F, s(X)) >= pow(F, X) because pow in Mul, [14] and [15], by (Stat) 14] F >= F by (Meta) 15] s(X) > X because [16], by definition 16] s*(X) >= X because [17], by (Select) 17] X >= X by (Meta) 18] Y >= Y by (Meta) 19] @_{o -> o}(op(F, G), X) >= #argfun-~AP1##(@_{o -> o}(F, ~AP1(G, X))) because [20], by (Star) 20] @_{o -> o}*(op(F, G), X) >= #argfun-~AP1##(@_{o -> o}(F, ~AP1(G, X))) because [21], by (Select) 21] op(F, G) @_{o -> o}*(op(F, G), X) >= #argfun-~AP1##(@_{o -> o}(F, ~AP1(G, X))) because [22] 22] op*(F, G, @_{o -> o}*(op(F, G), X)) >= #argfun-~AP1##(@_{o -> o}(F, ~AP1(G, X))) because op > #argfun-~AP1## and [23], by (Copy) 23] op*(F, G, @_{o -> o}*(op(F, G), X)) >= @_{o -> o}(F, ~AP1(G, X)) because op > @_{o -> o}, [24] and [26], by (Copy) 24] op*(F, G, @_{o -> o}*(op(F, G), X)) >= F because [25], by (Select) 25] F >= F by (Meta) 26] op*(F, G, @_{o -> o}*(op(F, G), X)) >= ~AP1(G, X) because op > ~AP1, [27] and [29], by (Copy) 27] op*(F, G, @_{o -> o}*(op(F, G), X)) >= G because [28], by (Select) 28] G >= G by (Meta) 29] op*(F, G, @_{o -> o}*(op(F, G), X)) >= X because [30], by (Select) 30] @_{o -> o}*(op(F, G), X) >= X because [31], by (Select) 31] X >= X by (Meta) 32] @_{o -> o}(~L1(/\x.~AP1(F, x)), X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [33] and [37], by (Fun) 33] ~L1(/\x.~AP1(F, x)) >= F because [34], by (Star) 34] ~L1*(/\x.~AP1(F, x)) >= F because [35], by (Select) 35] /\x.~AP1(F, x) >= F because [36], by (Eta)[Kop13:2] 36] F >= F by (Meta) 37] X >= X by (Meta) 38] @_{o -> o}(~L1(/\x.@_{o -> o}(pow(F, X), x)), Y) >= @_{o -> o}(pow(F, X), Y) because @_{o -> o} in Mul, [39] and [45], by (Fun) 39] ~L1(/\x.@_{o -> o}(pow(F, X), x)) >= pow(F, X) because [40], by (Star) 40] ~L1*(/\x.@_{o -> o}(pow(F, X), x)) >= pow(F, X) because [41], by (Select) 41] /\x.@_{o -> o}(pow(F, X), x) >= pow(F, X) because [42], by (Eta)[Kop13:2] 42] pow(F, X) >= pow(F, X) because pow in Mul, [43] and [44], by (Fun) 43] F >= F by (Meta) 44] X >= X by (Meta) 45] Y >= Y by (Meta) 46] #argfun-~AP1##(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) because [47], by (Star) 47] #argfun-~AP1##*(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) because [48], by (Select) 48] @_{o -> o}(F, X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [49] and [50], by (Fun) 49] F >= F by (Meta) 50] X >= X by (Meta) 51] @_{o -> o}(~L1(F), X) > @_{o -> o}(F, X) because [52], by definition 52] @_{o -> o}*(~L1(F), X) >= @_{o -> o}(F, X) because [53], by (Select) 53] ~L1(F) @_{o -> o}*(~L1(F), X) >= @_{o -> o}(F, X) because [54] 54] ~L1*(F, @_{o -> o}*(~L1(F), X)) >= @_{o -> o}(F, X) because ~L1 > @_{o -> o}, [55] and [57], by (Copy) 55] ~L1*(F, @_{o -> o}*(~L1(F), X)) >= F because [56], by (Select) 56] F >= F by (Meta) 57] ~L1*(F, @_{o -> o}*(~L1(F), X)) >= X because [58], by (Select) 58] @_{o -> o}*(~L1(F), X) >= X because [59], by (Select) 59] X >= X by (Meta) 60] map(F, _|_) >= _|_ by (Bot) 61] map(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) because [62], by (Star) 62] map*(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) because map > cons, [63] and [68], by (Copy) 63] map*(F, cons(X, Y)) >= ~AP1(F, X) because map = ~AP1, map in Mul, [64] and [65], by (Stat) 64] F >= F by (Meta) 65] cons(X, Y) > X because [66], by definition 66] cons*(X, Y) >= X because [67], by (Select) 67] X >= X by (Meta) 68] map*(F, cons(X, Y)) >= map(F, Y) because map in Mul, [64] and [69], by (Stat) 69] cons(X, Y) > Y because [70], by definition 70] cons*(X, Y) >= Y because [71], by (Select) 71] Y >= Y by (Meta) 72] pow(F, 0) >= ~L1(/\x.x) because [3], by (Star) 73] pow(F, s(X)) >= op(F, pow(F, X)) because [10], by (Star) 74] @_{o -> o}(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [75], by (Star) 75] @_{o -> o}*(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [76], by (Select) 76] op(F, G) @_{o -> o}*(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [77] 77] op*(F, G, @_{o -> o}*(op(F, G), X)) >= ~AP1(F, ~AP1(G, X)) because op > ~AP1, [24] and [26], by (Copy) 78] ~L1(/\x.~AP1(F, x)) >= F because [34], by (Star) 79] ~L1(/\x.@_{o -> o}(op(F, G), x)) >= op(F, G) because [80], by (Star) 80] ~L1*(/\x.@_{o -> o}(op(F, G), x)) >= op(F, G) because [81], by (Select) 81] /\x.@_{o -> o}(op(F, G), x) >= op(F, G) because [82], by (Eta)[Kop13:2] 82] op(F, G) >= op(F, G) because op in Mul, [83] and [84], by (Fun) 83] F >= F by (Meta) 84] G >= G by (Meta) 85] ~L1(/\x.@_{o -> o}(pow(F, X), x)) >= pow(F, X) because [40], by (Star) 86] ~AP1(F, X) >= @_{o -> o}(F, X) because [87], by (Star) 87] ~AP1*(F, X) >= @_{o -> o}(F, X) because ~AP1 > @_{o -> o}, [88] and [89], by (Copy) 88] ~AP1*(F, X) >= F because [49], by (Select) 89] ~AP1*(F, X) >= X because [50], by (Select) 90] ~L1(F) >= F because [91], by (Star) 91] ~L1*(F) >= F because [56], by (Select) 92] ~AP1(F, X) >= #argfun-~AP1##(@_{o -> o}(F, X)) because [93], by (Star) 93] ~AP1*(F, X) >= #argfun-~AP1##(@_{o -> o}(F, X)) because ~AP1 > #argfun-~AP1## and [94], by (Copy) 94] ~AP1*(F, X) >= @_{o -> o}(F, X) because ~AP1 > @_{o -> o}, [95] and [97], by (Copy) 95] ~AP1*(F, X) >= F because [96], by (Select) 96] F >= F by (Meta) 97] ~AP1*(F, X) >= X because [98], by (Select) 98] 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_6, R_0, minimal, all) by (P_7, R_0, minimal, all), where P_7 consists of: pow(F, 0) X =#> ~L1(/\x.x) X pow(F, s(X)) Y =#> op(F, pow(F, X)) Y op(F, G) X =#> ~AP1#(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) X =#> F(X) ~L1(/\x.pow(F, X) x) Y =#> pow(F, X) Y ~AP1#(F, X) =#> F(X) Thus, the original system is terminating if each of (P_4, R_0, minimal, all) and (P_7, R_0, minimal, all) is finite. We consider the dependency pair problem (P_7, 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 : 2 * 2 : 5 * 3 : 0, 1, 2, 3, 4, 5 * 4 : 0, 1 * 5 : 0, 1, 2, 3, 4, 5 This graph has the following strongly connected components: P_8: pow(F, s(X)) Y =#> op(F, pow(F, X)) Y op(F, G) X =#> ~AP1#(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) X =#> F(X) ~L1(/\x.pow(F, X) x) Y =#> pow(F, X) Y ~AP1#(F, X) =#> F(X) By [Kop12, Thm. 7.31], we may replace any dependency pair problem (P_7, R_0, m, f) by (P_8, R_0, m, f). Thus, the original system is terminating if each of (P_4, R_0, minimal, all) and (P_8, R_0, minimal, all) is finite. We consider the dependency pair problem (P_8, 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: pow(F, s(X)) Y >? op(F, pow(F, X)) Y op(F, G) X >? ~AP1#(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) X >? F(X) ~L1(/\x.pow(F, X) x) Y >? pow(F, X) Y ~AP1#(F, X) >? F(X) map(F, nil) >= nil map(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) pow(F, 0) >= ~L1(/\x.x) pow(F, s(X)) >= op(F, pow(F, X)) op(F, G) X >= ~AP1(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) >= F ~L1(/\x.op(F, G) x) >= op(F, G) ~L1(/\x.pow(F, X) x) >= pow(F, X) ~AP1(F, X) >= F X ~L1(F) >= F ~AP1(F, X) >= ~AP1#(F, X) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( ~AP1#(F, X) ) = #argfun-~AP1##(F X) Since this representation is not advantageous for the higher-order recursive path ordering, we present the strict requirements in their unextended form, which is not problematic since for any F, s and substituion gamma: (F s)gamma beta-reduces to F(s)gamma.) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[#argfun-~AP1##(x_1)]] = x_1 [[nil]] = _|_ We choose Lex = {@_{o -> o}, ~AP1} and Mul = {0, cons, map, op, pow, s, ~AP1#, ~L1}, and the following precedence: 0 > map > cons > pow > s > @_{o -> o} = ~AP1 > op > ~AP1# > ~L1 Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: @_{o -> o}(pow(F, s(X)), Y) > @_{o -> o}(op(F, pow(F, X)), Y) @_{o -> o}(op(F, G), X) >= @_{o -> o}(F, ~AP1(G, X)) @_{o -> o}(~L1(/\x.~AP1(F, x)), X) >= @_{o -> o}(F, X) @_{o -> o}(~L1(/\x.@_{o -> o}(pow(F, X), x)), Y) >= @_{o -> o}(pow(F, X), Y) @_{o -> o}(F, X) >= @_{o -> o}(F, X) map(F, _|_) >= _|_ map(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) pow(F, 0) >= ~L1(/\x.x) pow(F, s(X)) >= op(F, pow(F, X)) @_{o -> o}(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) >= F ~L1(/\x.@_{o -> o}(op(F, G), x)) >= op(F, G) ~L1(/\x.@_{o -> o}(pow(F, X), x)) >= pow(F, X) ~AP1(F, X) >= @_{o -> o}(F, X) ~L1(F) >= F ~AP1(F, X) >= @_{o -> o}(F, X) With these choices, we have: 1] @_{o -> o}(pow(F, s(X)), Y) > @_{o -> o}(op(F, pow(F, X)), Y) because [2], by definition 2] @_{o -> o}*(pow(F, s(X)), Y) >= @_{o -> o}(op(F, pow(F, X)), Y) because [3], [12] and [14], by (Stat) 3] pow(F, s(X)) > op(F, pow(F, X)) because [4], by definition 4] pow*(F, s(X)) >= op(F, pow(F, X)) because pow > op, [5] and [7], by (Copy) 5] pow*(F, s(X)) >= F because [6], by (Select) 6] F >= F by (Meta) 7] pow*(F, s(X)) >= pow(F, X) because pow in Mul, [8] and [9], by (Stat) 8] F >= F by (Meta) 9] s(X) > X because [10], by definition 10] s*(X) >= X because [11], by (Select) 11] X >= X by (Meta) 12] @_{o -> o}*(pow(F, s(X)), Y) >= op(F, pow(F, X)) because [13], by (Select) 13] pow(F, s(X)) >= op(F, pow(F, X)) because [4], by (Star) 14] @_{o -> o}*(pow(F, s(X)), Y) >= Y because [15], by (Select) 15] Y >= Y by (Meta) 16] @_{o -> o}(op(F, G), X) >= @_{o -> o}(F, ~AP1(G, X)) because [17], by (Star) 17] @_{o -> o}*(op(F, G), X) >= @_{o -> o}(F, ~AP1(G, X)) because [18], [21] and [23], by (Stat) 18] op(F, G) > F because [19], by definition 19] op*(F, G) >= F because [20], by (Select) 20] F >= F by (Meta) 21] @_{o -> o}*(op(F, G), X) >= F because [22], by (Select) 22] op(F, G) >= F because [19], by (Star) 23] @_{o -> o}*(op(F, G), X) >= ~AP1(G, X) because @_{o -> o} = ~AP1, [24], [27] and [29], by (Stat) 24] op(F, G) > G because [25], by definition 25] op*(F, G) >= G because [26], by (Select) 26] G >= G by (Meta) 27] @_{o -> o}*(op(F, G), X) >= G because [28], by (Select) 28] op(F, G) >= G because [25], by (Star) 29] @_{o -> o}*(op(F, G), X) >= X because [30], by (Select) 30] X >= X by (Meta) 31] @_{o -> o}(~L1(/\x.~AP1(F, x)), X) >= @_{o -> o}(F, X) because [32] and [36], by (Fun) 32] ~L1(/\x.~AP1(F, x)) >= F because [33], by (Star) 33] ~L1*(/\x.~AP1(F, x)) >= F because [34], by (Select) 34] /\x.~AP1(F, x) >= F because [35], by (Eta)[Kop13:2] 35] F >= F by (Meta) 36] X >= X by (Meta) 37] @_{o -> o}(~L1(/\x.@_{o -> o}(pow(F, X), x)), Y) >= @_{o -> o}(pow(F, X), Y) because [38] and [44], by (Fun) 38] ~L1(/\x.@_{o -> o}(pow(F, X), x)) >= pow(F, X) because [39], by (Star) 39] ~L1*(/\x.@_{o -> o}(pow(F, X), x)) >= pow(F, X) because [40], by (Select) 40] /\x.@_{o -> o}(pow(F, X), x) >= pow(F, X) because [41], by (Eta)[Kop13:2] 41] pow(F, X) >= pow(F, X) because pow in Mul, [42] and [43], by (Fun) 42] F >= F by (Meta) 43] X >= X by (Meta) 44] Y >= Y by (Meta) 45] @_{o -> o}(F, X) >= @_{o -> o}(F, X) because [46] and [47], by (Fun) 46] F >= F by (Meta) 47] X >= X by (Meta) 48] map(F, _|_) >= _|_ by (Bot) 49] map(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) because [50], by (Star) 50] map*(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) because map > cons, [51] and [58], by (Copy) 51] map*(F, cons(X, Y)) >= ~AP1(F, X) because map > ~AP1, [52] and [54], by (Copy) 52] map*(F, cons(X, Y)) >= F because [53], by (Select) 53] F >= F by (Meta) 54] map*(F, cons(X, Y)) >= X because [55], by (Select) 55] cons(X, Y) >= X because [56], by (Star) 56] cons*(X, Y) >= X because [57], by (Select) 57] X >= X by (Meta) 58] map*(F, cons(X, Y)) >= map(F, Y) because map in Mul, [59] and [60], by (Stat) 59] F >= F by (Meta) 60] cons(X, Y) > Y because [61], by definition 61] cons*(X, Y) >= Y because [62], by (Select) 62] Y >= Y by (Meta) 63] pow(F, 0) >= ~L1(/\x.x) because [64], by (Star) 64] pow*(F, 0) >= ~L1(/\x.x) because pow > ~L1 and [65], by (Copy) 65] pow*(F, 0) >= /\y.y because [66], by (F-Abs) 66] pow*(F, 0, x) >= x because [67], by (Select) 67] x >= x by (Var) 68] pow(F, s(X)) >= op(F, pow(F, X)) because [4], by (Star) 69] @_{o -> o}(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [70], by (Star) 70] @_{o -> o}*(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because @_{o -> o} = ~AP1, [18], [21] and [23], by (Stat) 71] ~L1(/\x.~AP1(F, x)) >= F because [33], by (Star) 72] ~L1(/\x.@_{o -> o}(op(F, G), x)) >= op(F, G) because [73], by (Star) 73] ~L1*(/\x.@_{o -> o}(op(F, G), x)) >= op(F, G) because [74], by (Select) 74] /\x.@_{o -> o}(op(F, G), x) >= op(F, G) because [75], by (Eta)[Kop13:2] 75] op(F, G) >= op(F, G) because op in Mul, [76] and [77], by (Fun) 76] F >= F by (Meta) 77] G >= G by (Meta) 78] ~L1(/\x.@_{o -> o}(pow(F, X), x)) >= pow(F, X) because [39], by (Star) 79] ~AP1(F, X) >= @_{o -> o}(F, X) because ~AP1 = @_{o -> o}, [46] and [47], by (Fun) 80] ~L1(F) >= F because [81], by (Star) 81] ~L1*(F) >= F because [82], by (Select) 82] F >= F by (Meta) 83] ~AP1(F, X) >= @_{o -> o}(F, X) because ~AP1 = @_{o -> o}, [84] and [85], by (Fun) 84] F >= F by (Meta) 85] 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_8, R_0, minimal, all) by (P_9, R_0, minimal, all), where P_9 consists of: op(F, G) X =#> ~AP1#(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) X =#> F(X) ~L1(/\x.pow(F, X) x) Y =#> pow(F, X) Y ~AP1#(F, X) =#> F(X) Thus, the original system is terminating if each of (P_4, R_0, minimal, all) and (P_9, R_0, minimal, all) is finite. We consider the dependency pair problem (P_9, 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 : 3 * 1 : 0, 1, 2, 3 * 2 : * 3 : 0, 1, 2, 3 This graph has the following strongly connected components: P_10: op(F, G) X =#> ~AP1#(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) X =#> F(X) ~AP1#(F, X) =#> F(X) By [Kop12, Thm. 7.31], we may replace any dependency pair problem (P_9, R_0, m, f) by (P_10, R_0, m, f). Thus, the original system is terminating if each of (P_4, R_0, minimal, all) and (P_10, R_0, minimal, all) is finite. We consider the dependency pair problem (P_10, 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: op(F, G) X >? ~AP1#(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) X >? F(X) ~AP1#(F, X) >? F(X) map(F, nil) >= nil map(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) pow(F, 0) >= ~L1(/\x.x) pow(F, s(X)) >= op(F, pow(F, X)) op(F, G) X >= ~AP1(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) >= F ~L1(/\x.op(F, G) x) >= op(F, G) ~L1(/\x.pow(F, X) x) >= pow(F, X) ~AP1(F, X) >= F X ~L1(F) >= F ~AP1(F, X) >= ~AP1#(F, X) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( ~AP1#(F, X) ) = #argfun-~AP1##(F X) Since this representation is not advantageous for the higher-order recursive path ordering, we present the strict requirements in their unextended form, which is not problematic since for any F, s and substituion gamma: (F s)gamma beta-reduces to F(s)gamma.) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[#argfun-~AP1##(x_1)]] = x_1 [[nil]] = _|_ We choose Lex = {} and Mul = {0, @_{o -> o}, cons, map, op, pow, s, ~AP1, ~AP1#, ~L1}, and the following precedence: 0 > map > cons > pow > op > s > ~AP1 > ~AP1# > ~L1 > @_{o -> o} Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: @_{o -> o}(op(F, G), X) >= @_{o -> o}(F, ~AP1(G, X)) @_{o -> o}(~L1(/\x.~AP1(F, x)), X) > @_{o -> o}(F, X) @_{o -> o}(F, X) >= @_{o -> o}(F, X) map(F, _|_) >= _|_ map(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) pow(F, 0) >= ~L1(/\x.x) pow(F, s(X)) >= op(F, pow(F, X)) @_{o -> o}(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) >= F ~L1(/\x.@_{o -> o}(op(F, G), x)) >= op(F, G) ~L1(/\x.@_{o -> o}(pow(F, X), x)) >= pow(F, X) ~AP1(F, X) >= @_{o -> o}(F, X) ~L1(F) >= F ~AP1(F, X) >= @_{o -> o}(F, X) With these choices, we have: 1] @_{o -> o}(op(F, G), X) >= @_{o -> o}(F, ~AP1(G, X)) because [2], by (Star) 2] @_{o -> o}*(op(F, G), X) >= @_{o -> o}(F, ~AP1(G, X)) because [3], by (Select) 3] op(F, G) @_{o -> o}*(op(F, G), X) >= @_{o -> o}(F, ~AP1(G, X)) because [4] 4] op*(F, G, @_{o -> o}*(op(F, G), X)) >= @_{o -> o}(F, ~AP1(G, X)) because op > @_{o -> o}, [5] and [7], by (Copy) 5] op*(F, G, @_{o -> o}*(op(F, G), X)) >= F because [6], by (Select) 6] F >= F by (Meta) 7] op*(F, G, @_{o -> o}*(op(F, G), X)) >= ~AP1(G, X) because op > ~AP1, [8] and [10], by (Copy) 8] op*(F, G, @_{o -> o}*(op(F, G), X)) >= G because [9], by (Select) 9] G >= G by (Meta) 10] op*(F, G, @_{o -> o}*(op(F, G), X)) >= X because [11], by (Select) 11] @_{o -> o}*(op(F, G), X) >= X because [12], by (Select) 12] X >= X by (Meta) 13] @_{o -> o}(~L1(/\x.~AP1(F, x)), X) > @_{o -> o}(F, X) because [14], by definition 14] @_{o -> o}*(~L1(/\x.~AP1(F, x)), X) >= @_{o -> o}(F, X) because [15], by (Select) 15] ~L1(/\x.~AP1(F, x)) @_{o -> o}*(~L1(/\y.~AP1(F, y)), X) >= @_{o -> o}(F, X) because [16] 16] ~L1*(/\x.~AP1(F, x), @_{o -> o}*(~L1(/\y.~AP1(F, y)), X)) >= @_{o -> o}(F, X) because ~L1 > @_{o -> o}, [17] and [20], by (Copy) 17] ~L1*(/\x.~AP1(F, x), @_{o -> o}*(~L1(/\y.~AP1(F, y)), X)) >= F because [18], by (Select) 18] /\x.~AP1(F, x) >= F because [19], by (Eta)[Kop13:2] 19] F >= F by (Meta) 20] ~L1*(/\x.~AP1(F, x), @_{o -> o}*(~L1(/\y.~AP1(F, y)), X)) >= X because [21], by (Select) 21] ~AP1(F, ~L1*(/\x.~AP1(F, x), @_{o -> o}*(~L1(/\y.~AP1(F, y)), X))) >= X because [22], by (Star) 22] ~AP1*(F, ~L1*(/\x.~AP1(F, x), @_{o -> o}*(~L1(/\y.~AP1(F, y)), X))) >= X because [23], by (Select) 23] ~L1*(/\x.~AP1(F, x), @_{o -> o}*(~L1(/\y.~AP1(F, y)), X)) >= X because [24], by (Select) 24] @_{o -> o}*(~L1(/\x.~AP1(F, x)), X) >= X because [25], by (Select) 25] X >= X by (Meta) 26] @_{o -> o}(F, X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [27] and [28], by (Fun) 27] F >= F by (Meta) 28] X >= X by (Meta) 29] map(F, _|_) >= _|_ by (Bot) 30] map(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) because [31], by (Star) 31] map*(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) because map > cons, [32] and [39], by (Copy) 32] map*(F, cons(X, Y)) >= ~AP1(F, X) because map > ~AP1, [33] and [35], by (Copy) 33] map*(F, cons(X, Y)) >= F because [34], by (Select) 34] F >= F by (Meta) 35] map*(F, cons(X, Y)) >= X because [36], by (Select) 36] cons(X, Y) >= X because [37], by (Star) 37] cons*(X, Y) >= X because [38], by (Select) 38] X >= X by (Meta) 39] map*(F, cons(X, Y)) >= map(F, Y) because map in Mul, [40] and [41], by (Stat) 40] F >= F by (Meta) 41] cons(X, Y) > Y because [42], by definition 42] cons*(X, Y) >= Y because [43], by (Select) 43] Y >= Y by (Meta) 44] pow(F, 0) >= ~L1(/\x.x) because [45], by (Star) 45] pow*(F, 0) >= ~L1(/\x.x) because pow > ~L1 and [46], by (Copy) 46] pow*(F, 0) >= /\y.y because [47], by (F-Abs) 47] pow*(F, 0, x) >= x because [48], by (Select) 48] x >= x by (Var) 49] pow(F, s(X)) >= op(F, pow(F, X)) because [50], by (Star) 50] pow*(F, s(X)) >= op(F, pow(F, X)) because pow > op, [51] and [53], by (Copy) 51] pow*(F, s(X)) >= F because [52], by (Select) 52] F >= F by (Meta) 53] pow*(F, s(X)) >= pow(F, X) because pow in Mul, [54] and [55], by (Stat) 54] F >= F by (Meta) 55] s(X) > X because [56], by definition 56] s*(X) >= X because [57], by (Select) 57] X >= X by (Meta) 58] @_{o -> o}(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [59], by (Star) 59] @_{o -> o}*(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [60], by (Select) 60] op(F, G) @_{o -> o}*(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [61] 61] op*(F, G, @_{o -> o}*(op(F, G), X)) >= ~AP1(F, ~AP1(G, X)) because op > ~AP1, [5] and [7], by (Copy) 62] ~L1(/\x.~AP1(F, x)) >= F because [63], by (Star) 63] ~L1*(/\x.~AP1(F, x)) >= F because [18], by (Select) 64] ~L1(/\x.@_{o -> o}(op(F, G), x)) >= op(F, G) because [65], by (Star) 65] ~L1*(/\x.@_{o -> o}(op(F, G), x)) >= op(F, G) because [66], by (Select) 66] /\x.@_{o -> o}(op(F, G), x) >= op(F, G) because [67], by (Eta)[Kop13:2] 67] op(F, G) >= op(F, G) because op in Mul, [68] and [69], by (Fun) 68] F >= F by (Meta) 69] G >= G by (Meta) 70] ~L1(/\x.@_{o -> o}(pow(F, X), x)) >= pow(F, X) because [71], by (Star) 71] ~L1*(/\x.@_{o -> o}(pow(F, X), x)) >= pow(F, X) because [72], by (Select) 72] /\x.@_{o -> o}(pow(F, X), x) >= pow(F, X) because [73], by (Eta)[Kop13:2] 73] pow(F, X) >= pow(F, X) because pow in Mul, [74] and [75], by (Fun) 74] F >= F by (Meta) 75] X >= X by (Meta) 76] ~AP1(F, X) >= @_{o -> o}(F, X) because [77], by (Star) 77] ~AP1*(F, X) >= @_{o -> o}(F, X) because ~AP1 > @_{o -> o}, [78] and [79], by (Copy) 78] ~AP1*(F, X) >= F because [27], by (Select) 79] ~AP1*(F, X) >= X because [28], by (Select) 80] ~L1(F) >= F because [81], by (Star) 81] ~L1*(F) >= F because [82], by (Select) 82] F >= F by (Meta) 83] ~AP1(F, X) >= @_{o -> o}(F, X) because [84], by (Star) 84] ~AP1*(F, X) >= @_{o -> o}(F, X) because ~AP1 > @_{o -> o}, [85] and [87], by (Copy) 85] ~AP1*(F, X) >= F because [86], by (Select) 86] F >= F by (Meta) 87] ~AP1*(F, X) >= X because [88], by (Select) 88] 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_10, R_0, minimal, all) by (P_11, R_0, minimal, all), where P_11 consists of: op(F, G) X =#> ~AP1#(F, ~AP1(G, X)) ~AP1#(F, X) =#> F(X) Thus, the original system is terminating if each of (P_4, R_0, minimal, all) and (P_11, R_0, minimal, all) is finite. We consider the dependency pair problem (P_11, 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: op(F, G) X >? ~AP1#(F, ~AP1(G, X)) ~AP1#(F, X) >? F(X) map(F, nil) >= nil map(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) pow(F, 0) >= ~L1(/\x.x) pow(F, s(X)) >= op(F, pow(F, X)) op(F, G) X >= ~AP1(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) >= F ~L1(/\x.op(F, G) x) >= op(F, G) ~L1(/\x.pow(F, X) x) >= pow(F, X) ~AP1(F, X) >= F X ~L1(F) >= F ~AP1(F, X) >= ~AP1#(F, X) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( ~AP1#(F, X) ) = #argfun-~AP1##(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: [[nil]] = _|_ [[~L1(x_1)]] = x_1 We choose Lex = {} and Mul = {#argfun-~AP1##, 0, @_{o -> o}, cons, map, op, pow, s, ~AP1, ~AP1#}, and the following precedence: 0 > pow > op > s > map = ~AP1 > cons > @_{o -> o} > #argfun-~AP1## > ~AP1# Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: @_{o -> o}(op(F, G), X) >= #argfun-~AP1##(@_{o -> o}(F, ~AP1(G, X))) #argfun-~AP1##(@_{o -> o}(F, X)) > @_{o -> o}(F, X) map(F, _|_) >= _|_ map(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) pow(F, 0) >= /\x.x pow(F, s(X)) >= op(F, pow(F, X)) @_{o -> o}(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) /\x.~AP1(F, x) >= F /\x.@_{o -> o}(op(F, G), x) >= op(F, G) /\x.@_{o -> o}(pow(F, X), x) >= pow(F, X) ~AP1(F, X) >= @_{o -> o}(F, X) F >= F ~AP1(F, X) >= #argfun-~AP1##(@_{o -> o}(F, X)) With these choices, we have: 1] @_{o -> o}(op(F, G), X) >= #argfun-~AP1##(@_{o -> o}(F, ~AP1(G, X))) because [2], by (Star) 2] @_{o -> o}*(op(F, G), X) >= #argfun-~AP1##(@_{o -> o}(F, ~AP1(G, X))) because [3], by (Select) 3] op(F, G) @_{o -> o}*(op(F, G), X) >= #argfun-~AP1##(@_{o -> o}(F, ~AP1(G, X))) because [4] 4] op*(F, G, @_{o -> o}*(op(F, G), X)) >= #argfun-~AP1##(@_{o -> o}(F, ~AP1(G, X))) because op > #argfun-~AP1## and [5], by (Copy) 5] op*(F, G, @_{o -> o}*(op(F, G), X)) >= @_{o -> o}(F, ~AP1(G, X)) because op > @_{o -> o}, [6] and [8], by (Copy) 6] op*(F, G, @_{o -> o}*(op(F, G), X)) >= F because [7], by (Select) 7] F >= F by (Meta) 8] op*(F, G, @_{o -> o}*(op(F, G), X)) >= ~AP1(G, X) because op > ~AP1, [9] and [11], by (Copy) 9] op*(F, G, @_{o -> o}*(op(F, G), X)) >= G because [10], by (Select) 10] G >= G by (Meta) 11] op*(F, G, @_{o -> o}*(op(F, G), X)) >= X because [12], by (Select) 12] @_{o -> o}*(op(F, G), X) >= X because [13], by (Select) 13] X >= X by (Meta) 14] #argfun-~AP1##(@_{o -> o}(F, X)) > @_{o -> o}(F, X) because [15], by definition 15] #argfun-~AP1##*(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) because [16], by (Select) 16] @_{o -> o}(F, X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [17] and [18], by (Fun) 17] F >= F by (Meta) 18] X >= X by (Meta) 19] map(F, _|_) >= _|_ by (Bot) 20] map(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) because [21], by (Star) 21] map*(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) because map > cons, [22] and [27], by (Copy) 22] map*(F, cons(X, Y)) >= ~AP1(F, X) because map = ~AP1, map in Mul, [23] and [24], by (Stat) 23] F >= F by (Meta) 24] cons(X, Y) > X because [25], by definition 25] cons*(X, Y) >= X because [26], by (Select) 26] X >= X by (Meta) 27] map*(F, cons(X, Y)) >= map(F, Y) because map in Mul, [23] and [28], by (Stat) 28] cons(X, Y) > Y because [29], by definition 29] cons*(X, Y) >= Y because [30], by (Select) 30] Y >= Y by (Meta) 31] pow(F, 0) >= /\x.x because [32], by (Star) 32] pow*(F, 0) >= /\y.y because [33], by (F-Abs) 33] pow*(F, 0, x) >= x because [34], by (Select) 34] x >= x by (Var) 35] pow(F, s(X)) >= op(F, pow(F, X)) because [36], by (Star) 36] pow*(F, s(X)) >= op(F, pow(F, X)) because pow > op, [37] and [39], by (Copy) 37] pow*(F, s(X)) >= F because [38], by (Select) 38] F >= F by (Meta) 39] pow*(F, s(X)) >= pow(F, X) because pow in Mul, [40] and [41], by (Stat) 40] F >= F by (Meta) 41] s(X) > X because [42], by definition 42] s*(X) >= X because [43], by (Select) 43] X >= X by (Meta) 44] @_{o -> o}(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [45], by (Star) 45] @_{o -> o}*(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [46], by (Select) 46] op(F, G) @_{o -> o}*(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [47] 47] op*(F, G, @_{o -> o}*(op(F, G), X)) >= ~AP1(F, ~AP1(G, X)) because op > ~AP1, [6] and [8], by (Copy) 48] /\x.~AP1(F, x) >= F because [49], by (Eta)[Kop13:2] 49] F >= F by (Meta) 50] /\x.@_{o -> o}(op(F, G), x) >= op(F, G) because [51], by (Eta)[Kop13:2] 51] op(F, G) >= op(F, G) because op in Mul, [52] and [53], by (Fun) 52] F >= F by (Meta) 53] G >= G by (Meta) 54] /\x.@_{o -> o}(pow(F, X), x) >= pow(F, X) because [55], by (Eta)[Kop13:2] 55] pow(F, X) >= pow(F, X) because pow in Mul, [56] and [57], by (Fun) 56] F >= F by (Meta) 57] X >= X by (Meta) 58] ~AP1(F, X) >= @_{o -> o}(F, X) because [59], by (Star) 59] ~AP1*(F, X) >= @_{o -> o}(F, X) because ~AP1 > @_{o -> o}, [60] and [61], by (Copy) 60] ~AP1*(F, X) >= F because [17], by (Select) 61] ~AP1*(F, X) >= X because [18], by (Select) 62] F >= F by (Meta) 63] ~AP1(F, X) >= #argfun-~AP1##(@_{o -> o}(F, X)) because [64], by (Star) 64] ~AP1*(F, X) >= #argfun-~AP1##(@_{o -> o}(F, X)) because ~AP1 > #argfun-~AP1## and [65], by (Copy) 65] ~AP1*(F, X) >= @_{o -> o}(F, X) because ~AP1 > @_{o -> o}, [66] and [68], by (Copy) 66] ~AP1*(F, X) >= F because [67], by (Select) 67] F >= F by (Meta) 68] ~AP1*(F, X) >= X because [69], by (Select) 69] 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_11, R_0, minimal, all) by (P_12, R_0, minimal, all), where P_12 consists of: op(F, G) X =#> ~AP1#(F, ~AP1(G, X)) Thus, the original system is terminating if each of (P_4, R_0, minimal, all) and (P_12, R_0, minimal, all) is finite. We consider the dependency pair problem (P_12, 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 : This graph has no strongly connected components. By [Kop12, Thm. 7.31], this implies finiteness of the dependency pair problem. Thus, the original system is terminating if (P_4, R_0, minimal, all) is finite. We consider the dependency pair problem (P_4, R_0, minimal, all). We apply the subterm criterion with the following projection function: nu(map#) = 2 Thus, we can orient the dependency pairs as follows: nu(map#(F, cons(X, Y))) = cons(X, Y) |> Y = nu(map#(F, Y)) By [Kop12, Thm. 7.35], we may replace a dependency pair problem (P_4, R_0, minimal, f) by ({}, R_0, minimal, f). By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed. As all dependency pair problems were succesfully simplified with sound (and complete) processors until nothing remained, we conclude termination. +++ Citations +++ [Kop11] C. Kop. Simplifying Algebraic Functional Systems. In Proceedings of CAI 2011, volume 6742 of LNCS. 201--215, Springer, 2011. [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.