We consider the system extrec.

  Alphabet:

    !plus : [nat * nat] --> nat 
    !times : [nat * nat] --> nat 
    0 : [] --> nat 
    rec : [nat * nat * nat -> nat -> nat] --> nat 
    s : [nat] --> nat 

  Rules:

    !plus(x, 0) => x 
    !plus(x, s(y)) => s(!plus(x, y)) 
    rec(0, x, f) => x 
    rec(s(x), y, f) => f x rec(x, y, f) 
    !times(x, y) => rec(y, 0, /\z./\u.!plus(x, u)) 

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]).

We thus obtain the following dependency pair problem (P_0, R_0, static, formative):

  Dependency Pairs P_0:

    0] !plus#(X, s(Y)) =#> !plus#(X, Y)   
    1] rec#(s(X), Y, F) =#> rec#(X, Y, F)   
    2] !times#(X, Y) =#> rec#(Y, 0, /\x./\y.!plus(X, y))   
    3] !times#(X, Y) =#> !plus#(X, Z)   

  Rules R_0:

    !plus(X, 0) => X 
    !plus(X, s(Y)) => s(!plus(X, Y)) 
    rec(0, X, F) => X 
    rec(s(X), Y, F) => F X rec(X, Y, F) 
    !times(X, Y) => rec(Y, 0, /\x./\y.!plus(X, y)) 

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 : 1 
    * 2 : 1 
    * 3 : 0 

This graph has the following strongly connected components:

  P_1:

    !plus#(X, s(Y)) =#> !plus#(X, Y)   

  P_2:

    rec#(s(X), Y, F) =#> rec#(X, Y, F)   

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, 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:

  rec#(s(X), Y, F) >? rec#(X, Y, F) 
  !plus(X, 0) >= X 
  !plus(X, s(Y)) >= s(!plus(X, Y)) 
  rec(0, X, F) >= X 
  rec(s(X), Y, F) >= F X rec(X, Y, F) 
  !times(X, Y) >= rec(Y, 0, /\x./\y.!plus(X, y)) 

