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) ~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] ~AP1#(F, X) =#> F(X) 13] ~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) ~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 : 12 * 1 : 0, 1 * 2 : 13 * 3 : * 4 : 7, 8 * 5 : * 6 : 3, 5, 6 * 7 : 12 * 8 : 12 * 9 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13 * 10 : 7, 8 * 11 : * 12 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13 * 13 : 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13 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 ~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 [FuhKop19, Thm. 61], 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 ~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) ~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]. Argument functions: [[~L1(x_1)]] = x_1 We choose Lex = {} and Mul = {#argfun-~AP1##, 0, @_{o -> o}, cons, map, map#, nil, op, pow, s, ~AP1, ~AP1#}, and the following precedence: pow > 0 > s > map > op > ~AP1 > @_{o -> o} = map# > nil > ~AP1# > #argfun-~AP1## > cons Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: map#(F, cons(X, Y)) > #argfun-~AP1##(@_{o -> o}(F, X)) map#(F, cons(X, Y)) >= map#(F, Y) @_{o -> o}(pow(F, 0), X) >= @_{o -> o}(/\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}(op(F, G), X) >= #argfun-~AP1##(@_{o -> o}(G, X)) @_{o -> o}(/\x.~AP1(F, x), X) >= @_{o -> o}(F, X) @_{o -> o}(/\x.@_{o -> o}(op(F, G), x), X) >= @_{o -> o}(op(F, G), X) #argfun-~AP1##(@_{o -> o}(F, X)) > @_{o -> o}(F, X) @_{o -> o}(F, X) >= @_{o -> o}(F, X) map(F, nil) >= nil 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) ~AP1(F, X) >= @_{o -> o}(F, X) F >= F map(F, X) >= map#(F, X) ~AP1(F, X) >= #argfun-~AP1##(@_{o -> o}(F, X)) 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}, map# in Mul, [4] and [5], by (Stat) 4] F >= F by (Meta) 5] cons(X, Y) > X because [6], by definition 6] cons*(X, Y) >= X because [7], by (Select) 7] X >= X by (Meta) 8] map#(F, cons(X, Y)) >= map#(F, Y) because map# in Mul, [4] and [9], by (Fun) 9] cons(X, Y) >= Y because [10], by (Star) 10] cons*(X, Y) >= Y because [11], by (Select) 11] Y >= Y by (Meta) 12] @_{o -> o}(pow(F, 0), X) >= @_{o -> o}(/\x.x, X) because @_{o -> o} in Mul, [13] and [17], by (Fun) 13] pow(F, 0) >= /\x.x because [14], by (Star) 14] pow*(F, 0) >= /\y.y because [15], by (F-Abs) 15] pow*(F, 0, x) >= x because [16], by (Select) 16] x >= x by (Var) 17] X >= X by (Meta) 18] @_{o -> o}(pow(F, s(X)), Y) >= @_{o -> o}(op(F, pow(F, X)), Y) because @_{o -> o} in Mul, [19] and [28], by (Fun) 19] pow(F, s(X)) >= op(F, pow(F, X)) because [20], by (Star) 20] pow*(F, s(X)) >= op(F, pow(F, X)) because pow > op, [21] and [23], by (Copy) 21] pow*(F, s(X)) >= F because [22], by (Select) 22] F >= F by (Meta) 23] pow*(F, s(X)) >= pow(F, X) because pow in Mul, [24] and [25], by (Stat) 24] F >= F by (Meta) 25] s(X) > X because [26], by definition 26] s*(X) >= X because [27], by (Select) 27] X >= X by (Meta) 28] Y >= Y by (Meta) 29] @_{o -> o}(op(F, G), X) >= #argfun-~AP1##(@_{o -> o}(F, ~AP1(G, X))) because [30], by (Star) 30] @_{o -> o}*(op(F, G), X) >= #argfun-~AP1##(@_{o -> o}(F, ~AP1(G, X))) because [31], by (Select) 31] op(F, G) @_{o -> o}*(op(F, G), X) >= #argfun-~AP1##(@_{o -> o}(F, ~AP1(G, X))) because [32] 32] op*(F, G, @_{o -> o}*(op(F, G), X)) >= #argfun-~AP1##(@_{o -> o}(F, ~AP1(G, X))) because op > #argfun-~AP1## and [33], by (Copy) 33] op*(F, G, @_{o -> o}*(op(F, G), X)) >= @_{o -> o}(F, ~AP1(G, X)) because op > @_{o -> o}, [34] and [36], by (Copy) 34] op*(F, G, @_{o -> o}*(op(F, G), X)) >= F because [35], by (Select) 35] F >= F by (Meta) 36] op*(F, G, @_{o -> o}*(op(F, G), X)) >= ~AP1(G, X) because op > ~AP1, [37] and [39], by (Copy) 37] op*(F, G, @_{o -> o}*(op(F, G), X)) >= G because [38], by (Select) 38] G >= G by (Meta) 39] op*(F, G, @_{o -> o}*(op(F, G), X)) >= X because [40], by (Select) 40] @_{o -> o}*(op(F, G), X) >= X because [41], by (Select) 41] X >= X by (Meta) 42] @_{o -> o}(op(F, G), X) >= #argfun-~AP1##(@_{o -> o}(G, X)) because [43], by (Star) 43] @_{o -> o}*(op(F, G), X) >= #argfun-~AP1##(@_{o -> o}(G, X)) because @_{o -> o} > #argfun-~AP1## and [44], by (Copy) 44] @_{o -> o}*(op(F, G), X) >= @_{o -> o}(G, X) because [45], by (Select) 45] op(F, G) @_{o -> o}*(op(F, G), X) >= @_{o -> o}(G, X) because [46] 46] op*(F, G, @_{o -> o}*(op(F, G), X)) >= @_{o -> o}(G, X) because op > @_{o -> o}, [37] and [39], by (Copy) 47] @_{o -> o}(/\x.~AP1(F, x), X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [48] and [50], by (Fun) 48] /\x.~AP1(F, x) >= F because [49], by (Eta)[Kop13:2] 49] F >= F by (Meta) 50] X >= X by (Meta) 51] @_{o -> o}(/\x.@_{o -> o}(op(F, G), x), X) >= @_{o -> o}(op(F, G), X) because @_{o -> o} in Mul, [52] and [56], by (Fun) 52] /\x.@_{o -> o}(op(F, G), x) >= op(F, G) because [53], by (Eta)[Kop13:2] 53] op(F, G) >= op(F, G) because op in Mul, [54] and [55], by (Fun) 54] F >= F by (Meta) 55] G >= G by (Meta) 56] X >= X by (Meta) 57] #argfun-~AP1##(@_{o -> o}(F, X)) > @_{o -> o}(F, X) because [58], by definition 58] #argfun-~AP1##*(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) because [59], by (Select) 59] @_{o -> o}(F, X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [60] and [61], by (Fun) 60] F >= F by (Meta) 61] X >= X by (Meta) 62] @_{o -> o}(F, X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [63] and [64], by (Fun) 63] F >= F by (Meta) 64] X >= X by (Meta) 65] map(F, nil) >= nil because [66], by (Star) 66] map*(F, nil) >= nil because map > nil, by (Copy) 67] map(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) because [68], by (Star) 68] map*(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) because map > cons, [69] and [73], by (Copy) 69] map*(F, cons(X, Y)) >= ~AP1(F, X) because map > ~AP1, [70] and [71], by (Copy) 70] map*(F, cons(X, Y)) >= F because [4], by (Select) 71] map*(F, cons(X, Y)) >= X because [72], by (Select) 72] cons(X, Y) >= X because [6], by (Star) 73] map*(F, cons(X, Y)) >= map(F, Y) because map in Mul, [4] and [74], by (Stat) 74] cons(X, Y) > Y because [75], by definition 75] cons*(X, Y) >= Y because [11], by (Select) 76] pow(F, 0) >= /\x.x because [14], by (Star) 77] pow(F, s(X)) >= op(F, pow(F, X)) because [20], by (Star) 78] @_{o -> o}(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [79], by (Star) 79] @_{o -> o}*(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [80], by (Select) 80] op(F, G) @_{o -> o}*(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [81] 81] op*(F, G, @_{o -> o}*(op(F, G), X)) >= ~AP1(F, ~AP1(G, X)) because op > ~AP1, [34] and [36], by (Copy) 82] /\x.~AP1(F, x) >= F because [49], by (Eta)[Kop13:2] 83] /\x.@_{o -> o}(op(F, G), x) >= op(F, G) because [53], by (Eta)[Kop13:2] 84] ~AP1(F, X) >= @_{o -> o}(F, X) because [85], by (Star) 85] ~AP1*(F, X) >= @_{o -> o}(F, X) because ~AP1 > @_{o -> o}, [86] and [87], by (Copy) 86] ~AP1*(F, X) >= F because [60], by (Select) 87] ~AP1*(F, X) >= X because [61], by (Select) 88] F >= F by (Meta) 89] map(F, X) >= map#(F, X) because [90], by (Star) 90] map*(F, X) >= map#(F, X) because map > map#, [91] and [93], by (Copy) 91] map*(F, X) >= F because [92], by (Select) 92] F >= F by (Meta) 93] map*(F, X) >= X because [94], by (Select) 94] X >= X by (Meta) 95] ~AP1(F, X) >= #argfun-~AP1##(@_{o -> o}(F, X)) because [96], by (Star) 96] ~AP1*(F, X) >= #argfun-~AP1##(@_{o -> o}(F, X)) because ~AP1 > #argfun-~AP1## and [97], by (Copy) 97] ~AP1*(F, X) >= @_{o -> o}(F, X) because ~AP1 > @_{o -> o}, [98] and [100], by (Copy) 98] ~AP1*(F, X) >= F because [99], by (Select) 99] F >= F by (Meta) 100] ~AP1*(F, X) >= X because [101], by (Select) 101] 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)) 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(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 : 7 * 2 : 3, 4 * 3 : * 4 : * 5 : 0, 1, 2, 3, 4, 5, 6, 7 * 6 : 3, 4 * 7 : 0, 1, 2, 3, 4, 5, 6, 7 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 ~L1(/\x.~AP1(F, x)) 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 ~L1(/\x.~AP1(F, x)) 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) ~AP1(F, X) >= F X ~L1(F) >= F 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 = {0, @_{o -> o}, cons, map, op, pow, s, ~AP1, ~L1}, and the following precedence: pow > s > op > map = ~AP1 > 0 > cons > @_{o -> o} > ~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, 0), X) > @_{o -> o}(~L1(/\x.x), X) @_{o -> o}(~L1(/\x.~AP1(F, x)), 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) ~AP1(F, X) >= @_{o -> o}(F, X) ~L1(F) >= F With these choices, we have: 1] @_{o -> o}(pow(F, 0), X) > @_{o -> o}(~L1(/\x.x), X) because [2], by definition 2] @_{o -> o}*(pow(F, 0), X) >= @_{o -> o}(~L1(/\x.x), X) because [3], by (Select) 3] pow(F, 0) @_{o -> o}*(pow(F, 0), X) >= @_{o -> o}(~L1(/\x.x), X) because [4] 4] pow*(F, 0, @_{o -> o}*(pow(F, 0), X)) >= @_{o -> o}(~L1(/\x.x), X) because pow > @_{o -> o}, [5] and [9], by (Copy) 5] pow*(F, 0, @_{o -> o}*(pow(F, 0), X)) >= ~L1(/\x.x) because pow > ~L1 and [6], by (Copy) 6] pow*(F, 0, @_{o -> o}*(pow(F, 0), X)) >= /\y.y because [7], by (F-Abs) 7] pow*(F, 0, @_{o -> o}*(pow(F, 0), X), x) >= x because [8], by (Select) 8] x >= x by (Var) 9] pow*(F, 0, @_{o -> o}*(pow(F, 0), X)) >= X because [10], by (Select) 10] @_{o -> o}*(pow(F, 0), X) >= X because [11], by (Select) 11] X >= X by (Meta) 12] @_{o -> o}(~L1(/\x.~AP1(F, x)), X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [13] and [17], by (Fun) 13] ~L1(/\x.~AP1(F, x)) >= F because [14], by (Star) 14] ~L1*(/\x.~AP1(F, x)) >= F because [15], by (Select) 15] /\x.~AP1(F, x) >= F because [16], by (Eta)[Kop13:2] 16] F >= F by (Meta) 17] X >= X by (Meta) 18] @_{o -> o}(~L1(F), X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [19] and [22], by (Fun) 19] ~L1(F) >= F because [20], by (Star) 20] ~L1*(F) >= F because [21], by (Select) 21] F >= F by (Meta) 22] X >= X by (Meta) 23] map(F, _|_) >= _|_ by (Bot) 24] map(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) because [25], by (Star) 25] map*(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) because map > cons, [26] and [31], by (Copy) 26] map*(F, cons(X, Y)) >= ~AP1(F, X) because map = ~AP1, map in Mul, [27] and [28], by (Stat) 27] F >= F by (Meta) 28] cons(X, Y) > X because [29], by definition 29] cons*(X, Y) >= X because [30], by (Select) 30] X >= X by (Meta) 31] map*(F, cons(X, Y)) >= map(F, Y) because map in Mul, [27] and [32], by (Stat) 32] cons(X, Y) > Y because [33], by definition 33] cons*(X, Y) >= Y because [34], by (Select) 34] Y >= Y by (Meta) 35] pow(F, 0) >= ~L1(/\x.x) because [36], by (Star) 36] pow*(F, 0) >= ~L1(/\x.x) because pow > ~L1 and [37], by (Copy) 37] pow*(F, 0) >= /\y.y because [38], by (F-Abs) 38] pow*(F, 0, x) >= x because [39], by (Select) 39] x >= x by (Var) 40] pow(F, s(X)) >= op(F, pow(F, X)) because [41], by (Star) 41] pow*(F, s(X)) >= op(F, pow(F, X)) because pow > op, [42] and [44], by (Copy) 42] pow*(F, s(X)) >= F because [43], by (Select) 43] F >= F by (Meta) 44] pow*(F, s(X)) >= pow(F, X) because pow in Mul, [45] and [46], by (Stat) 45] F >= F by (Meta) 46] s(X) > X because [47], by definition 47] s*(X) >= X because [48], by (Select) 48] X >= X by (Meta) 49] @_{o -> o}(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [50], by (Star) 50] @_{o -> o}*(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [51], by (Select) 51] op(F, G) @_{o -> o}*(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [52] 52] op*(F, G, @_{o -> o}*(op(F, G), X)) >= ~AP1(F, ~AP1(G, X)) because op > ~AP1, [53] and [55], by (Copy) 53] op*(F, G, @_{o -> o}*(op(F, G), X)) >= F because [54], by (Select) 54] F >= F by (Meta) 55] op*(F, G, @_{o -> o}*(op(F, G), X)) >= ~AP1(G, X) because op > ~AP1, [56] and [58], by (Copy) 56] op*(F, G, @_{o -> o}*(op(F, G), X)) >= G because [57], by (Select) 57] G >= G by (Meta) 58] op*(F, G, @_{o -> o}*(op(F, G), X)) >= X because [59], by (Select) 59] @_{o -> o}*(op(F, G), X) >= X because [60], by (Select) 60] X >= X by (Meta) 61] ~L1(/\x.~AP1(F, x)) >= F because [14], by (Star) 62] ~L1(/\x.@_{o -> o}(op(F, G), x)) >= op(F, G) because [63], by (Star) 63] ~L1*(/\x.@_{o -> o}(op(F, G), x)) >= op(F, G) because [64], by (Select) 64] /\x.@_{o -> o}(op(F, G), x) >= op(F, G) because [65], by (Eta)[Kop13:2] 65] op(F, G) >= op(F, G) because op in Mul, [66] and [67], by (Fun) 66] F >= F by (Meta) 67] G >= G by (Meta) 68] ~AP1(F, X) >= @_{o -> o}(F, X) because [69], by (Star) 69] ~AP1*(F, X) >= @_{o -> o}(F, X) because ~AP1 > @_{o -> o}, [70] and [72], by (Copy) 70] ~AP1*(F, X) >= F because [71], by (Select) 71] F >= F by (Meta) 72] ~AP1*(F, X) >= X because [73], by (Select) 73] X >= X by (Meta) 74] ~L1(F) >= F because [20], by (Star) 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: ~L1(/\x.~AP1(F, x)) 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: ~L1(/\x.~AP1(F, x)) 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) ~AP1(F, X) >= F X ~L1(F) >= F 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 = {0, @_{o -> o}, cons, map, op, pow, s, ~AP1}, and the following precedence: 0 > map > pow > op > s > ~AP1 > @_{o -> o} > cons Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: @_{o -> o}(/\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) >= /\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) ~AP1(F, X) >= @_{o -> o}(F, X) F >= F With these choices, we have: 1] @_{o -> o}(/\x.~AP1(F, x), X) > @_{o -> o}(F, X) because [2], by definition 2] @_{o -> o}*(/\x.~AP1(F, x), X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [3] and [6], by (Stat) 3] /\x.~AP1(F, x) > F because [4], by definition 4] /\x.~AP1*(F, x) >= F because [5], by (Eta)[Kop13:2] 5] F >= F by (Meta) 6] X >= X by (Meta) 7] @_{o -> o}(F, X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [8] and [9], by (Fun) 8] F >= F by (Meta) 9] X >= X by (Meta) 10] map(F, _|_) >= _|_ by (Bot) 11] map(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) because [12], by (Star) 12] map*(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) because map > cons, [13] and [20], by (Copy) 13] map*(F, cons(X, Y)) >= ~AP1(F, X) because map > ~AP1, [14] and [16], by (Copy) 14] map*(F, cons(X, Y)) >= F because [15], by (Select) 15] F >= F by (Meta) 16] map*(F, cons(X, Y)) >= X because [17], by (Select) 17] cons(X, Y) >= X because [18], by (Star) 18] cons*(X, Y) >= X because [19], by (Select) 19] X >= X by (Meta) 20] map*(F, cons(X, Y)) >= map(F, Y) because map in Mul, [21] and [22], by (Stat) 21] F >= F by (Meta) 22] cons(X, Y) > Y because [23], by definition 23] cons*(X, Y) >= Y because [24], by (Select) 24] Y >= Y by (Meta) 25] pow(F, 0) >= /\x.x because [26], by (Star) 26] pow*(F, 0) >= /\y.y because [27], by (F-Abs) 27] pow*(F, 0, x) >= x because [28], by (Select) 28] x >= x by (Var) 29] pow(F, s(X)) >= op(F, pow(F, X)) because [30], by (Star) 30] pow*(F, s(X)) >= op(F, pow(F, X)) because pow > op, [31] and [33], by (Copy) 31] pow*(F, s(X)) >= F because [32], by (Select) 32] F >= F by (Meta) 33] pow*(F, s(X)) >= pow(F, X) because pow in Mul, [34] and [35], by (Stat) 34] F >= F by (Meta) 35] s(X) > X because [36], by definition 36] s*(X) >= X because [37], by (Select) 37] X >= X by (Meta) 38] @_{o -> o}(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [39], by (Star) 39] @_{o -> o}*(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [40], by (Select) 40] op(F, G) @_{o -> o}*(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [41] 41] op*(F, G, @_{o -> o}*(op(F, G), X)) >= ~AP1(F, ~AP1(G, X)) because op > ~AP1, [42] and [44], by (Copy) 42] op*(F, G, @_{o -> o}*(op(F, G), X)) >= F because [43], by (Select) 43] F >= F by (Meta) 44] op*(F, G, @_{o -> o}*(op(F, G), X)) >= ~AP1(G, X) because op > ~AP1, [45] and [47], by (Copy) 45] op*(F, G, @_{o -> o}*(op(F, G), X)) >= G because [46], by (Select) 46] G >= G by (Meta) 47] op*(F, G, @_{o -> o}*(op(F, G), X)) >= X because [48], by (Select) 48] @_{o -> o}*(op(F, G), X) >= X because [49], by (Select) 49] X >= X by (Meta) 50] /\x.~AP1(F, x) >= F because [5], by (Eta)[Kop13:2] 51] /\x.@_{o -> o}(op(F, G), x) >= op(F, G) because [52], by (Eta)[Kop13:2] 52] op(F, G) >= op(F, G) because op in Mul, [53] and [54], by (Fun) 53] F >= F by (Meta) 54] G >= G by (Meta) 55] ~AP1(F, X) >= @_{o -> o}(F, X) because [56], by (Star) 56] ~AP1*(F, X) >= @_{o -> o}(F, X) because ~AP1 > @_{o -> o}, [57] and [59], by (Copy) 57] ~AP1*(F, X) >= F because [58], by (Select) 58] F >= F by (Meta) 59] ~AP1*(F, X) >= X because [60], by (Select) 60] X >= X by (Meta) 61] F >= F 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: ~L1(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 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: ~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) ~AP1(F, X) >= F X ~L1(F) >= F 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 = {0, @_{o -> o}, cons, map, op, pow, s, ~AP1, ~L1}, and the following precedence: 0 > map > cons > pow > s > ~L1 > op > ~AP1 > @_{o -> o} Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: @_{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) ~AP1(F, X) >= @_{o -> o}(F, X) ~L1(F) >= F With these choices, we have: 1] @_{o -> o}(~L1(F), X) > @_{o -> o}(F, X) because [2], by definition 2] @_{o -> o}*(~L1(F), X) >= @_{o -> o}(F, X) because [3], by (Select) 3] ~L1(F) @_{o -> o}*(~L1(F), X) >= @_{o -> o}(F, X) because [4] 4] ~L1*(F, @_{o -> o}*(~L1(F), X)) >= @_{o -> o}(F, X) because ~L1 > @_{o -> o}, [5] and [7], by (Copy) 5] ~L1*(F, @_{o -> o}*(~L1(F), X)) >= F because [6], by (Select) 6] F >= F by (Meta) 7] ~L1*(F, @_{o -> o}*(~L1(F), X)) >= X because [8], by (Select) 8] @_{o -> o}*(~L1(F), X) >= X because [9], by (Select) 9] X >= X by (Meta) 10] map(F, _|_) >= _|_ by (Bot) 11] map(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) because [12], by (Star) 12] map*(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) because map > cons, [13] and [20], by (Copy) 13] map*(F, cons(X, Y)) >= ~AP1(F, X) because map > ~AP1, [14] and [16], by (Copy) 14] map*(F, cons(X, Y)) >= F because [15], by (Select) 15] F >= F by (Meta) 16] map*(F, cons(X, Y)) >= X because [17], by (Select) 17] cons(X, Y) >= X because [18], by (Star) 18] cons*(X, Y) >= X because [19], by (Select) 19] X >= X by (Meta) 20] map*(F, cons(X, Y)) >= map(F, Y) because map in Mul, [21] and [22], by (Stat) 21] F >= F by (Meta) 22] cons(X, Y) > Y because [23], by definition 23] cons*(X, Y) >= Y because [24], by (Select) 24] Y >= Y by (Meta) 25] pow(F, 0) >= ~L1(/\x.x) because [26], by (Star) 26] pow*(F, 0) >= ~L1(/\x.x) because pow > ~L1 and [27], by (Copy) 27] pow*(F, 0) >= /\y.y because [28], by (F-Abs) 28] pow*(F, 0, x) >= x because [29], by (Select) 29] x >= x by (Var) 30] pow(F, s(X)) >= op(F, pow(F, X)) because [31], by (Star) 31] pow*(F, s(X)) >= op(F, pow(F, X)) because pow > op, [32] and [34], by (Copy) 32] pow*(F, s(X)) >= F because [33], by (Select) 33] F >= F by (Meta) 34] pow*(F, s(X)) >= pow(F, X) because pow in Mul, [35] and [36], by (Stat) 35] F >= F by (Meta) 36] s(X) > X because [37], by definition 37] s*(X) >= X because [38], by (Select) 38] X >= X by (Meta) 39] @_{o -> o}(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [40], by (Star) 40] @_{o -> o}*(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [41], by (Select) 41] op(F, G) @_{o -> o}*(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [42] 42] op*(F, G, @_{o -> o}*(op(F, G), X)) >= ~AP1(F, ~AP1(G, X)) because op > ~AP1, [43] and [45], by (Copy) 43] op*(F, G, @_{o -> o}*(op(F, G), X)) >= F because [44], by (Select) 44] F >= F by (Meta) 45] op*(F, G, @_{o -> o}*(op(F, G), X)) >= ~AP1(G, X) because op > ~AP1, [46] and [48], by (Copy) 46] op*(F, G, @_{o -> o}*(op(F, G), X)) >= G because [47], by (Select) 47] G >= G by (Meta) 48] op*(F, G, @_{o -> o}*(op(F, G), X)) >= X because [49], by (Select) 49] @_{o -> o}*(op(F, G), X) >= X because [50], by (Select) 50] X >= X by (Meta) 51] ~L1(/\x.~AP1(F, x)) >= F because [52], by (Star) 52] ~L1*(/\x.~AP1(F, x)) >= F because [53], by (Select) 53] /\x.~AP1(F, x) >= F because [54], by (Eta)[Kop13:2] 54] F >= F by (Meta) 55] ~L1(/\x.@_{o -> o}(op(F, G), x)) >= op(F, G) because [56], by (Star) 56] ~L1*(/\x.@_{o -> o}(op(F, G), x)) >= op(F, G) because ~L1 > op, [57] and [62], by (Copy) 57] ~L1*(/\x.@_{o -> o}(op(F, G), x)) >= F because [58], by (Select) 58] /\x.@_{o -> o}(op(F, G), x) >= F because [59], by (Eta)[Kop13:2] 59] op(F, G) >= F because [60], by (Star) 60] op*(F, G) >= F because [61], by (Select) 61] F >= F by (Meta) 62] ~L1*(/\x.@_{o -> o}(op(F, G), x)) >= G because [63], by (Select) 63] /\x.@_{o -> o}(op(F, G), x) >= G because [64], by (Eta)[Kop13:2] 64] op(F, G) >= G because [65], by (Star) 65] op*(F, G) >= G because [66], by (Select) 66] G >= G by (Meta) 67] ~AP1(F, X) >= @_{o -> o}(F, X) because [68], by (Star) 68] ~AP1*(F, X) >= @_{o -> o}(F, X) because ~AP1 > @_{o -> o}, [69] and [71], by (Copy) 69] ~AP1*(F, X) >= F because [70], by (Select) 70] F >= F by (Meta) 71] ~AP1*(F, X) >= X because [72], by (Select) 72] X >= X by (Meta) 73] ~L1(F) >= F because [74], by (Star) 74] ~L1*(F) >= F because [6], by (Select) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_7, 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_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 [FuhKop19, Thm. 61], we may replace a dependency pair problem (P_4, R_0, minimal, f) by ({}, R_0, minimal, f). By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed. 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. [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.