We consider the system fuhkop12rta2. Alphabet: 0 : [] --> nat build : [nat] --> list collapse : [list] --> nat cons : [nat -> nat * list] --> list diff : [nat * nat] --> nat gcd : [nat * nat] --> nat min : [nat * nat] --> nat nil : [] --> list s : [nat] --> nat Rules: min(x, 0) => 0 min(0, x) => 0 min(s(x), s(y)) => s(min(x, y)) diff(x, 0) => x diff(0, x) => x diff(s(x), s(y)) => diff(x, y) gcd(s(x), 0) => s(x) gcd(0, s(x)) => s(x) gcd(s(x), s(y)) => gcd(diff(x, y), s(min(x, y))) collapse(nil) => 0 collapse(cons(f, x)) => f collapse(x) build(0) => nil build(s(x)) => cons(/\y.gcd(y, x), build(x)) 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 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] min#(s(X), s(Y)) =#> min#(X, Y) 1] diff#(s(X), s(Y)) =#> diff#(X, Y) 2] gcd#(s(X), s(Y)) =#> gcd#(diff(X, Y), s(min(X, Y))) 3] gcd#(s(X), s(Y)) =#> diff#(X, Y) 4] gcd#(s(X), s(Y)) =#> min#(X, Y) 5] collapse#(cons(F, X)) =#> F(collapse(X)) 6] collapse#(cons(F, X)) =#> collapse#(X) 7] build#(s(X)) =#> gcd#(x, X) 8] build#(s(X)) =#> build#(X) Rules R_0: min(X, 0) => 0 min(0, X) => 0 min(s(X), s(Y)) => s(min(X, Y)) diff(X, 0) => X diff(0, X) => X diff(s(X), s(Y)) => diff(X, Y) gcd(s(X), 0) => s(X) gcd(0, s(X)) => s(X) gcd(s(X), s(Y)) => gcd(diff(X, Y), s(min(X, Y))) collapse(nil) => 0 collapse(cons(F, X)) => F collapse(X) build(0) => nil build(s(X)) => cons(/\x.gcd(x, X), build(X)) 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 : 1 * 2 : 2, 3, 4 * 3 : 1 * 4 : 0 * 5 : 0, 1, 2, 3, 4, 5, 6, 7, 8 * 6 : 5, 6 * 7 : * 8 : 7, 8 This graph has the following strongly connected components: P_1: min#(s(X), s(Y)) =#> min#(X, Y) P_2: diff#(s(X), s(Y)) =#> diff#(X, Y) P_3: gcd#(s(X), s(Y)) =#> gcd#(diff(X, Y), s(min(X, Y))) P_4: collapse#(cons(F, X)) =#> F(collapse(X)) collapse#(cons(F, X)) =#> collapse#(X) P_5: build#(s(X)) =#> build#(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), (P_2, R_0, m, f), (P_3, R_0, m, f), (P_4, R_0, m, f) and (P_5, R_0, m, f). Thus, the original system is terminating if each of (P_1, R_0, minimal, formative), (P_2, R_0, minimal, formative), (P_3, R_0, minimal, formative), (P_4, R_0, minimal, formative) and (P_5, R_0, minimal, formative) is finite. We consider the dependency pair problem (P_5, R_0, minimal, formative). We apply the subterm criterion with the following projection function: nu(build#) = 1 Thus, we can orient the dependency pairs as follows: nu(build#(s(X))) = s(X) |> X = nu(build#(X)) By [Kop12, Thm. 7.35], we may replace a dependency pair problem (P_5, 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 each of (P_1, R_0, minimal, formative), (P_2, R_0, minimal, formative), (P_3, R_0, minimal, formative) and (P_4, R_0, minimal, formative) is finite. We consider the dependency pair problem (P_4, 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: collapse#(cons(F, X)) >? F(collapse(X)) collapse#(cons(F, X)) >? collapse#(X) min(X, 0) >= 0 min(0, X) >= 0 min(s(X), s(Y)) >= s(min(X, Y)) diff(X, 0) >= X diff(0, X) >= X diff(s(X), s(Y)) >= diff(X, Y) gcd(s(X), 0) >= s(X) gcd(0, s(X)) >= s(X) gcd(s(X), s(Y)) >= gcd(diff(X, Y), s(min(X, Y))) collapse(nil) >= 0 collapse(cons(F, X)) >= F collapse(X) build(0) >= nil build(s(X)) >= cons(/\x.gcd-(x, X), build(X)) gcd-(X, Y) >= gcd(X, Y) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 0 build = \y0.y0 collapse = \y0.y0 collapse# = \y0.3 + 2y0 cons = \G0y1.y1 + G0(y1) diff = \y0y1.y0 + y1 gcd = \y0y1.y0 + y1 gcd- = \y0y1.y0 + y1 min = \y0y1.0 nil = 0 s = \y0.3y0 Using this interpretation, the requirements translate to: [[collapse#(cons(_F0, _x1))]] = 3 + 2x1 + 2F0(x1) > F0(x1) = [[_F0(collapse(_x1))]] [[collapse#(cons(_F0, _x1))]] = 3 + 2x1 + 2F0(x1) >= 3 + 2x1 = [[collapse#(_x1)]] [[min(_x0, 0)]] = 0 >= 0 = [[0]] [[min(0, _x0)]] = 0 >= 0 = [[0]] [[min(s(_x0), s(_x1))]] = 0 >= 0 = [[s(min(_x0, _x1))]] [[diff(_x0, 0)]] = x0 >= x0 = [[_x0]] [[diff(0, _x0)]] = x0 >= x0 = [[_x0]] [[diff(s(_x0), s(_x1))]] = 3x0 + 3x1 >= x0 + x1 = [[diff(_x0, _x1)]] [[gcd(s(_x0), 0)]] = 3x0 >= 3x0 = [[s(_x0)]] [[gcd(0, s(_x0))]] = 3x0 >= 3x0 = [[s(_x0)]] [[gcd(s(_x0), s(_x1))]] = 3x0 + 3x1 >= x0 + x1 = [[gcd(diff(_x0, _x1), s(min(_x0, _x1)))]] [[collapse(nil)]] = 0 >= 0 = [[0]] [[collapse(cons(_F0, _x1))]] = x1 + F0(x1) >= max(x1, F0(x1)) = [[_F0 collapse(_x1)]] [[build(0)]] = 0 >= 0 = [[nil]] [[build(s(_x0))]] = 3x0 >= 3x0 = [[cons(/\x.gcd-(x, _x0), build(_x0))]] [[gcd-(_x0, _x1)]] = x0 + x1 >= x0 + x1 = [[gcd(_x0, _x1)]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_4, R_0, minimal, formative) by (P_6, R_0, minimal, formative), where P_6 consists of: collapse#(cons(F, X)) =#> collapse#(X) Thus, the original system is terminating if each of (P_1, R_0, minimal, formative), (P_2, R_0, minimal, formative), (P_3, R_0, minimal, formative) and (P_6, R_0, minimal, formative) is finite. We consider the dependency pair problem (P_6, R_0, minimal, formative). We apply the subterm criterion with the following projection function: nu(collapse#) = 1 Thus, we can orient the dependency pairs as follows: nu(collapse#(cons(F, X))) = cons(F, X) |> X = nu(collapse#(X)) By [Kop12, Thm. 7.35], we may replace a dependency pair problem (P_6, 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 each of (P_1, R_0, minimal, formative), (P_2, R_0, minimal, formative) and (P_3, R_0, minimal, formative) is finite. We consider the dependency pair problem (P_3, R_0, minimal, formative). We will use the reduction pair processor with usable rules [Kop12, Thm. 7.44]. The usable rules of (P_3, R_0) are: min(X, 0) => 0 min(0, X) => 0 min(s(X), s(Y)) => s(min(X, Y)) diff(X, 0) => X diff(0, X) => X diff(s(X), s(Y)) => diff(X, Y) It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: gcd#(s(X), s(Y)) >? gcd#(diff(X, Y), s(min(X, Y))) min(X, 0) >= 0 min(0, X) >= 0 min(s(X), s(Y)) >= s(min(X, Y)) diff(X, 0) >= X diff(0, X) >= X diff(s(X), s(Y)) >= diff(X, Y) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 0 diff = \y0y1.y0 + y1 gcd# = \y0y1.y1 + 2y0 min = \y0y1.y0 s = \y0.1 + 2y0 Using this interpretation, the requirements translate to: [[gcd#(s(_x0), s(_x1))]] = 3 + 2x1 + 4x0 > 1 + 2x1 + 4x0 = [[gcd#(diff(_x0, _x1), s(min(_x0, _x1)))]] [[min(_x0, 0)]] = x0 >= 0 = [[0]] [[min(0, _x0)]] = 0 >= 0 = [[0]] [[min(s(_x0), s(_x1))]] = 1 + 2x0 >= 1 + 2x0 = [[s(min(_x0, _x1))]] [[diff(_x0, 0)]] = x0 >= x0 = [[_x0]] [[diff(0, _x0)]] = x0 >= x0 = [[_x0]] [[diff(s(_x0), s(_x1))]] = 2 + 2x0 + 2x1 >= x0 + x1 = [[diff(_x0, _x1)]] 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, minimal, formative) and (P_2, R_0, minimal, formative) is finite. We consider the dependency pair problem (P_2, R_0, minimal, formative). We apply the subterm criterion with the following projection function: nu(diff#) = 1 Thus, we can orient the dependency pairs as follows: nu(diff#(s(X), s(Y))) = s(X) |> X = nu(diff#(X, Y)) 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, formative) is finite. We consider the dependency pair problem (P_1, R_0, minimal, formative). We apply the subterm criterion with the following projection function: nu(min#) = 1 Thus, we can orient the dependency pairs as follows: nu(min#(s(X), s(Y))) = s(X) |> X = nu(min#(X, Y)) By [Kop12, Thm. 7.35], we may replace a dependency pair problem (P_1, 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 +++ [Kop12] C. Kop. Higher Order Termination. PhD Thesis, 2012.