We consider the system 1037.

  Alphabet:

    0 : [] --> nat 
    rec : [nat * nat * nat -> nat -> nat] --> nat 
    s : [nat] --> nat 
    v : [var] --> nat 
    xplus : [nat * nat] --> nat 
    xtimes : [nat * nat] --> nat 

  Rules:

    xplus(X, 0) => X 
    xplus(X, s(Y)) => s(xplus(X, Y)) 
    rec(0, X, /\x./\y.Y(x, y)) => X 
    rec(s(v(X)), Y, /\x./\y.Z(x, y)) => Z(v(X), rec(v(X), Y, /\z./\u.Z(z, u))) 
    xtimes(X, Y) => rec(Y, 0, /\x./\y.xplus(X, y)) 

We observe that the rules contain a first-order subset:

  xplus(X, 0) => X 
  xplus(X, s(Y)) => s(xplus(X, 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:
 || 
 ||    xplus(%X, 0) -> %X
 ||    xplus(%X, s(%Y)) -> s(xplus(%X, %Y))
 || 
 || Q is empty.
 || 
 || ----------------------------------------
 || 
 || (1) QTRSRRRProof (EQUIVALENT)
 || Used ordering:
 || Polynomial interpretation [POLO]:
 || 
 ||    POL(0) = 2
 ||    POL(s(x_1)) = 1 + x_1
 ||    POL(xplus(x_1, x_2)) = 2 + 2*x_1 + 2*x_2
 || With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
 || 
 ||    xplus(%X, 0) -> %X
 ||    xplus(%X, s(%Y)) -> s(xplus(%X, %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.

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

  Dependency Pairs P_0:

    0] rec#(s(v(X)), Y, /\x./\y.Z(x, y)) =#> Z(v(X), rec(v(X), Y, /\z./\u.Z(z, u)))   
    1] rec#(s(v(X)), Y, /\x./\y.Z(x, y)) =#> rec#(v(X), Y, /\z./\u.Z(z, u)) {Z : 2}  
    2] rec#(s(v(X)), Y, /\x./\y.Z(x, y)) =#> Z(z, u) {Z : 2}  
    3] xtimes#(X, Y) =#> rec#(Y, 0, /\x./\y.xplus(X, y))   
    4] xtimes#(X, Y) =#> xplus#(X, x)   

  Rules R_0:

    xplus(X, 0) => X 
    xplus(X, s(Y)) => s(xplus(X, Y)) 
    rec(0, X, /\x./\y.Y(x, y)) => X 
    rec(s(v(X)), Y, /\x./\y.Z(x, y)) => Z(v(X), rec(v(X), Y, /\z./\u.Z(z, u))) 
    xtimes(X, Y) => rec(Y, 0, /\x./\y.xplus(X, y)) 

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

