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 observe that the rules contain a first-order subset: 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) Moreover, the system is orthogonal. Thus, by [Kop12, Thm. 7.55], we may omit all first-order dependency pairs from the dependency pair problem (DP(R), R) if this first-order part is terminating when seen as a many-sorted first-order TRS. According to the external first-order termination prover, this system is indeed terminating: || proof of resources/system.trs || # AProVE Commit ID: d84c10301d352dfd14de2104819581f4682260f5 fuhs 20130616 || || || Termination w.r.t. Q of the given QTRS could be proven: || || (0) QTRS || (1) QTRSRRRProof [EQUIVALENT] || (2) QTRS || (3) RisEmptyProof [EQUIVALENT] || (4) YES || || || ---------------------------------------- || || (0) || Obligation: || Q restricted rewrite system: || The TRS R consists of the following rules: || || 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) || || Q is empty. || || ---------------------------------------- || || (1) QTRSRRRProof (EQUIVALENT) || Used ordering: || Quasi precedence: || mult_2 > add_2 > s_1 || mult_2 > 0 > s_1 || || || Status: || add_2: multiset status || 0: multiset status || s_1: multiset status || mult_2: multiset status || || With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly: || || 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) || || || || || ---------------------------------------- || || (2) || Obligation: || Q restricted rewrite system: || R is empty. || Q is empty. || || ---------------------------------------- || || (3) RisEmptyProof (EQUIVALENT) || The TRS R is empty. Hence, termination is trivially proven. || ---------------------------------------- || || (4) || YES || We use the dependency pair framework as described in [Kop12, Ch. 6/7], with dynamic dependency pairs. After applying [Kop12, Thm. 7.22] to denote collapsing dependency pairs in an extended form, we thus obtain the following dependency pair problem (P_0, R_0, minimal, formative): Dependency Pairs P_0: 0] rec(F, X) s(Y) =#> F(s(Y), rec(F, X) Y) 1] rec(F, X) s(Y) =#> rec(F, X) Y 2] rec(F, X) s(Y) =#> rec#(F, X) 3] fact X =#> rec(mult, s(0)) X 4] fact# =#> rec#(mult, s(0)) 5] fact# =#> mult# 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 => rec(mult, s(0)) Thus, the original system is terminating if (P_0, R_0, minimal, formative) is finite. We consider the dependency pair problem (P_0, R_0, minimal, 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, 2, 3, 4, 5 * 1 : 0, 1, 2 * 2 : * 3 : 0, 1, 2 * 4 : * 5 : This graph has the following strongly connected components: P_1: rec(F, X) s(Y) =#> F(s(Y), rec(F, X) Y) rec(F, X) s(Y) =#> rec(F, X) Y fact X =#> rec(mult, s(0)) X By [Kop12, Thm. 7.31], we may replace any dependency pair problem (P_0, R_0, m, f) by (P_1, R_0, m, f). Thus, the original system is terminating if (P_1, R_0, minimal, formative) is finite. We consider the dependency pair problem (P_1, R_0, minimal, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. As the system is abstraction-simple and the formative flag is set, it suffices to find a tagged reduction pair [Kop12, Def. 6.70]. Thus, we must orient: rec(F, X) s(Y) >? F(s(Y), rec(F, X) Y) rec(F, X) s(Y) >? rec(F, X) Y fact X >? rec(mult, s(0)) X 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)) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( fact ) = #argfun-fact#(/\x.rec(mult, s(0)) x, rec(mult, s(0))) 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]] = _|_ [[mult]] = _|_ We choose Lex = {} and Mul = {#argfun-fact#, @_{o -> o -> o}, @_{o -> o}, add, fact, rec, s}, and the following precedence: #argfun-fact# > rec > fact > @_{o -> o -> o} > @_{o -> o} > add > s Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: @_{o -> o}(rec(F, X), s(Y)) > @_{o -> o}(@_{o -> o -> o}(F, s(Y)), @_{o -> o}(rec(F, X), Y)) @_{o -> o}(rec(F, X), s(Y)) >= @_{o -> o}(rec(F, X), Y) @_{o -> o}(#argfun-fact#(/\x.@_{o -> o}(rec(_|_, s(_|_)), x), rec(_|_, s(_|_))), X) >= @_{o -> o}(rec(_|_, s(_|_)), X) add(_|_, X) >= X add(s(X), Y) >= s(add(X, Y)) @_{o -> o}(@_{o -> o -> o}(_|_, _|_), X) >= _|_ @_{o -> o}(@_{o -> o -> o}(_|_, s(X)), Y) >= add(@_{o -> o}(@_{o -> o -> o}(_|_, X), Y), Y) @_{o -> o}(rec(F, X), _|_) >= X @_{o -> o}(rec(F, X), s(Y)) >= @_{o -> o}(@_{o -> o -> o}(F, s(Y)), @_{o -> o}(rec(F, X), Y)) #argfun-fact#(/\x.@_{o -> o}(rec(_|_, s(_|_)), x), rec(_|_, s(_|_))) >= rec(_|_, s(_|_)) With these choices, we have: 1] @_{o -> o}(rec(F, X), s(Y)) > @_{o -> o}(@_{o -> o -> o}(F, s(Y)), @_{o -> o}(rec(F, X), Y)) because [2], by definition 2] @_{o -> o}*(rec(F, X), s(Y)) >= @_{o -> o}(@_{o -> o -> o}(F, s(Y)), @_{o -> o}(rec(F, X), Y)) because [3], by (Select) 3] rec(F, X) @_{o -> o}*(rec(F, X), s(Y)) >= @_{o -> o}(@_{o -> o -> o}(F, s(Y)), @_{o -> o}(rec(F, X), Y)) because [4] 4] rec*(F, X, @_{o -> o}*(rec(F, X), s(Y))) >= @_{o -> o}(@_{o -> o -> o}(F, s(Y)), @_{o -> o}(rec(F, X), Y)) because rec > @_{o -> o}, [5] and [12], by (Copy) 5] rec*(F, X, @_{o -> o}*(rec(F, X), s(Y))) >= @_{o -> o -> o}(F, s(Y)) because rec > @_{o -> o -> o}, [6] and [8], by (Copy) 6] rec*(F, X, @_{o -> o}*(rec(F, X), s(Y))) >= F because [7], by (Select) 7] F >= F by (Meta) 8] rec*(F, X, @_{o -> o}*(rec(F, X), s(Y))) >= s(Y) because [9], by (Select) 9] @_{o -> o}*(rec(F, X), s(Y)) >= s(Y) because [10], by (Select) 10] s(Y) >= s(Y) because s in Mul and [11], by (Fun) 11] Y >= Y by (Meta) 12] rec*(F, X, @_{o -> o}*(rec(F, X), s(Y))) >= @_{o -> o}(rec(F, X), Y) because [13], by (Select) 13] @_{o -> o}*(rec(F, X), s(Y)) >= @_{o -> o}(rec(F, X), Y) because @_{o -> o} in Mul, [14] and [17], by (Stat) 14] rec(F, X) >= rec(F, X) because rec in Mul, [15] and [16], by (Fun) 15] F >= F by (Meta) 16] X >= X by (Meta) 17] s(Y) > Y because [18], by definition 18] s*(Y) >= Y because [11], by (Select) 19] @_{o -> o}(rec(F, X), s(Y)) >= @_{o -> o}(rec(F, X), Y) because [13], by (Star) 20] @_{o -> o}(#argfun-fact#(/\x.@_{o -> o}(rec(_|_, s(_|_)), x), rec(_|_, s(_|_))), X) >= @_{o -> o}(rec(_|_, s(_|_)), X) because @_{o -> o} in Mul, [21] and [28], by (Fun) 21] #argfun-fact#(/\x.@_{o -> o}(rec(_|_, s(_|_)), x), rec(_|_, s(_|_))) >= rec(_|_, s(_|_)) because [22], by (Star) 22] #argfun-fact#*(/\x.@_{o -> o}(rec(_|_, s(_|_)), x), rec(_|_, s(_|_))) >= rec(_|_, s(_|_)) because #argfun-fact# > rec, [23] and [24], by (Copy) 23] #argfun-fact#*(/\x.@_{o -> o}(rec(_|_, s(_|_)), x), rec(_|_, s(_|_))) >= _|_ by (Bot) 24] #argfun-fact#*(/\x.@_{o -> o}(rec(_|_, s(_|_)), x), rec(_|_, s(_|_))) >= s(_|_) because [25], by (Select) 25] rec(_|_, s(_|_)) #argfun-fact#*(/\x.@_{o -> o}(rec(_|_, s(_|_)), x), rec(_|_, s(_|_))) >= s(_|_) because [26] 26] rec*(_|_, s(_|_), #argfun-fact#*(/\x.@_{o -> o}(rec(_|_, s(_|_)), x), rec(_|_, s(_|_)))) >= s(_|_) because rec > s and [27], by (Copy) 27] rec*(_|_, s(_|_), #argfun-fact#*(/\x.@_{o -> o}(rec(_|_, s(_|_)), x), rec(_|_, s(_|_)))) >= _|_ by (Bot) 28] X >= X by (Meta) 29] add(_|_, X) >= X because [30], by (Star) 30] add*(_|_, X) >= X because [31], by (Select) 31] X >= X by (Meta) 32] add(s(X), Y) >= s(add(X, Y)) because [33], by (Star) 33] add*(s(X), Y) >= s(add(X, Y)) because add > s and [34], by (Copy) 34] add*(s(X), Y) >= add(X, Y) because add in Mul, [35] and [38], by (Stat) 35] s(X) > X because [36], by definition 36] s*(X) >= X because [37], by (Select) 37] X >= X by (Meta) 38] Y >= Y by (Meta) 39] @_{o -> o}(@_{o -> o -> o}(_|_, _|_), X) >= _|_ by (Bot) 40] @_{o -> o}(@_{o -> o -> o}(_|_, s(X)), Y) >= add(@_{o -> o}(@_{o -> o -> o}(_|_, X), Y), Y) because [41], by (Star) 41] @_{o -> o}*(@_{o -> o -> o}(_|_, s(X)), Y) >= add(@_{o -> o}(@_{o -> o -> o}(_|_, X), Y), Y) because @_{o -> o} > add, [42] and [50], by (Copy) 42] @_{o -> o}*(@_{o -> o -> o}(_|_, s(X)), Y) >= @_{o -> o}(@_{o -> o -> o}(_|_, X), Y) because @_{o -> o} in Mul, [43] and [49], by (Stat) 43] @_{o -> o -> o}(_|_, s(X)) > @_{o -> o -> o}(_|_, X) because [44], by definition 44] @_{o -> o -> o}*(_|_, s(X)) >= @_{o -> o -> o}(_|_, X) because @_{o -> o -> o} in Mul, [45] and [46], by (Stat) 45] _|_ >= _|_ by (Bot) 46] s(X) > X because [47], by definition 47] s*(X) >= X because [48], by (Select) 48] X >= X by (Meta) 49] Y >= Y by (Meta) 50] @_{o -> o}*(@_{o -> o -> o}(_|_, s(X)), Y) >= Y because [49], by (Select) 51] @_{o -> o}(rec(F, X), _|_) >= X because [52], by (Star) 52] @_{o -> o}*(rec(F, X), _|_) >= X because [53], by (Select) 53] rec(F, X) @_{o -> o}*(rec(F, X), _|_) >= X because [54] 54] rec*(F, X, @_{o -> o}*(rec(F, X), _|_)) >= X because [55], by (Select) 55] X >= X by (Meta) 56] @_{o -> o}(rec(F, X), s(Y)) >= @_{o -> o}(@_{o -> o -> o}(F, s(Y)), @_{o -> o}(rec(F, X), Y)) because [2], by (Star) 57] #argfun-fact#(/\x.@_{o -> o}(rec(_|_, s(_|_)), x), rec(_|_, s(_|_))) >= rec(_|_, s(_|_)) because [22], by (Star) 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, formative) by (P_2, R_0, minimal, formative), where P_2 consists of: rec(F, X) s(Y) =#> rec(F, X) Y fact X =#> rec(mult, s(0)) X Thus, the original system is terminating if (P_2, R_0, minimal, formative) is finite. We consider the dependency pair problem (P_2, R_0, minimal, 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 This graph has the following strongly connected components: P_3: rec(F, X) s(Y) =#> rec(F, X) Y By [Kop12, Thm. 7.31], we may replace any dependency pair problem (P_2, R_0, m, f) by (P_3, R_0, m, f). Thus, the original system is terminating if (P_3, R_0, minimal, formative) is finite. We consider the dependency pair problem (P_3, R_0, minimal, formative). We apply the subterm criterion with the following projection function: nu(rec) = 3 Thus, we can orient the dependency pairs as follows: nu(rec(F, X) s(Y)) = s(Y) |> Y = nu(rec(F, X) Y) By [FuhKop19, Thm. 61], we may replace a dependency pair problem (P_3, R_0, minimal, f) by ({}, R_0, minimal, f). By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed. As all dependency pair problems were succesfully simplified with sound (and complete) processors until nothing remained, we conclude termination. +++ Citations +++ [FuhKop19] C. Fuhs, and C. Kop. A static higher-order dependency pair framework. In Proceedings of ESOP 2019, 2019. [Kop12] C. Kop. Higher Order Termination. PhD Thesis, 2012.