We consider the system AotoYamada_05__Ex5TermProof. Alphabet: 0 : [] --> a add : [a * a] --> a fact : [] --> a -> a mult : [] --> a -> a -> a rec : [a -> a -> a * a] --> a -> a s : [a] --> a Rules: add(0, x) => x add(s(x), y) => s(add(x, y)) mult 0 x => 0 mult s(x) y => add(mult x y, y) rec(f, x) 0 => x rec(f, x) s(y) => f s(y) (rec(f, x) y) fact => rec(mult, s(0)) This AFS is converted to an AFSM simply by replacing all free variables by meta-variables (with arity 0). We use the dependency pair framework as described in [Kop12, Ch. 6/7], with static dependency pairs (see [KusIsoSakBla09] and the adaptation for AFSMs and accessible arguments in [Kop13]). In order to do so, we start by eta-expanding the system, which gives: add(0, X) => X add(s(X), Y) => s(add(X, Y)) mult(0, X) => 0 mult(s(X), Y) => add(mult(X, Y), Y) rec(F, X, 0) => X rec(F, X, s(Y)) => F s(Y) rec(F, X, Y) fact(X) => rec(/\x./\y.mult(x, y), s(0), X) We thus obtain the following dependency pair problem (P_0, R_0, static, formative): Dependency Pairs P_0: 0] add#(s(X), Y) =#> add#(X, Y) 1] mult#(s(X), Y) =#> add#(mult(X, Y), Y) 2] mult#(s(X), Y) =#> mult#(X, Y) 3] rec#(F, X, s(Y)) =#> rec#(F, X, Y) 4] fact#(X) =#> rec#(/\x./\y.mult(x, y), s(0), X) 5] fact#(X) =#> mult#(Y, Z) Rules R_0: add(0, X) => X add(s(X), Y) => s(add(X, Y)) mult(0, X) => 0 mult(s(X), Y) => add(mult(X, Y), Y) rec(F, X, 0) => X rec(F, X, s(Y)) => F s(Y) rec(F, X, Y) fact(X) => rec(/\x./\y.mult(x, y), s(0), X) Thus, the original system is terminating if (P_0, R_0, static, formative) is finite. We consider the dependency pair problem (P_0, R_0, static, formative). 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 * 2 : 1, 2 * 3 : 3 * 4 : 3 * 5 : 1, 2 This graph has the following strongly connected components: P_1: add#(s(X), Y) =#> add#(X, Y) P_2: mult#(s(X), Y) =#> mult#(X, Y) P_3: rec#(F, X, s(Y)) =#> rec#(F, X, Y) 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), (P_2, R_0, m, f) and (P_3, R_0, m, f). Thus, the original system is terminating if each of (P_1, R_0, static, formative), (P_2, R_0, static, formative) and (P_3, R_0, static, formative) is finite. We consider the dependency pair problem (P_3, R_0, static, formative). 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#(F, X, s(Y)) >? rec#(F, X, Y) add(0, X) >= X add(s(X), Y) >= s(add(X, Y)) mult(0, X) >= 0 mult(s(X), Y) >= add(mult(X, Y), Y) rec(F, X, 0) >= X rec(F, X, s(Y)) >= F s(Y) rec(F, X, Y) fact(X) >= rec(/\x./\y.mult(x, y), s(0), X) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( fact(X) ) = #argfun-fact#(rec(/\x./\y.mult(x, y), s(0), 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-fact#(x_1)]] = x_1 [[fact(x_1)]] = x_1 [[rec#(x_1, x_2, x_3)]] = rec#(x_1, x_3, x_2) We choose Lex = {rec#} and Mul = {0, @_{o -> o -> o}, @_{o -> o}, add, mult, rec, s}, and the following precedence: rec > rec# > 0 > @_{o -> o} > mult > add > @_{o -> o -> o} > s Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: rec#(F, X, s(Y)) > rec#(F, X, Y) add(0, X) >= X add(s(X), Y) >= s(add(X, Y)) mult(0, X) >= 0 mult(s(X), Y) >= add(mult(X, Y), Y) rec(F, X, 0) >= X rec(F, X, s(Y)) >= @_{o -> o}(@_{o -> o -> o}(F, s(Y)), rec(F, X, Y)) rec(/\x./\y.mult(x, y), s(0), X) >= rec(/\x./\y.mult(x, y), s(0), X) With these choices, we have: 1] rec#(F, X, s(Y)) > rec#(F, X, Y) because [2], by definition 2] rec#*(F, X, s(Y)) >= rec#(F, X, Y) because [3], [4], [7], [8] and [10], by (Stat) 3] F >= F by (Meta) 4] s(Y) > Y because [5], by definition 5] s*(Y) >= Y because [6], by (Select) 6] Y >= Y by (Meta) 7] rec#*(F, X, s(Y)) >= F because [3], by (Select) 8] rec#*(F, X, s(Y)) >= X because [9], by (Select) 9] X >= X by (Meta) 10] rec#*(F, X, s(Y)) >= Y because [11], by (Select) 11] s(Y) >= Y because [5], by (Star) 12] add(0, X) >= X because [13], by (Star) 13] add*(0, X) >= X because [14], by (Select) 14] X >= X by (Meta) 15] add(s(X), Y) >= s(add(X, Y)) because [16], by (Star) 16] add*(s(X), Y) >= s(add(X, Y)) because add > s and [17], by (Copy) 17] add*(s(X), Y) >= add(X, Y) because add in Mul, [18] and [21], by (Stat) 18] s(X) > X because [19], by definition 19] s*(X) >= X because [20], by (Select) 20] X >= X by (Meta) 21] Y >= Y by (Meta) 22] mult(0, X) >= 0 because [23], by (Star) 23] mult*(0, X) >= 0 because [24], by (Select) 24] 0 >= 0 by (Fun) 25] mult(s(X), Y) >= add(mult(X, Y), Y) because [26], by (Star) 26] mult*(s(X), Y) >= add(mult(X, Y), Y) because mult > add, [27] and [32], by (Copy) 27] mult*(s(X), Y) >= mult(X, Y) because mult in Mul, [28] and [31], by (Stat) 28] s(X) > X because [29], by definition 29] s*(X) >= X because [30], by (Select) 30] X >= X by (Meta) 31] Y >= Y by (Meta) 32] mult*(s(X), Y) >= Y because [31], by (Select) 33] rec(F, X, 0) >= X because [34], by (Star) 34] rec*(F, X, 0) >= X because [35], by (Select) 35] X >= X by (Meta) 36] rec(F, X, s(Y)) >= @_{o -> o}(@_{o -> o -> o}(F, s(Y)), rec(F, X, Y)) because [37], by (Star) 37] rec*(F, X, s(Y)) >= @_{o -> o}(@_{o -> o -> o}(F, s(Y)), rec(F, X, Y)) because rec > @_{o -> o}, [38] and [43], by (Copy) 38] rec*(F, X, s(Y)) >= @_{o -> o -> o}(F, s(Y)) because rec > @_{o -> o -> o}, [39] and [40], by (Copy) 39] rec*(F, X, s(Y)) >= F because [3], by (Select) 40] rec*(F, X, s(Y)) >= s(Y) because [41], by (Select) 41] s(Y) >= s(Y) because s in Mul and [42], by (Fun) 42] Y >= Y by (Meta) 43] rec*(F, X, s(Y)) >= rec(F, X, Y) because rec in Mul, [3], [44] and [4], by (Stat) 44] X >= X by (Meta) 45] rec(/\x./\y.mult(x, y), s(0), X) >= rec(/\x./\y.mult(x, y), s(0), X) because rec in Mul, [46], [51] and [53], by (Fun) 46] /\x./\z.mult(x, z) >= /\x./\z.mult(x, z) because [47], by (Abs) 47] /\z.mult(y, z) >= /\z.mult(y, z) because [48], by (Abs) 48] mult(y, x) >= mult(y, x) because mult in Mul, [49] and [50], by (Fun) 49] y >= y by (Var) 50] x >= x by (Var) 51] s(0) >= s(0) because s in Mul and [52], by (Fun) 52] 0 >= 0 by (Fun) 53] X >= X by (Meta) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_3, 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 each of (P_1, R_0, static, formative) and (P_2, R_0, static, formative) is finite. We consider the dependency pair problem (P_2, R_0, static, formative). 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: mult#(s(X), Y) >? mult#(X, Y) add(0, X) >= X add(s(X), Y) >= s(add(X, Y)) mult(0, X) >= 0 mult(s(X), Y) >= add(mult(X, Y), Y) rec(F, X, 0) >= X rec(F, X, s(Y)) >= F s(Y) rec(F, X, Y) fact(X) >= rec(/\x./\y.mult(x, y), s(0), X) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( fact(X) ) = #argfun-fact#(rec(/\x./\y.mult(x, y), s(0), 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]] = _|_ [[fact(x_1)]] = x_1 We choose Lex = {mult#} and Mul = {#argfun-fact#, @_{o -> o -> o}, @_{o -> o}, add, mult, rec, s}, and the following precedence: #argfun-fact# > mult > add > mult# > rec = s > @_{o -> o -> o} > @_{o -> o} Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: mult#(s(X), Y) > mult#(X, Y) add(_|_, X) >= X add(s(X), Y) >= s(add(X, Y)) mult(_|_, X) >= _|_ mult(s(X), Y) >= add(mult(X, Y), Y) rec(F, X, _|_) >= X rec(F, X, s(Y)) >= @_{o -> o}(@_{o -> o -> o}(F, s(Y)), rec(F, X, Y)) #argfun-fact#(rec(/\x./\y.mult(x, y), s(_|_), X)) >= rec(/\x./\y.mult(x, y), s(_|_), X) With these choices, we have: 1] mult#(s(X), Y) > mult#(X, Y) because [2], by definition 2] mult#*(s(X), Y) >= mult#(X, Y) because [3], [6] and [8], by (Stat) 3] s(X) > X because [4], by definition 4] s*(X) >= X because [5], by (Select) 5] X >= X by (Meta) 6] mult#*(s(X), Y) >= X because [7], by (Select) 7] s(X) >= X because [4], by (Star) 8] mult#*(s(X), Y) >= Y because [9], by (Select) 9] Y >= Y by (Meta) 10] add(_|_, X) >= X because [11], by (Star) 11] add*(_|_, X) >= X because [12], by (Select) 12] X >= X by (Meta) 13] add(s(X), Y) >= s(add(X, Y)) because [14], by (Star) 14] add*(s(X), Y) >= s(add(X, Y)) because add > s and [15], by (Copy) 15] add*(s(X), Y) >= add(X, Y) because add in Mul, [16] and [19], by (Stat) 16] s(X) > X because [17], by definition 17] s*(X) >= X because [18], by (Select) 18] X >= X by (Meta) 19] Y >= Y by (Meta) 20] mult(_|_, X) >= _|_ by (Bot) 21] mult(s(X), Y) >= add(mult(X, Y), Y) because [22], by (Star) 22] mult*(s(X), Y) >= add(mult(X, Y), Y) because mult > add, [23] and [25], by (Copy) 23] mult*(s(X), Y) >= mult(X, Y) because mult in Mul, [3] and [24], by (Stat) 24] Y >= Y by (Meta) 25] mult*(s(X), Y) >= Y because [24], by (Select) 26] rec(F, X, _|_) >= X because [27], by (Star) 27] rec*(F, X, _|_) >= X because [28], by (Select) 28] X >= X by (Meta) 29] rec(F, X, s(Y)) >= @_{o -> o}(@_{o -> o -> o}(F, s(Y)), rec(F, X, Y)) because [30], by (Star) 30] rec*(F, X, s(Y)) >= @_{o -> o}(@_{o -> o -> o}(F, s(Y)), rec(F, X, Y)) because rec > @_{o -> o}, [31] and [38], by (Copy) 31] rec*(F, X, s(Y)) >= @_{o -> o -> o}(F, s(Y)) because rec > @_{o -> o -> o}, [32] and [34], by (Copy) 32] rec*(F, X, s(Y)) >= F because [33], by (Select) 33] F >= F by (Meta) 34] rec*(F, X, s(Y)) >= s(Y) because rec = s, rec in Mul and [35], by (Stat) 35] s(Y) > Y because [36], by definition 36] s*(Y) >= Y because [37], by (Select) 37] Y >= Y by (Meta) 38] rec*(F, X, s(Y)) >= rec(F, X, Y) because rec in Mul, [39], [40] and [35], by (Stat) 39] F >= F by (Meta) 40] X >= X by (Meta) 41] #argfun-fact#(rec(/\x./\y.mult(x, y), s(_|_), X)) >= rec(/\x./\y.mult(x, y), s(_|_), X) because [42], by (Star) 42] #argfun-fact#*(rec(/\x./\y.mult(x, y), s(_|_), X)) >= rec(/\x./\y.mult(x, y), s(_|_), X) because #argfun-fact# > rec, [43], [50] and [52], by (Copy) 43] #argfun-fact#*(rec(/\x./\y.mult(x, y), s(_|_), X)) >= /\x./\y.mult(x, y) because [44], by (F-Abs) 44] #argfun-fact#*(rec(/\x./\y.mult(x, y), s(_|_), X), z) >= /\x.mult(z, x) because [45], by (F-Abs) 45] #argfun-fact#*(rec(/\x./\y.mult(x, y), s(_|_), X), z, u) >= mult(z, u) because #argfun-fact# > mult, [46] and [48], by (Copy) 46] #argfun-fact#*(rec(/\x./\y.mult(x, y), s(_|_), X), z, u) >= z because [47], by (Select) 47] z >= z by (Var) 48] #argfun-fact#*(rec(/\x./\y.mult(x, y), s(_|_), X), z, u) >= u because [49], by (Select) 49] u >= u by (Var) 50] #argfun-fact#*(rec(/\x./\y.mult(x, y), s(_|_), X)) >= s(_|_) because #argfun-fact# > s and [51], by (Copy) 51] #argfun-fact#*(rec(/\x./\y.mult(x, y), s(_|_), X)) >= _|_ by (Bot) 52] #argfun-fact#*(rec(/\x./\y.mult(x, y), s(_|_), X)) >= X because [53], by (Select) 53] rec(/\x./\y.mult(x, y), s(_|_), X) >= X because [54], by (Star) 54] rec*(/\x./\y.mult(x, y), s(_|_), X) >= X because [55], by (Select) 55] X >= X by (Meta) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_2, 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_1, R_0, static, formative) is finite. We consider the dependency pair problem (P_1, R_0, static, formative). 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: add#(s(X), Y) >? add#(X, Y) add(0, X) >= X add(s(X), Y) >= s(add(X, Y)) mult(0, X) >= 0 mult(s(X), Y) >= add(mult(X, Y), Y) rec(F, X, 0) >= X rec(F, X, s(Y)) >= F s(Y) rec(F, X, Y) fact(X) >= rec(/\x./\y.mult(x, y), s(0), X) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( fact(X) ) = #argfun-fact#(rec(/\x./\y.mult(x, y), s(0), 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: [[fact(x_1)]] = x_1 We choose Lex = {add#} and Mul = {#argfun-fact#, 0, @_{o -> o -> o}, @_{o -> o}, add, mult, rec, s}, and the following precedence: #argfun-fact# > add# > mult > add > rec > 0 > @_{o -> o -> o} > @_{o -> o} > s Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: add#(s(X), Y) > add#(X, Y) add(0, X) >= X add(s(X), Y) >= s(add(X, Y)) mult(0, X) >= 0 mult(s(X), Y) >= add(mult(X, Y), Y) rec(F, X, 0) >= X rec(F, X, s(Y)) >= @_{o -> o}(@_{o -> o -> o}(F, s(Y)), rec(F, X, Y)) #argfun-fact#(rec(/\x./\y.mult(x, y), s(0), X)) >= rec(/\x./\y.mult(x, y), s(0), X) With these choices, we have: 1] add#(s(X), Y) > add#(X, Y) because [2], by definition 2] add#*(s(X), Y) >= add#(X, Y) because [3], [6] and [8], by (Stat) 3] s(X) > X because [4], by definition 4] s*(X) >= X because [5], by (Select) 5] X >= X by (Meta) 6] add#*(s(X), Y) >= X because [7], by (Select) 7] s(X) >= X because [4], by (Star) 8] add#*(s(X), Y) >= Y because [9], by (Select) 9] Y >= Y by (Meta) 10] add(0, X) >= X because [11], by (Star) 11] add*(0, X) >= X because [12], by (Select) 12] X >= X by (Meta) 13] add(s(X), Y) >= s(add(X, Y)) because [14], by (Star) 14] add*(s(X), Y) >= s(add(X, Y)) because add > s and [15], by (Copy) 15] add*(s(X), Y) >= add(X, Y) because add in Mul, [3] and [16], by (Stat) 16] Y >= Y by (Meta) 17] mult(0, X) >= 0 because [18], by (Star) 18] mult*(0, X) >= 0 because mult > 0, by (Copy) 19] mult(s(X), Y) >= add(mult(X, Y), Y) because [20], by (Star) 20] mult*(s(X), Y) >= add(mult(X, Y), Y) because mult > add, [21] and [26], by (Copy) 21] mult*(s(X), Y) >= mult(X, Y) because mult in Mul, [22] and [25], by (Stat) 22] s(X) > X because [23], by definition 23] s*(X) >= X because [24], by (Select) 24] X >= X by (Meta) 25] Y >= Y by (Meta) 26] mult*(s(X), Y) >= Y because [25], by (Select) 27] rec(F, X, 0) >= X because [28], by (Star) 28] rec*(F, X, 0) >= X because [29], by (Select) 29] X >= X by (Meta) 30] rec(F, X, s(Y)) >= @_{o -> o}(@_{o -> o -> o}(F, s(Y)), rec(F, X, Y)) because [31], by (Star) 31] rec*(F, X, s(Y)) >= @_{o -> o}(@_{o -> o -> o}(F, s(Y)), rec(F, X, Y)) because rec > @_{o -> o}, [32] and [40], by (Copy) 32] rec*(F, X, s(Y)) >= @_{o -> o -> o}(F, s(Y)) because rec > @_{o -> o -> o}, [33] and [35], by (Copy) 33] rec*(F, X, s(Y)) >= F because [34], by (Select) 34] F >= F by (Meta) 35] rec*(F, X, s(Y)) >= s(Y) because rec > s and [36], by (Copy) 36] rec*(F, X, s(Y)) >= Y because [37], by (Select) 37] s(Y) >= Y because [38], by (Star) 38] s*(Y) >= Y because [39], by (Select) 39] Y >= Y by (Meta) 40] rec*(F, X, s(Y)) >= rec(F, X, Y) because rec in Mul, [41], [42] and [43], by (Stat) 41] F >= F by (Meta) 42] X >= X by (Meta) 43] s(Y) > Y because [44], by definition 44] s*(Y) >= Y because [39], by (Select) 45] #argfun-fact#(rec(/\x./\y.mult(x, y), s(0), X)) >= rec(/\x./\y.mult(x, y), s(0), X) because [46], by (Star) 46] #argfun-fact#*(rec(/\x./\y.mult(x, y), s(0), X)) >= rec(/\x./\y.mult(x, y), s(0), X) because #argfun-fact# > rec, [47], [54] and [58], by (Copy) 47] #argfun-fact#*(rec(/\x./\y.mult(x, y), s(0), X)) >= /\x./\y.mult(x, y) because [48], by (F-Abs) 48] #argfun-fact#*(rec(/\x./\y.mult(x, y), s(0), X), z) >= /\x.mult(z, x) because [49], by (F-Abs) 49] #argfun-fact#*(rec(/\x./\y.mult(x, y), s(0), X), z, u) >= mult(z, u) because #argfun-fact# > mult, [50] and [52], by (Copy) 50] #argfun-fact#*(rec(/\x./\y.mult(x, y), s(0), X), z, u) >= z because [51], by (Select) 51] z >= z by (Var) 52] #argfun-fact#*(rec(/\x./\y.mult(x, y), s(0), X), z, u) >= u because [53], by (Select) 53] u >= u by (Var) 54] #argfun-fact#*(rec(/\x./\y.mult(x, y), s(0), X)) >= s(0) because [55], by (Select) 55] rec(/\x./\y.mult(x, y), s(0), X) >= s(0) because [56], by (Star) 56] rec*(/\x./\y.mult(x, y), s(0), X) >= s(0) because rec > s and [57], by (Copy) 57] rec*(/\x./\y.mult(x, y), s(0), X) >= 0 because rec > 0, by (Copy) 58] #argfun-fact#*(rec(/\x./\y.mult(x, y), s(0), X)) >= X because [59], by (Select) 59] rec(/\x./\y.mult(x, y), s(0), X) >= X because [60], by (Star) 60] rec*(/\x./\y.mult(x, y), s(0), X) >= X because [61], by (Select) 61] X >= X by (Meta) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_1, R_0) by ({}, R_0). 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 +++ [Kop12] C. Kop. Higher Order Termination. PhD Thesis, 2012. [Kop13] C. Kop. Static Dependency Pairs with Accessibility. Unpublished manuscript, http://cl-informatik.uibk.ac.at/users/kop/static.pdf, 2013. [KusIsoSakBla09] K. Kusakari, Y. Isogai, M. Sakai, and F. Blanqui. Static Dependency Pair Method Based On Strong Computability for Higher-Order Rewrite Systems. In volume 92(10) of IEICE Transactions on Information and Systems. 2007--2015, 2009.