We apply [Kop12, Thm. 6.75] and use the following argument functions:

  pi( !times(X, Y) ) = #argfun-!times#(rec(Y, 0, /\x./\y.!plus(X, y))) 

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:

  [[rec#(x_1, x_2, x_3)]] = rec#(x_1) 

We choose Lex = {} and Mul = {!plus, !times, #argfun-!times#, 0, @_{o -> o -> o}, @_{o -> o}, rec, rec#, s}, and the following precedence: !times > rec > @_{o -> o -> o} > !plus > rec# = s > @_{o -> o} > #argfun-!times# > 0

Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows:

  rec#(s(X)) > rec#(X) 
  !plus(X, 0) >= X 
  !plus(X, s(Y)) >= s(!plus(X, Y)) 
  rec(0, X, F) >= X 
  rec(s(X), Y, F) >= @_{o -> o}(@_{o -> o -> o}(F, X), rec(X, Y, F)) 
  #argfun-!times#(rec(X, 0, /\x./\y.!plus(Y, y))) >= rec(X, 0, /\x./\y.!plus(Y, y)) 

With these choices, we have:

  1] rec#(s(X)) > rec#(X)  because [2], by definition 
  2] rec#*(s(X)) >= rec#(X)  because [3], by (Select) 
  3] s(X) >= rec#(X)  because s = rec#, s in Mul and [4], by (Fun) 
  4] X >= X  by (Meta) 

  5] !plus(X, 0) >= X  because [6], by (Star) 
  6] !plus*(X, 0) >= X  because [7], by (Select) 
  7] X >= X  by (Meta) 

  8] !plus(X, s(Y)) >= s(!plus(X, Y))  because [9], by (Star) 
  9] !plus*(X, s(Y)) >= s(!plus(X, Y))  because !plus > s and [10], by (Copy) 
  10] !plus*(X, s(Y)) >= !plus(X, Y)  because !plus in Mul, [11] and [12], by (Stat) 
  11] X >= X  by (Meta) 
  12] s(Y) > Y  because [13], by definition 
  13] s*(Y) >= Y  because [14], by (Select) 
  14] Y >= Y  by (Meta) 

  15] rec(0, X, F) >= X  because [16], by (Star) 
  16] rec*(0, X, F) >= X  because [17], by (Select) 
  17] X >= X  by (Meta) 

  18] rec(s(X), Y, F) >= @_{o -> o}(@_{o -> o -> o}(F, X), rec(X, Y, F))  because [19], by (Star) 
  19] rec*(s(X), Y, F) >= @_{o -> o}(@_{o -> o -> o}(F, X), rec(X, Y, F))  because rec > @_{o -> o}, [20] and [26], by (Copy) 
  20] rec*(s(X), Y, F) >= @_{o -> o -> o}(F, X)  because rec > @_{o -> o -> o}, [21] and [23], by (Copy) 
  21] rec*(s(X), Y, F) >= F  because [22], by (Select) 
  22] F >= F  by (Meta) 
  23] rec*(s(X), Y, F) >= X  because [24], by (Select) 
  24] s(X) >= X  because [25], by (Star) 
  25] s*(X) >= X  because [4], by (Select) 
  26] rec*(s(X), Y, F) >= rec(X, Y, F)  because rec in Mul, [27], [29] and [30], by (Stat) 
  27] s(X) > X  because [28], by definition 
  28] s*(X) >= X  because [4], by (Select) 
  29] Y >= Y  by (Meta) 
  30] F >= F  by (Meta) 

  31] #argfun-!times#(rec(X, 0, /\x./\y.!plus(Y, y))) >= rec(X, 0, /\x./\y.!plus(Y, y))  because [32], by (Star) 
  32] #argfun-!times#*(rec(X, 0, /\x./\y.!plus(Y, y))) >= rec(X, 0, /\x./\y.!plus(Y, y))  because [33], by (Select) 
  33] rec(X, 0, /\x./\y.!plus(Y, y)) >= rec(X, 0, /\x./\y.!plus(Y, y))  because rec in Mul, [34], [35] and [36], by (Fun) 
  34] X >= X  by (Meta) 
  35] 0 >= 0  by (Fun) 
  36] /\x./\y.!plus(Y, y) >= /\x./\y.!plus(Y, y)  because [37], by (Abs) 
  37] /\y.!plus(Y, y) >= /\y.!plus(Y, y)  because [38], by (Abs) 
  38] !plus(Y, x) >= !plus(Y, x)  because !plus in Mul, [39] and [40], by (Fun) 
  39] Y >= Y  by (Meta) 
  40] x >= x  by (Var) 

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:

  !plus#(X, s(Y)) >? !plus#(X, Y) 
  !plus(X, 0) >= X 
  !plus(X, s(Y)) >= s(!plus(X, Y)) 
  rec(0, X, F) >= X 
  rec(s(X), Y, F) >= F X rec(X, Y, F) 
  !times(X, Y) >= rec(Y, 0, /\x./\y.!plus(X, y)) 

We apply [Kop12, Thm. 6.75] and use the following argument functions:

  pi( !times(X, Y) ) = #argfun-!times#(rec(Y, 0, /\x./\y.!plus(X, y))) 

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]] = _|_ 