This graph has the following strongly connected components:

  P_1:

    rec#(s(v(X)), Y, /\x./\y.Z(x, y)) =#> Z(v(X), rec(v(X), Y, /\z./\u.Z(z, u)))   
    rec#(s(v(X)), Y, /\x./\y.Z(x, y)) =#> Z(z, u) {Z : 2}  
    xtimes#(X, Y) =#> rec#(Y, 0, /\x./\y.xplus(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).

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#(s(v(X)), Y, /\x./\y.Z(x, y)) >? Z(v(X), rec(v(X), Y, /\z./\u.Z(z, u))) 
  rec#(s(v(X)), Y, /\x./\y.Z(x, y)) >? Z(~c0, ~c1) 
  xtimes#(X, Y) >? rec#(Y, 0, /\x./\y.xplus-(X, y)) 
  xplus(X, 0) >= X 
  xplus(X, s(Y)) >= s(xplus(X, Y)) 
  rec(0, X, /\x./\y.Y(x, y)) >= X 
  rec(s(v(X)), Y, /\x./\y.Z(x, y)) >= Z(v(X), rec(v(X), Y, /\z./\u.Z(z, u))) 
  xtimes(X, Y) >= rec(Y, 0, /\x./\y.xplus-(X, y)) 
  xplus-(X, Y) >= xplus(X, Y) 

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

  pi( xtimes(X, Y) ) = #argfun-xtimes#(rec(Y, 0, /\x./\y.xplus-(X, y))) 
  pi( xtimes#(X, Y) ) = #argfun-xtimes##(rec#(Y, 0, /\x./\y.xplus-(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:

  [[#argfun-xtimes##(x_1)]] = x_1 
  [[0]] = _|_ 
  [[~c0]] = _|_ 
  [[~c1]] = _|_ 

We choose Lex = {} and Mul = {#argfun-xtimes#, rec, rec#, s, v, xplus, xplus-, xtimes, xtimes#}, and the following precedence: #argfun-xtimes# > xtimes > rec# > xtimes# > xplus- > xplus > s > v > rec

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

  rec#(s(v(X)), Y, /\x./\y.Z(x, y)) >= Z(v(X), rec(v(X), Y, /\x./\y.Z(x, y))) 
  rec#(s(v(X)), Y, /\x./\y.Z(x, y)) > Z(_|_, _|_) 
  rec#(X, _|_, /\x./\y.xplus-(Y, y)) >= rec#(X, _|_, /\x./\y.xplus-(Y, y)) 
  xplus(X, _|_) >= X 
  xplus(X, s(Y)) >= s(xplus(X, Y)) 
  rec(_|_, X, /\x./\y.Y(x, y)) >= X 
  rec(s(v(X)), Y, /\x./\y.Z(x, y)) >= Z(v(X), rec(v(X), Y, /\x./\y.Z(x, y))) 
  #argfun-xtimes#(rec(X, _|_, /\x./\y.xplus-(Y, y))) >= rec(X, _|_, /\x./\y.xplus-(Y, y)) 
  xplus-(X, Y) >= xplus(X, Y) 

With these choices, we have:

  1] rec#(s(v(X)), Y, /\x./\y.Z(x, y)) >= Z(v(X), rec(v(X), Y, /\x./\y.Z(x, y)))  because [2], by (Star) 
  2] rec#*(s(v(X)), Y, /\x./\y.Z(x, y)) >= Z(v(X), rec(v(X), Y, /\x./\y.Z(x, y)))  because [3], by (Select) 
  3] Z(rec#*(s(v(X)), Y, /\x./\y.Z(x, y)), rec#*(s(v(X)), Y, /\z./\u.Z(z, u))) >= Z(v(X), rec(v(X), Y, /\x./\y.Z(x, y)))  because [4] and [11], by (Meta) 
  4] rec#*(s(v(X)), Y, /\x./\y.Z(x, y)) >= v(X)  because [5], by (Select) 
  5] s(v(X)) >= v(X)  because [6], by (Star) 
  6] s*(v(X)) >= v(X)  because s > v and [7], by (Copy) 
  7] s*(v(X)) >= X  because [8], by (Select) 
  8] v(X) >= X  because [9], by (Star) 
  9] v*(X) >= X  because [10], by (Select) 
  10] X >= X  by (Meta) 
  11] rec#*(s(v(X)), Y, /\x./\y.Z(x, y)) >= rec(v(X), Y, /\x./\y.Z(x, y))  because rec# > rec, [4], [12] and [14], by (Copy) 
  12] rec#*(s(v(X)), Y, /\x./\y.Z(x, y)) >= Y  because [13], by (Select) 
  13] Y >= Y  by (Meta) 
  14] rec#*(s(v(X)), Y, /\x./\y.Z(x, y)) >= /\x./\y.Z(x, y)  because [15], by (Select) 
  15] /\x./\z.Z(x, z) >= /\x./\z.Z(x, z)  because [16], by (Abs) 
  16] /\z.Z(y, z) >= /\z.Z(y, z)  because [17], by (Abs) 
  17] Z(y, x) >= Z(y, x)  because [18] and [19], by (Meta) 
  18] y >= y  by (Var) 
  19] x >= x  by (Var) 

  20] rec#(s(v(X)), Y, /\x./\y.Z(x, y)) > Z(_|_, _|_)  because [21], by definition 
  21] rec#*(s(v(X)), Y, /\x./\y.Z(x, y)) >= Z(_|_, _|_)  because [22], by (Select) 
  22] Z(rec#*(s(v(X)), Y, /\x./\y.Z(x, y)), rec#*(s(v(X)), Y, /\z./\u.Z(z, u))) >= Z(_|_, _|_)  because [23] and [24], by (Meta) 
  23] rec#*(s(v(X)), Y, /\x./\y.Z(x, y)) >= _|_  by (Bot) 
  24] rec#*(s(v(X)), Y, /\x./\y.Z(x, y)) >= _|_  by (Bot) 

  25] rec#(X, _|_, /\x./\y.xplus-(Y, y)) >= rec#(X, _|_, /\x./\y.xplus-(Y, y))  because rec# in Mul, [26], [27] and [28], by (Fun) 
  26] X >= X  by (Meta) 
  27] _|_ >= _|_  by (Bot) 
  28] /\x./\y.xplus-(Y, y) >= /\x./\y.xplus-(Y, y)  because [29], by (Abs) 
  29] /\y.xplus-(Y, y) >= /\y.xplus-(Y, y)  because [30], by (Abs) 
  30] xplus-(Y, x) >= xplus-(Y, x)  because xplus- in Mul, [31] and [32], by (Fun) 
  31] Y >= Y  by (Meta) 
  32] x >= x  by (Var) 

  33] xplus(X, _|_) >= X  because [34], by (Star) 
  34] xplus*(X, _|_) >= X  because [35], by (Select) 
  35] X >= X  by (Meta) 

  36] xplus(X, s(Y)) >= s(xplus(X, Y))  because [37], by (Star) 
  37] xplus*(X, s(Y)) >= s(xplus(X, Y))  because xplus > s and [38], by (Copy) 
  38] xplus*(X, s(Y)) >= xplus(X, Y)  because xplus in Mul, [39] and [40], by (Stat) 
  39] X >= X  by (Meta) 
  40] s(Y) > Y  because [41], by definition 
  41] s*(Y) >= Y  because [42], by (Select) 
  42] Y >= Y  by (Meta) 

  43] rec(_|_, X, /\x./\y.Y(x, y)) >= X  because [44], by (Star) 
  44] rec*(_|_, X, /\x./\y.Y(x, y)) >= X  because [45], by (Select) 
  45] X >= X  by (Meta) 

  46] rec(s(v(X)), Y, /\x./\y.Z(x, y)) >= Z(v(X), rec(v(X), Y, /\x./\y.Z(x, y)))  because [47], by (Star) 
  47] rec*(s(v(X)), Y, /\x./\y.Z(x, y)) >= Z(v(X), rec(v(X), Y, /\x./\y.Z(x, y)))  because [48], by (Select) 
  48] Z(rec*(s(v(X)), Y, /\x./\y.Z(x, y)), rec*(s(v(X)), Y, /\z./\u.Z(z, u))) >= Z(v(X), rec(v(X), Y, /\x./\y.Z(x, y)))  because [49] and [50], by (Meta) 
  49] rec*(s(v(X)), Y, /\x./\y.Z(x, y)) >= v(X)  because [5], by (Select) 
  50] rec*(s(v(X)), Y, /\x./\y.Z(x, y)) >= rec(v(X), Y, /\x./\y.Z(x, y))  because rec in Mul, [51], [53] and [54], by (Stat) 
  51] s(v(X)) > v(X)  because [52], by definition 
  52] s*(v(X)) >= v(X)  because s > v and [7], by (Copy) 
  53] Y >= Y  by (Meta) 
  54] /\x./\z.Z(x, z) >= /\x./\z.Z(x, z)  because [16], by (Abs) 

  55] #argfun-xtimes#(rec(X, _|_, /\x./\y.xplus-(Y, y))) >= rec(X, _|_, /\x./\y.xplus-(Y, y))  because [56], by (Star) 
  56] #argfun-xtimes#*(rec(X, _|_, /\x./\y.xplus-(Y, y))) >= rec(X, _|_, /\x./\y.xplus-(Y, y))  because [57], by (Select) 
  57] rec(X, _|_, /\x./\y.xplus-(Y, y)) >= rec(X, _|_, /\x./\y.xplus-(Y, y))  because rec in Mul, [26], [27] and [28], by (Fun) 

  58] xplus-(X, Y) >= xplus(X, Y)  because [59], by (Star) 
  59] xplus-*(X, Y) >= xplus(X, Y)  because xplus- > xplus, [60] and [62], by (Copy) 
  60] xplus-*(X, Y) >= X  because [61], by (Select) 
  61] X >= X  by (Meta) 
  62] xplus-*(X, Y) >= Y  because [63], by (Select) 
  63] Y >= Y  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, formative) by (P_2, R_0, minimal, formative), where P_2 consists of:

  rec#(s(v(X)), Y, /\x./\y.Z(x, y)) =#> Z(v(X), rec(v(X), Y, /\z./\u.Z(z, u)))   
  xtimes#(X, Y) =#> rec#(Y, 0, /\x./\y.xplus(X, y))   

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 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#(s(v(X)), Y, /\x./\y.Z(x, y)) >? Z(v(X), rec(v(X), Y, /\z./\u.Z(z, u))) 
  xtimes#(X, Y) >? rec#(Y, 0, /\x./\y.xplus-(X, y)) 
  xplus(X, 0) >= X 
  xplus(X, s(Y)) >= s(xplus(X, Y)) 
  rec(0, X, /\x./\y.Y(x, y)) >= X 
  rec(s(v(X)), Y, /\x./\y.Z(x, y)) >= Z(v(X), rec(v(X), Y, /\z./\u.Z(z, u))) 
  xtimes(X, Y) >= rec(Y, 0, /\x./\y.xplus-(X, y)) 
  xplus-(X, Y) >= xplus(X, Y) 

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

  pi( xtimes(X, Y) ) = #argfun-xtimes#(rec(Y, 0, /\x./\y.xplus-(X, y))) 
  pi( xtimes#(X, Y) ) = #argfun-xtimes##(rec#(Y, 0, /\x./\y.xplus-(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 = {#argfun-xtimes#, #argfun-xtimes##, rec, rec#, s, v, xplus, xplus-, xtimes, xtimes#}, and the following precedence: #argfun-xtimes# > #argfun-xtimes## > rec# > rec > v > xplus- > xplus > s > xtimes > xtimes#

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

  rec#(s(v(X)), Y, /\x./\y.Z(x, y)) > Z(v(X), rec(v(X), Y, /\x./\y.Z(x, y))) 
  #argfun-xtimes##(rec#(X, _|_, /\x./\y.xplus-(Y, y))) >= rec#(X, _|_, /\x./\y.xplus-(Y, y)) 
  xplus(X, _|_) >= X 
  xplus(X, s(Y)) >= s(xplus(X, Y)) 
  rec(_|_, X, /\x./\y.Y(x, y)) >= X 
  rec(s(v(X)), Y, /\x./\y.Z(x, y)) >= Z(v(X), rec(v(X), Y, /\x./\y.Z(x, y))) 
  #argfun-xtimes#(rec(X, _|_, /\x./\y.xplus-(Y, y))) >= rec(X, _|_, /\x./\y.xplus-(Y, y)) 
  xplus-(X, Y) >= xplus(X, Y) 

With these choices, we have:

  1] rec#(s(v(X)), Y, /\x./\y.Z(x, y)) > Z(v(X), rec(v(X), Y, /\x./\y.Z(x, y)))  because [2], by definition 
  2] rec#*(s(v(X)), Y, /\x./\y.Z(x, y)) >= Z(v(X), rec(v(X), Y, /\x./\y.Z(x, y)))  because [3], by (Select) 
  3] Z(rec#*(s(v(X)), Y, /\x./\y.Z(x, y)), rec#*(s(v(X)), Y, /\z./\u.Z(z, u))) >= Z(v(X), rec(v(X), Y, /\x./\y.Z(x, y)))  because [4] and [9], by (Meta) 
  4] rec#*(s(v(X)), Y, /\x./\y.Z(x, y)) >= v(X)  because [5], by (Select) 
  5] s(v(X)) >= v(X)  because [6], by (Star) 
  6] s*(v(X)) >= v(X)  because [7], by (Select) 
  7] v(X) >= v(X)  because v in Mul and [8], by (Fun) 
  8] X >= X  by (Meta) 
  9] rec#*(s(v(X)), Y, /\x./\y.Z(x, y)) >= rec(v(X), Y, /\x./\y.Z(x, y))  because rec# > rec, [4], [10] and [12], by (Copy) 
  10] rec#*(s(v(X)), Y, /\x./\y.Z(x, y)) >= Y  because [11], by (Select) 
  11] Y >= Y  by (Meta) 
  12] rec#*(s(v(X)), Y, /\x./\y.Z(x, y)) >= /\x./\y.Z(x, y)  because [13], by (Select) 
  13] /\x./\z.Z(x, z) >= /\x./\z.Z(x, z)  because [14], by (Abs) 
  14] /\z.Z(y, z) >= /\z.Z(y, z)  because [15], by (Abs) 
  15] Z(y, x) >= Z(y, x)  because [16] and [17], by (Meta) 
  16] y >= y  by (Var) 
  17] x >= x  by (Var) 

  18] #argfun-xtimes##(rec#(X, _|_, /\x./\y.xplus-(Y, y))) >= rec#(X, _|_, /\x./\y.xplus-(Y, y))  because [19], by (Star) 
  19] #argfun-xtimes##*(rec#(X, _|_, /\x./\y.xplus-(Y, y))) >= rec#(X, _|_, /\x./\y.xplus-(Y, y))  because #argfun-xtimes## > rec#, [20], [24] and [25], by (Copy) 
  20] #argfun-xtimes##*(rec#(X, _|_, /\x./\y.xplus-(Y, y))) >= X  because [21], by (Select) 
  21] rec#(X, _|_, /\x./\y.xplus-(Y, y)) >= X  because [22], by (Star) 
  22] rec#*(X, _|_, /\x./\y.xplus-(Y, y)) >= X  because [23], by (Select) 
  23] X >= X  by (Meta) 
  24] #argfun-xtimes##*(rec#(X, _|_, /\x./\y.xplus-(Y, y))) >= _|_  by (Bot) 
  25] #argfun-xtimes##*(rec#(X, _|_, /\x./\y.xplus-(Y, y))) >= /\x./\y.xplus-(Y, y)  because [26], by (F-Abs) 
  26] #argfun-xtimes##*(rec#(X, _|_, /\x./\y.xplus-(Y, y)), z) >= /\x.xplus-(Y, x)  because [27], by (F-Abs) 
  27] #argfun-xtimes##*(rec#(X, _|_, /\x./\y.xplus-(Y, y)), z, u) >= xplus-(Y, u)  because #argfun-xtimes## > xplus-, [28] and [34], by (Copy) 
  28] #argfun-xtimes##*(rec#(X, _|_, /\x./\y.xplus-(Y, y)), z, u) >= Y  because [29], by (Select) 
  29] rec#(X, _|_, /\x./\y.xplus-(Y, y)) >= Y  because [30], by (Star) 
  30] rec#*(X, _|_, /\x./\y.xplus-(Y, y)) >= Y  because [31], by (Select) 
  31] xplus-(Y, rec#*(X, _|_, /\x./\y.xplus-(Y, y))) >= Y  because [32], by (Star) 
  32] xplus-*(Y, rec#*(X, _|_, /\x./\y.xplus-(Y, y))) >= Y  because [33], by (Select) 
  33] Y >= Y  by (Meta) 
  34] #argfun-xtimes##*(rec#(X, _|_, /\x./\y.xplus-(Y, y)), z, u) >= u  because [35], by (Select) 
  35] u >= u  by (Var) 

  36] xplus(X, _|_) >= X  because [37], by (Star) 
  37] xplus*(X, _|_) >= X  because [38], by (Select) 
  38] X >= X  by (Meta) 

  39] xplus(X, s(Y)) >= s(xplus(X, Y))  because [40], by (Star) 
  40] xplus*(X, s(Y)) >= s(xplus(X, Y))  because xplus > s and [41], by (Copy) 
  41] xplus*(X, s(Y)) >= xplus(X, Y)  because xplus in Mul, [42] and [43], by (Stat) 
  42] X >= X  by (Meta) 
  43] s(Y) > Y  because [44], by definition 
  44] s*(Y) >= Y  because [45], by (Select) 
  45] Y >= Y  by (Meta) 

  46] rec(_|_, X, /\x./\y.Y(x, y)) >= X  because [47], by (Star) 
  47] rec*(_|_, X, /\x./\y.Y(x, y)) >= X  because [48], by (Select) 
  48] X >= X  by (Meta) 

  49] rec(s(v(X)), Y, /\x./\y.Z(x, y)) >= Z(v(X), rec(v(X), Y, /\x./\y.Z(x, y)))  because [50], by (Star) 
  50] rec*(s(v(X)), Y, /\x./\y.Z(x, y)) >= Z(v(X), rec(v(X), Y, /\x./\y.Z(x, y)))  because [51], by (Select) 
  51] Z(rec*(s(v(X)), Y, /\x./\y.Z(x, y)), rec*(s(v(X)), Y, /\z./\u.Z(z, u))) >= Z(v(X), rec(v(X), Y, /\x./\y.Z(x, y)))  because [52] and [53], by (Meta) 
  52] rec*(s(v(X)), Y, /\x./\y.Z(x, y)) >= v(X)  because [5], by (Select) 
  53] rec*(s(v(X)), Y, /\x./\y.Z(x, y)) >= rec(v(X), Y, /\x./\y.Z(x, y))  because rec in Mul, [54], [56] and [57], by (Stat) 
  54] s(v(X)) > v(X)  because [55], by definition 
  55] s*(v(X)) >= v(X)  because [7], by (Select) 
  56] Y >= Y  by (Meta) 
  57] /\x./\z.Z(x, z) >= /\x./\z.Z(x, z)  because [14], by (Abs) 

  58] #argfun-xtimes#(rec(X, _|_, /\x./\y.xplus-(Y, y))) >= rec(X, _|_, /\x./\y.xplus-(Y, y))  because [59], by (Star) 
  59] #argfun-xtimes#*(rec(X, _|_, /\x./\y.xplus-(Y, y))) >= rec(X, _|_, /\x./\y.xplus-(Y, y))  because #argfun-xtimes# > rec, [60], [63] and [64], by (Copy) 
  60] #argfun-xtimes#*(rec(X, _|_, /\x./\y.xplus-(Y, y))) >= X  because [61], by (Select) 
  61] rec(X, _|_, /\x./\y.xplus-(Y, y)) >= X  because [62], by (Star) 
  62] rec*(X, _|_, /\x./\y.xplus-(Y, y)) >= X  because [23], by (Select) 
  63] #argfun-xtimes#*(rec(X, _|_, /\x./\y.xplus-(Y, y))) >= _|_  by (Bot) 
  64] #argfun-xtimes#*(rec(X, _|_, /\x./\y.xplus-(Y, y))) >= /\x./\y.xplus-(Y, y)  because [65], by (F-Abs) 
  65] #argfun-xtimes#*(rec(X, _|_, /\x./\y.xplus-(Y, y)), z) >= /\x.xplus-(Y, x)  because [66], by (F-Abs) 
  66] #argfun-xtimes#*(rec(X, _|_, /\x./\y.xplus-(Y, y)), z, u) >= xplus-(Y, u)  because #argfun-xtimes# > xplus-, [67] and [73], by (Copy) 
  67] #argfun-xtimes#*(rec(X, _|_, /\x./\y.xplus-(Y, y)), z, u) >= Y  because [68], by (Select) 
  68] rec(X, _|_, /\x./\y.xplus-(Y, y)) >= Y  because [69], by (Star) 
  69] rec*(X, _|_, /\x./\y.xplus-(Y, y)) >= Y  because [70], by (Select) 
  70] xplus-(Y, rec*(X, _|_, /\x./\y.xplus-(Y, y))) >= Y  because [71], by (Star) 
  71] xplus-*(Y, rec*(X, _|_, /\x./\y.xplus-(Y, y))) >= Y  because [72], by (Select) 
  72] Y >= Y  by (Meta) 
  73] #argfun-xtimes#*(rec(X, _|_, /\x./\y.xplus-(Y, y)), z, u) >= u  because [74], by (Select) 
  74] u >= u  by (Var) 

  75] xplus-(X, Y) >= xplus(X, Y)  because [76], by (Star) 
  76] xplus-*(X, Y) >= xplus(X, Y)  because xplus- > xplus, [77] and [79], by (Copy) 
  77] xplus-*(X, Y) >= X  because [78], by (Select) 
  78] X >= X  by (Meta) 
  79] xplus-*(X, Y) >= Y  because [80], by (Select) 
  80] Y >= Y  by (Meta) 

By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_2, R_0, minimal, formative) by (P_3, R_0, minimal, formative), where P_3 consists of:

  xtimes#(X, Y) =#> rec#(Y, 0, /\x./\y.xplus(X, y))   

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 place the elements of P in a dependency graph approximation G (see e.g. [Kop12, Thm. 7.27, 7.29], as follows:

    * 0 :  

This graph has no strongly connected components.  By [Kop12, Thm. 7.31], this implies finiteness of the dependency pair problem.

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.