We choose Lex = {} and Mul = {!plus, !plus#, !times, #argfun-!times#, @_{o -> o -> o}, @_{o -> o}, rec, s}, and the following precedence: !plus# > !times > #argfun-!times# > !plus > rec > @_{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:

  !plus#(X, s(Y)) > !plus#(X, Y) 
  !plus(X, _|_) >= X 
  !plus(X, s(Y)) >= s(!plus(X, Y)) 
  rec(_|_, X, F) >= X 
  rec(s(X), Y, F) >= @_{o -> o}(@_{o -> o -> o}(F, X), rec(X, Y, F)) 
  #argfun-!times#(rec(X, _|_, /\x./\y.!plus(Y, y))) >= rec(X, _|_, /\x./\y.!plus(Y, y)) 

With these choices, we have:

  1] !plus#(X, s(Y)) > !plus#(X, Y)  because [2], by definition 
  2] !plus#*(X, s(Y)) >= !plus#(X, Y)  because !plus# in Mul, [3] and [4], by (Stat) 
  3] X >= X  by (Meta) 
  4] s(Y) > Y  because [5], by definition 
  5] s*(Y) >= Y  because [6], by (Select) 
  6] Y >= Y  by (Meta) 

  7] !plus(X, _|_) >= X  because [8], by (Star) 
  8] !plus*(X, _|_) >= X  because [9], by (Select) 
  9] X >= X  by (Meta) 

  10] !plus(X, s(Y)) >= s(!plus(X, Y))  because [11], by (Star) 
  11] !plus*(X, s(Y)) >= s(!plus(X, Y))  because !plus > s and [12], by (Copy) 
  12] !plus*(X, s(Y)) >= !plus(X, Y)  because !plus in Mul, [3] and [4], by (Stat) 

  13] rec(_|_, X, F) >= X  because [14], by (Star) 
  14] rec*(_|_, X, F) >= X  because [15], by (Select) 
  15] X >= X  by (Meta) 

  16] rec(s(X), Y, F) >= @_{o -> o}(@_{o -> o -> o}(F, X), rec(X, Y, F))  because [17], by (Star) 
  17] rec*(s(X), Y, F) >= @_{o -> o}(@_{o -> o -> o}(F, X), rec(X, Y, F))  because rec > @_{o -> o}, [18] and [25], by (Copy) 
  18] rec*(s(X), Y, F) >= @_{o -> o -> o}(F, X)  because rec > @_{o -> o -> o}, [19] and [21], by (Copy) 
  19] rec*(s(X), Y, F) >= F  because [20], by (Select) 
  20] F >= F  by (Meta) 
  21] rec*(s(X), Y, F) >= X  because [22], by (Select) 
  22] s(X) >= X  because [23], by (Star) 
  23] s*(X) >= X  because [24], by (Select) 
  24] X >= X  by (Meta) 
  25] rec*(s(X), Y, F) >= rec(X, Y, F)  because rec in Mul, [26], [28] and [29], by (Stat) 
  26] s(X) > X  because [27], by definition 
  27] s*(X) >= X  because [24], by (Select) 
  28] Y >= Y  by (Meta) 
  29] F >= F  by (Meta) 

  30] #argfun-!times#(rec(X, _|_, /\x./\y.!plus(Y, y))) >= rec(X, _|_, /\x./\y.!plus(Y, y))  because [31], by (Star) 
  31] #argfun-!times#*(rec(X, _|_, /\x./\y.!plus(Y, y))) >= rec(X, _|_, /\x./\y.!plus(Y, y))  because #argfun-!times# > rec, [32], [36] and [37], by (Copy) 
  32] #argfun-!times#*(rec(X, _|_, /\x./\y.!plus(Y, y))) >= X  because [33], by (Select) 
  33] rec(X, _|_, /\x./\y.!plus(Y, y)) >= X  because [34], by (Star) 
  34] rec*(X, _|_, /\x./\y.!plus(Y, y)) >= X  because [35], by (Select) 
  35] X >= X  by (Meta) 
  36] #argfun-!times#*(rec(X, _|_, /\x./\y.!plus(Y, y))) >= _|_  by (Bot) 
  37] #argfun-!times#*(rec(X, _|_, /\x./\y.!plus(Y, y))) >= /\x./\y.!plus(Y, y)  because [38], by (F-Abs) 
  38] #argfun-!times#*(rec(X, _|_, /\x./\y.!plus(Y, y)), z) >= /\x.!plus(Y, x)  because [39], by (F-Abs) 
  39] #argfun-!times#*(rec(X, _|_, /\x./\y.!plus(Y, y)), z, u) >= !plus(Y, u)  because #argfun-!times# > !plus, [40] and [46], by (Copy) 
  40] #argfun-!times#*(rec(X, _|_, /\x./\y.!plus(Y, y)), z, u) >= Y  because [41], by (Select) 
  41] rec(X, _|_, /\x./\y.!plus(Y, y)) >= Y  because [42], by (Star) 
  42] rec*(X, _|_, /\x./\y.!plus(Y, y)) >= Y  because [43], by (Select) 
  43] !plus(Y, rec*(X, _|_, /\x./\y.!plus(Y, y))) >= Y  because [44], by (Star) 
  44] !plus*(Y, rec*(X, _|_, /\x./\y.!plus(Y, y))) >= Y  because [45], by (Select) 
  45] Y >= Y  by (Meta) 
  46] #argfun-!times#*(rec(X, _|_, /\x./\y.!plus(Y, y)), z, u) >= u  because [47], by (Select) 
  47] u >= u  by (Var) 

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.