We consider the system h47.

  Alphabet:

    0 : [] --> nat 
    rec : [nat * nat * nat -> nat -> nat] --> nat 
    s : [nat] --> nat 
    xap : [nat -> nat -> nat * nat] --> nat -> nat 
    xplus : [nat * nat] --> nat 
    xtimes : [nat * nat] --> nat 
    yap : [nat -> nat * nat] --> nat 

  Rules:

    xplus(x, 0) => x 
    xplus(x, s(y)) => s(xplus(x, y)) 
    rec(0, x, /\y./\z.yap(xap(f, y), z)) => x 
    rec(s(x), y, /\z./\u.yap(xap(f, z), u)) => yap(xap(f, x), rec(x, y, /\v./\w.yap(xap(f, v), w))) 
    xtimes(x, y) => rec(y, 0, /\z./\u.xplus(x, u)) 
    xap(f, x) => f x 
    yap(f, x) => f x 

This AFS is converted to an AFSM simply by replacing all free variables by meta-variables (with arity 0).

Symbol xap is an encoding for application that is only used in innocuous ways.  We can simplify the program (without losing non-termination) by removing it.  This gives:

  Alphabet:

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

  Rules:

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

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 finitely branching.  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 Ce-terminating when seen as a many-sorted first-order TRS.

According to the external first-order termination prover, this system is indeed Ce-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))
 ||    ~PAIR(%X, %Y) -> %X
 ||    ~PAIR(%X, %Y) -> %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
 ||    POL(~PAIR(x_1, x_2)) = 2 + x_1 + 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))
 ||    ~PAIR(%X, %Y) -> %X
 ||    ~PAIR(%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, all):

  Dependency Pairs P_0:

    0] rec#(s(X), Y, /\x./\y.yap(F(x), y)) =#> yap#(F(X), rec(X, Y, /\z./\u.yap(F(z), u)))   
    1] rec#(s(X), Y, /\x./\y.yap(F(x), y)) =#> F(X)   
    2] rec#(s(X), Y, /\x./\y.yap(F(x), y)) =#> rec#(X, Y, /\z./\u.yap(F(z), u))   
    3] rec#(s(X), Y, /\x./\y.yap(F(x), y)) =#> yap#(F(z), u)   
    4] rec#(s(X), Y, /\x./\y.yap(F(x), y)) =#> F(z)   
    5] xtimes#(X, Y) =#> rec#(Y, 0, /\x./\y.xplus(X, y))   
    6] xtimes#(X, Y) =#> xplus#(X, x)   
    7] yap#(F, X) =#> F(X)   

  Rules R_0:

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

Thus, the original system is terminating if (P_0, R_0, minimal, all) is finite.

We consider the dependency pair problem (P_0, R_0, minimal, all).

We place the elements of P in a dependency graph approximation G (see e.g. [Kop12, Thm. 7.27, 7.29], as follows:

    * 0 : 7 
    * 1 : 0, 1, 2, 3, 4, 5, 6, 7 
    * 2 : 0, 1, 2, 3, 4 
    * 3 :  
    * 4 : 0, 1, 2, 3, 4, 5, 6, 7 
    * 5 : 0, 1, 2, 3, 4 
    * 6 :  
    * 7 : 0, 1, 2, 3, 4, 5, 6, 7 

This graph has the following strongly connected components:

  P_1:

    rec#(s(X), Y, /\x./\y.yap(F(x), y)) =#> yap#(F(X), rec(X, Y, /\z./\u.yap(F(z), u)))   
    rec#(s(X), Y, /\x./\y.yap(F(x), y)) =#> F(X)   
    rec#(s(X), Y, /\x./\y.yap(F(x), y)) =#> rec#(X, Y, /\z./\u.yap(F(z), u))   
    rec#(s(X), Y, /\x./\y.yap(F(x), y)) =#> F(z)   
    xtimes#(X, Y) =#> rec#(Y, 0, /\x./\y.xplus(X, y))   
    yap#(F, X) =#> F(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, all) is finite.

We consider the dependency pair problem (P_1, R_0, minimal, all).

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

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( yap#(F, X) ) = #argfun-yap##(F 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-xtimes##(x_1)]] = x_1 
  [[0]] = _|_ 
  [[~c0]] = _|_ 
  [[~c1]] = _|_ 
  [[~c2]] = _|_ 

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

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

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

With these choices, we have:

  1] rec#(s(X), Y, /\x./\y.yap(F(x), y)) >= #argfun-yap##(@_{o -> o}(F(X), rec(X, Y, /\x./\y.yap(F(x), y))))  because [2], by (Star) 
  2] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= #argfun-yap##(@_{o -> o}(F(X), rec(X, Y, /\x./\y.yap(F(x), y))))  because [3], by (Select) 
  3] yap(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= #argfun-yap##(@_{o -> o}(F(X), rec(X, Y, /\x./\y.yap(F(x), y))))  because [4], by (Star) 
  4] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= #argfun-yap##(@_{o -> o}(F(X), rec(X, Y, /\x./\y.yap(F(x), y))))  because yap > #argfun-yap## and [5], by (Copy) 
  5] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= @_{o -> o}(F(X), rec(X, Y, /\x./\y.yap(F(x), y)))  because yap > @_{o -> o}, [6] and [12], by (Copy) 
  6] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= F(X)  because [7], by (Select) 
  7] F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(X)  because [8], by (Meta) 
  8] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= X  because [9], by (Select) 
  9] s(X) >= X  because [10], by (Star) 
  10] s*(X) >= X  because [11], by (Select) 
  11] X >= X  by (Meta) 
  12] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= rec(X, Y, /\x./\y.yap(F(x), y))  because [13], by (Select) 
  13] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= rec(X, Y, /\x./\y.yap(F(x), y))  because rec# = rec, rec# in Mul, [14], [16] and [17], by (Stat) 
  14] s(X) > X  because [15], by definition 
  15] s*(X) >= X  because [11], by (Select) 
  16] Y >= Y  by (Meta) 
  17] /\x./\z.yap(F(x), z) >= /\x./\z.yap(F(x), z)  because [18], by (Abs) 
  18] /\z.yap(F(y), z) >= /\z.yap(F(y), z)  because [19], by (Abs) 
  19] yap(F(y), x) >= yap(F(y), x)  because yap in Mul, [20] and [22], by (Fun) 
  20] F(y) >= F(y)  because [21], by (Meta) 
  21] y >= y  by (Var) 
  22] x >= x  by (Var) 

  23] rec#(s(X), Y, /\x./\y.yap(F(x), y)) >= @_{o -> o}(F(X), _|_)  because [24], by (Star) 
  24] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= @_{o -> o}(F(X), _|_)  because [25], by (Select) 
  25] yap(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= @_{o -> o}(F(X), _|_)  because [26], by (Star) 
  26] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= @_{o -> o}(F(X), _|_)  because yap > @_{o -> o}, [6] and [27], by (Copy) 
  27] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= _|_  by (Bot) 

  28] rec#(s(X), Y, /\x./\y.yap(F(x), y)) >= rec#(X, Y, /\x./\y.yap(F(x), y))  because rec# in Mul, [29], [16] and [17], by (Fun) 
  29] s(X) >= X  because [15], by (Star) 

  30] rec#(s(X), Y, /\x./\y.yap(F(x), y)) > @_{o -> o}(F(_|_), _|_)  because [31], by definition 
  31] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= @_{o -> o}(F(_|_), _|_)  because [32], by (Select) 
  32] yap(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= @_{o -> o}(F(_|_), _|_)  because [33], by (Star) 
  33] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= @_{o -> o}(F(_|_), _|_)  because yap > @_{o -> o}, [34] and [37], by (Copy) 
  34] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= F(_|_)  because [35], by (Select) 
  35] F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(_|_)  because [36], by (Meta) 
  36] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= _|_  by (Bot) 
  37] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= _|_  by (Bot) 

  38] rec#(X, _|_, /\x./\y.xplus(Y, y)) >= rec#(X, _|_, /\x./\y.xplus(Y, y))  because rec# in Mul, [39], [40] and [41], by (Fun) 
  39] X >= X  by (Meta) 
  40] _|_ >= _|_  by (Bot) 
  41] /\x./\y.xplus(Y, y) >= /\x./\y.xplus(Y, y)  because [42], by (Abs) 
  42] /\y.xplus(Y, y) >= /\y.xplus(Y, y)  because [43], by (Abs) 
  43] xplus(Y, x) >= xplus(Y, x)  because xplus in Mul, [44] and [45], by (Fun) 
  44] Y >= Y  by (Meta) 
  45] x >= x  by (Var) 

  46] #argfun-yap##(@_{o -> o}(F, X)) >= @_{o -> o}(F, X)  because [47], by (Star) 
  47] #argfun-yap##*(@_{o -> o}(F, X)) >= @_{o -> o}(F, X)  because [48], by (Select) 
  48] @_{o -> o}(F, X) >= @_{o -> o}(F, X)  because @_{o -> o} in Mul, [49] and [50], by (Fun) 
  49] F >= F  by (Meta) 
  50] X >= X  by (Meta) 

  51] xplus(X, _|_) >= X  because [52], by (Star) 
  52] xplus*(X, _|_) >= X  because [53], by (Select) 
  53] X >= X  by (Meta) 

  54] xplus(X, s(Y)) >= s(xplus(X, Y))  because [55], by (Star) 
  55] xplus*(X, s(Y)) >= s(xplus(X, Y))  because xplus > s and [56], by (Copy) 
  56] xplus*(X, s(Y)) >= xplus(X, Y)  because xplus in Mul, [57] and [58], by (Stat) 
  57] X >= X  by (Meta) 
  58] s(Y) > Y  because [59], by definition 
  59] s*(Y) >= Y  because [60], by (Select) 
  60] Y >= Y  by (Meta) 

  61] rec(_|_, X, /\x./\y.yap(F(x), y)) >= X  because [62], by (Star) 
  62] rec*(_|_, X, /\x./\y.yap(F(x), y)) >= X  because [63], by (Select) 
  63] X >= X  by (Meta) 

  64] rec(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y)))  because [65], by (Star) 
  65] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y)))  because rec > yap, [66] and [77], by (Copy) 
  66] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= F(X)  because [67], by (Select) 
  67] /\x.yap(F(rec*(s(X), Y, /\y./\z.yap(F(y), z))), x) >= F(X)  because [68], by (Eta)[Kop13:2] 
  68] F(rec*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(X)  because [69], by (Meta) 
  69] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= X  because [70], by (Select) 
  70] yap(F(rec*(s(X), Y, /\x./\y.yap(F(x), y))), rec*(s(X), Y, /\z./\u.yap(F(z), u))) >= X  because [71], by (Star) 
  71] yap*(F(rec*(s(X), Y, /\x./\y.yap(F(x), y))), rec*(s(X), Y, /\z./\u.yap(F(z), u))) >= X  because [72], by (Select) 
  72] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= X  because [73], by (Select) 
  73] yap(F(rec*(s(X), Y, /\x./\y.yap(F(x), y))), rec*(s(X), Y, /\z./\u.yap(F(z), u))) >= X  because [74], by (Star) 
  74] yap*(F(rec*(s(X), Y, /\x./\y.yap(F(x), y))), rec*(s(X), Y, /\z./\u.yap(F(z), u))) >= X  because [75], by (Select) 
  75] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= X  because [76], by (Select) 
  76] s(X) >= X  because [15], by (Star) 
  77] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= rec(X, Y, /\x./\y.yap(F(x), y))  because rec in Mul, [14], [16] and [17], by (Stat) 

  78] xtimes(X, Y) >= rec(Y, _|_, /\x./\y.xplus(X, y))  because [79], by (Star) 
  79] xtimes*(X, Y) >= rec(Y, _|_, /\x./\y.xplus(X, y))  because xtimes > rec, [80], [81] and [82], by (Copy) 
  80] xtimes*(X, Y) >= Y  because [39], by (Select) 
  81] xtimes*(X, Y) >= _|_  by (Bot) 
  82] xtimes*(X, Y) >= /\y./\z.xplus(X, z)  because [83], by (F-Abs) 
  83] xtimes*(X, Y, x) >= /\z.xplus(X, z)  because [84], by (F-Abs) 
  84] xtimes*(X, Y, x, y) >= xplus(X, y)  because xtimes > xplus, [85] and [86], by (Copy) 
  85] xtimes*(X, Y, x, y) >= X  because [44], by (Select) 
  86] xtimes*(X, Y, x, y) >= y  because [87], by (Select) 
  87] y >= y  by (Var) 

  88] yap(F, X) >= @_{o -> o}(F, X)  because [89], by (Star) 
  89] yap*(F, X) >= @_{o -> o}(F, X)  because yap > @_{o -> o}, [90] and [91], by (Copy) 
  90] yap*(F, X) >= F  because [49], by (Select) 
  91] yap*(F, X) >= X  because [50], by (Select) 

  92] rec(X, Y, F) >= rec#(X, Y, F)  because rec = rec#, rec in Mul, [93], [94] and [95], by (Fun) 
  93] X >= X  by (Meta) 
  94] Y >= Y  by (Meta) 
  95] F >= F  by (Meta) 

  96] xtimes(X, Y) >= rec#(Y, _|_, /\x./\y.xplus(X, y))  because [97], by (Star) 
  97] xtimes*(X, Y) >= rec#(Y, _|_, /\x./\y.xplus(X, y))  because xtimes > rec#, [98], [100] and [101], by (Copy) 
  98] xtimes*(X, Y) >= Y  because [99], by (Select) 
  99] Y >= Y  by (Meta) 
  100] xtimes*(X, Y) >= _|_  by (Bot) 
  101] xtimes*(X, Y) >= /\y./\z.xplus(X, z)  because [102], by (F-Abs) 
  102] xtimes*(X, Y, x) >= /\z.xplus(X, z)  because [103], by (F-Abs) 
  103] xtimes*(X, Y, x, y) >= xplus(X, y)  because xtimes > xplus, [104] and [106], by (Copy) 
  104] xtimes*(X, Y, x, y) >= X  because [105], by (Select) 
  105] X >= X  by (Meta) 
  106] xtimes*(X, Y, x, y) >= y  because [107], by (Select) 
  107] y >= y  by (Var) 

  108] yap(F, X) >= #argfun-yap##(@_{o -> o}(F, X))  because [109], by (Star) 
  109] yap*(F, X) >= #argfun-yap##(@_{o -> o}(F, X))  because yap > #argfun-yap## and [110], by (Copy) 
  110] yap*(F, X) >= @_{o -> o}(F, X)  because yap > @_{o -> o}, [111] and [113], by (Copy) 
  111] yap*(F, X) >= F  because [112], by (Select) 
  112] F >= F  by (Meta) 
  113] yap*(F, X) >= X  because [114], by (Select) 
  114] X >= X  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, all) by (P_2, R_0, minimal, all), where P_2 consists of:

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

Thus, the original system is terminating if (P_2, R_0, minimal, all) is finite.

We consider the dependency pair problem (P_2, R_0, minimal, all).

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

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( yap#(F, X) ) = #argfun-yap##(F 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-xtimes##(x_1)]] = x_1 
  [[0]] = _|_ 
  [[~c0]] = _|_ 

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

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

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

With these choices, we have:

  1] rec#(s(X), Y, /\x./\y.yap(F(x), y)) >= #argfun-yap##(@_{o -> o}(F(X), rec(X, Y, /\x./\y.yap(F(x), y))))  because [2], by (Star) 
  2] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= #argfun-yap##(@_{o -> o}(F(X), rec(X, Y, /\x./\y.yap(F(x), y))))  because [3], by (Select) 
  3] yap(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= #argfun-yap##(@_{o -> o}(F(X), rec(X, Y, /\x./\y.yap(F(x), y))))  because [4], by (Star) 
  4] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= #argfun-yap##(@_{o -> o}(F(X), rec(X, Y, /\x./\y.yap(F(x), y))))  because yap > #argfun-yap## and [5], by (Copy) 
  5] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= @_{o -> o}(F(X), rec(X, Y, /\x./\y.yap(F(x), y)))  because [6], by (Select) 
  6] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= @_{o -> o}(F(X), rec(X, Y, /\x./\y.yap(F(x), y)))  because rec# > @_{o -> o}, [7] and [14], by (Copy) 
  7] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= F(X)  because [8], by (Select) 
  8] /\x.yap(F(rec#*(s(X), Y, /\y./\z.yap(F(y), z))), x) >= F(X)  because [9], by (Eta)[Kop13:2] 
  9] F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(X)  because [10], by (Meta) 
  10] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= X  because [11], by (Select) 
  11] s(X) >= X  because [12], by (Star) 
  12] s*(X) >= X  because [13], by (Select) 
  13] X >= X  by (Meta) 
  14] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= rec(X, Y, /\x./\y.yap(F(x), y))  because rec# = rec, rec# in Mul, [15], [17] and [18], by (Stat) 
  15] s(X) > X  because [16], by definition 
  16] s*(X) >= X  because [13], by (Select) 
  17] Y >= Y  by (Meta) 
  18] /\x./\z.yap(F(x), z) >= /\x./\z.yap(F(x), z)  because [19], by (Abs) 
  19] /\z.yap(F(y), z) >= /\z.yap(F(y), z)  because [20], by (Abs) 
  20] yap(F(y), x) >= yap(F(y), x)  because yap in Mul, [21] and [23], by (Fun) 
  21] F(y) >= F(y)  because [22], by (Meta) 
  22] y >= y  by (Var) 
  23] x >= x  by (Var) 

  24] rec#(s(X), Y, /\x./\y.yap(F(x), y)) >= @_{o -> o}(F(X), _|_)  because [25], by (Star) 
  25] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= @_{o -> o}(F(X), _|_)  because [26], by (Select) 
  26] yap(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= @_{o -> o}(F(X), _|_)  because [27], by (Star) 
  27] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= @_{o -> o}(F(X), _|_)  because yap > @_{o -> o}, [28] and [29], by (Copy) 
  28] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= F(X)  because [9], by (Select) 
  29] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= _|_  by (Bot) 

  30] rec#(s(X), Y, /\x./\y.yap(F(x), y)) >= rec#(X, Y, /\x./\y.yap(F(x), y))  because [31], by (Star) 
  31] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= rec#(X, Y, /\x./\y.yap(F(x), y))  because rec# in Mul, [15], [17] and [18], by (Stat) 

  32] rec#(X, _|_, /\x./\y.xplus(Y, y)) >= rec#(X, _|_, /\x./\y.xplus(Y, y))  because rec# in Mul, [33], [34] and [35], by (Fun) 
  33] X >= X  by (Meta) 
  34] _|_ >= _|_  by (Bot) 
  35] /\x./\y.xplus(Y, y) >= /\x./\y.xplus(Y, y)  because [36], by (Abs) 
  36] /\y.xplus(Y, y) >= /\y.xplus(Y, y)  because [37], by (Abs) 
  37] xplus(Y, x) >= xplus(Y, x)  because xplus in Mul, [38] and [39], by (Fun) 
  38] Y >= Y  by (Meta) 
  39] x >= x  by (Var) 

  40] #argfun-yap##(@_{o -> o}(F, X)) > @_{o -> o}(F, X)  because [41], by definition 
  41] #argfun-yap##*(@_{o -> o}(F, X)) >= @_{o -> o}(F, X)  because [42], by (Select) 
  42] @_{o -> o}(F, X) >= @_{o -> o}(F, X)  because @_{o -> o} in Mul, [43] and [44], by (Fun) 
  43] F >= F  by (Meta) 
  44] X >= X  by (Meta) 

  45] xplus(X, _|_) >= X  because [46], by (Star) 
  46] xplus*(X, _|_) >= X  because [47], by (Select) 
  47] X >= X  by (Meta) 

  48] xplus(X, s(Y)) >= s(xplus(X, Y))  because [49], by (Star) 
  49] xplus*(X, s(Y)) >= s(xplus(X, Y))  because xplus > s and [50], by (Copy) 
  50] xplus*(X, s(Y)) >= xplus(X, Y)  because xplus in Mul, [51] and [52], by (Stat) 
  51] X >= X  by (Meta) 
  52] s(Y) > Y  because [53], by definition 
  53] s*(Y) >= Y  because [54], by (Select) 
  54] Y >= Y  by (Meta) 

  55] rec(_|_, X, /\x./\y.yap(F(x), y)) >= X  because [56], by (Star) 
  56] rec*(_|_, X, /\x./\y.yap(F(x), y)) >= X  because [57], by (Select) 
  57] X >= X  by (Meta) 

  58] rec(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y)))  because [59], by (Star) 
  59] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y)))  because rec > yap, [60] and [64], by (Copy) 
  60] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= F(X)  because [61], by (Select) 
  61] /\x.yap(F(rec*(s(X), Y, /\y./\z.yap(F(y), z))), x) >= F(X)  because [62], by (Eta)[Kop13:2] 
  62] F(rec*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(X)  because [63], by (Meta) 
  63] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= X  because [11], by (Select) 
  64] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= rec(X, Y, /\x./\y.yap(F(x), y))  because rec in Mul, [15], [17] and [18], by (Stat) 

  65] xtimes(X, Y) >= rec(Y, _|_, /\x./\y.xplus(X, y))  because [66], by (Star) 
  66] xtimes*(X, Y) >= rec(Y, _|_, /\x./\y.xplus(X, y))  because xtimes > rec, [67], [68] and [69], by (Copy) 
  67] xtimes*(X, Y) >= Y  because [33], by (Select) 
  68] xtimes*(X, Y) >= _|_  by (Bot) 
  69] xtimes*(X, Y) >= /\y./\z.xplus(X, z)  because [70], by (F-Abs) 
  70] xtimes*(X, Y, x) >= /\z.xplus(X, z)  because [71], by (F-Abs) 
  71] xtimes*(X, Y, x, y) >= xplus(X, y)  because xtimes > xplus, [72] and [73], by (Copy) 
  72] xtimes*(X, Y, x, y) >= X  because [38], by (Select) 
  73] xtimes*(X, Y, x, y) >= y  because [74], by (Select) 
  74] y >= y  by (Var) 

  75] yap(F, X) >= @_{o -> o}(F, X)  because [76], by (Star) 
  76] yap*(F, X) >= @_{o -> o}(F, X)  because yap > @_{o -> o}, [77] and [78], by (Copy) 
  77] yap*(F, X) >= F  because [43], by (Select) 
  78] yap*(F, X) >= X  because [44], by (Select) 

  79] rec(X, Y, F) >= rec#(X, Y, F)  because rec = rec#, rec in Mul, [80], [81] and [82], by (Fun) 
  80] X >= X  by (Meta) 
  81] Y >= Y  by (Meta) 
  82] F >= F  by (Meta) 

  83] xtimes(X, Y) >= rec#(Y, _|_, /\x./\y.xplus(X, y))  because [84], by (Star) 
  84] xtimes*(X, Y) >= rec#(Y, _|_, /\x./\y.xplus(X, y))  because xtimes > rec#, [85], [87] and [88], by (Copy) 
  85] xtimes*(X, Y) >= Y  because [86], by (Select) 
  86] Y >= Y  by (Meta) 
  87] xtimes*(X, Y) >= _|_  by (Bot) 
  88] xtimes*(X, Y) >= /\y./\z.xplus(X, z)  because [89], by (F-Abs) 
  89] xtimes*(X, Y, x) >= /\z.xplus(X, z)  because [90], by (F-Abs) 
  90] xtimes*(X, Y, x, y) >= xplus(X, y)  because xtimes > xplus, [91] and [93], by (Copy) 
  91] xtimes*(X, Y, x, y) >= X  because [92], by (Select) 
  92] X >= X  by (Meta) 
  93] xtimes*(X, Y, x, y) >= y  because [94], by (Select) 
  94] y >= y  by (Var) 

  95] yap(F, X) >= #argfun-yap##(@_{o -> o}(F, X))  because [96], by (Star) 
  96] yap*(F, X) >= #argfun-yap##(@_{o -> o}(F, X))  because yap > #argfun-yap## and [97], by (Copy) 
  97] yap*(F, X) >= @_{o -> o}(F, X)  because yap > @_{o -> o}, [98] and [100], by (Copy) 
  98] yap*(F, X) >= F  because [99], by (Select) 
  99] F >= F  by (Meta) 
  100] yap*(F, X) >= X  because [101], by (Select) 
  101] X >= X  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, all) by (P_3, R_0, minimal, all), where P_3 consists of:

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

Thus, the original system is terminating if (P_3, R_0, minimal, all) is finite.

We consider the dependency pair problem (P_3, R_0, minimal, all).

We place the elements of P in a dependency graph approximation G (see e.g. [Kop12, Thm. 7.27, 7.29], as follows:

    * 0 :  
    * 1 : 0, 1, 2, 3 
    * 2 : 0, 1, 2 
    * 3 : 0, 1, 2 

This graph has the following strongly connected components:

  P_4:

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

By [Kop12, Thm. 7.31], we may replace any dependency pair problem (P_3, R_0, m, f) by (P_4, R_0, m, f).

Thus, the original system is terminating if (P_4, R_0, minimal, all) is finite.

We consider the dependency pair problem (P_4, R_0, minimal, all).

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

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]] = _|_ 
  [[~c0]] = _|_ 

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

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

  rec#(s(X), Y, /\x./\y.yap(F(x), y)) >= @_{o -> o}(F(X), _|_) 
  rec#(s(X), Y, /\x./\y.yap(F(x), y)) >= rec#(X, Y, /\x./\y.yap(F(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.yap(F(x), y)) >= X 
  rec(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) 
  xtimes(X, Y) >= rec(Y, _|_, /\x./\y.xplus(X, y)) 
  yap(F, X) >= @_{o -> o}(F, X) 
  rec(X, Y, F) >= rec#(X, Y, F) 
  xtimes(X, Y) >= #argfun-xtimes##(rec#(Y, _|_, /\x./\y.xplus(X, y))) 

With these choices, we have:

  1] rec#(s(X), Y, /\x./\y.yap(F(x), y)) >= @_{o -> o}(F(X), _|_)  because [2], by (Star) 
  2] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= @_{o -> o}(F(X), _|_)  because [3], by (Select) 
  3] yap(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= @_{o -> o}(F(X), _|_)  because [4], by (Star) 
  4] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= @_{o -> o}(F(X), _|_)  because yap > @_{o -> o}, [5] and [11], by (Copy) 
  5] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= F(X)  because [6], by (Select) 
  6] F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(X)  because [7], by (Meta) 
  7] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= X  because [8], by (Select) 
  8] s(X) >= X  because [9], by (Star) 
  9] s*(X) >= X  because [10], by (Select) 
  10] X >= X  by (Meta) 
  11] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= _|_  by (Bot) 

  12] rec#(s(X), Y, /\x./\y.yap(F(x), y)) >= rec#(X, Y, /\x./\y.yap(F(x), y))  because [13], by (Star) 
  13] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= rec#(X, Y, /\x./\y.yap(F(x), y))  because rec# in Mul, [14], [16] and [17], by (Stat) 
  14] s(X) > X  because [15], by definition 
  15] s*(X) >= X  because [10], by (Select) 
  16] Y >= Y  by (Meta) 
  17] /\x./\z.yap(F(x), z) >= /\x./\z.yap(F(x), z)  because [18], by (Abs) 
  18] /\z.yap(F(y), z) >= /\z.yap(F(y), z)  because [19], by (Abs) 
  19] yap(F(y), x) >= yap(F(y), x)  because yap in Mul, [20] and [22], by (Fun) 
  20] F(y) >= F(y)  because [21], by (Meta) 
  21] y >= y  by (Var) 
  22] x >= x  by (Var) 

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

  41] xplus(X, _|_) >= X  because [42], by (Star) 
  42] xplus*(X, _|_) >= X  because [43], by (Select) 
  43] X >= X  by (Meta) 

  44] xplus(X, s(Y)) >= s(xplus(X, Y))  because [45], by (Star) 
  45] xplus*(X, s(Y)) >= s(xplus(X, Y))  because xplus > s and [46], by (Copy) 
  46] xplus*(X, s(Y)) >= xplus(X, Y)  because xplus in Mul, [47] and [48], by (Stat) 
  47] X >= X  by (Meta) 
  48] s(Y) > Y  because [49], by definition 
  49] s*(Y) >= Y  because [50], by (Select) 
  50] Y >= Y  by (Meta) 

  51] rec(_|_, X, /\x./\y.yap(F(x), y)) >= X  because [52], by (Star) 
  52] rec*(_|_, X, /\x./\y.yap(F(x), y)) >= X  because [53], by (Select) 
  53] X >= X  by (Meta) 

  54] rec(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y)))  because [55], by (Star) 
  55] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y)))  because rec > yap, [56] and [60], by (Copy) 
  56] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= F(X)  because [57], by (Select) 
  57] /\x.yap(F(rec*(s(X), Y, /\y./\z.yap(F(y), z))), x) >= F(X)  because [58], by (Eta)[Kop13:2] 
  58] F(rec*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(X)  because [59], by (Meta) 
  59] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= X  because [8], by (Select) 
  60] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= rec(X, Y, /\x./\y.yap(F(x), y))  because rec in Mul, [14], [16] and [17], by (Stat) 

  61] xtimes(X, Y) >= rec(Y, _|_, /\x./\y.xplus(X, y))  because [62], by (Star) 
  62] xtimes*(X, Y) >= rec(Y, _|_, /\x./\y.xplus(X, y))  because xtimes > rec, [63], [64] and [65], by (Copy) 
  63] xtimes*(X, Y) >= Y  because [28], by (Select) 
  64] xtimes*(X, Y) >= _|_  by (Bot) 
  65] xtimes*(X, Y) >= /\y./\z.xplus(X, z)  because [66], by (F-Abs) 
  66] xtimes*(X, Y, x) >= /\z.xplus(X, z)  because [67], by (F-Abs) 
  67] xtimes*(X, Y, x, y) >= xplus(X, y)  because xtimes > xplus, [68] and [69], by (Copy) 
  68] xtimes*(X, Y, x, y) >= X  because [38], by (Select) 
  69] xtimes*(X, Y, x, y) >= y  because [70], by (Select) 
  70] y >= y  by (Var) 

  71] yap(F, X) >= @_{o -> o}(F, X)  because [72], by (Star) 
  72] yap*(F, X) >= @_{o -> o}(F, X)  because yap > @_{o -> o}, [73] and [75], by (Copy) 
  73] yap*(F, X) >= F  because [74], by (Select) 
  74] F >= F  by (Meta) 
  75] yap*(F, X) >= X  because [76], by (Select) 
  76] X >= X  by (Meta) 

  77] rec(X, Y, F) >= rec#(X, Y, F)  because [78], by (Star) 
  78] rec*(X, Y, F) >= rec#(X, Y, F)  because rec > rec#, [79], [81] and [83], by (Copy) 
  79] rec*(X, Y, F) >= X  because [80], by (Select) 
  80] X >= X  by (Meta) 
  81] rec*(X, Y, F) >= Y  because [82], by (Select) 
  82] Y >= Y  by (Meta) 
  83] rec*(X, Y, F) >= F  because [84], by (Select) 
  84] F >= F  by (Meta) 

  85] xtimes(X, Y) >= #argfun-xtimes##(rec#(Y, _|_, /\x./\y.xplus(X, y)))  because [86], by (Star) 
  86] xtimes*(X, Y) >= #argfun-xtimes##(rec#(Y, _|_, /\x./\y.xplus(X, y)))  because xtimes > #argfun-xtimes## and [87], by (Copy) 
  87] xtimes*(X, Y) >= rec#(Y, _|_, /\x./\y.xplus(X, y))  because xtimes > rec#, [88], [90] and [91], by (Copy) 
  88] xtimes*(X, Y) >= Y  because [89], by (Select) 
  89] Y >= Y  by (Meta) 
  90] xtimes*(X, Y) >= _|_  by (Bot) 
  91] xtimes*(X, Y) >= /\y./\z.xplus(X, z)  because [92], by (F-Abs) 
  92] xtimes*(X, Y, x) >= /\z.xplus(X, z)  because [93], by (F-Abs) 
  93] xtimes*(X, Y, x, y) >= xplus(X, y)  because xtimes > xplus, [94] and [96], by (Copy) 
  94] xtimes*(X, Y, x, y) >= X  because [95], by (Select) 
  95] X >= X  by (Meta) 
  96] xtimes*(X, Y, x, y) >= y  because [97], by (Select) 
  97] y >= y  by (Var) 

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, all) by (P_5, R_0, minimal, all), where P_5 consists of:

  rec#(s(X), Y, /\x./\y.yap(F(x), y)) =#> F(X)   
  rec#(s(X), Y, /\x./\y.yap(F(x), y)) =#> rec#(X, Y, /\z./\u.yap(F(z), u))   

Thus, the original system is terminating if (P_5, R_0, minimal, all) is finite.

We consider the dependency pair problem (P_5, R_0, minimal, all).

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

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]] = _|_ 
  [[~c0]] = _|_ 

We choose Lex = {} and Mul = {@_{o -> o}, rec, rec#, s, xplus, xtimes, yap}, and the following precedence: xtimes > xplus > s > yap > rec = rec# > @_{o -> o}

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

  rec#(s(X), Y, /\x./\y.yap(F(x), y)) >= @_{o -> o}(F(X), _|_) 
  rec#(s(X), Y, /\x./\y.yap(F(x), y)) > rec#(X, Y, /\x./\y.yap(F(x), y)) 
  xplus(X, _|_) >= X 
  xplus(X, s(Y)) >= s(xplus(X, Y)) 
  rec(_|_, X, /\x./\y.yap(F(x), y)) >= X 
  rec(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) 
  xtimes(X, Y) >= rec(Y, _|_, /\x./\y.xplus(X, y)) 
  yap(F, X) >= @_{o -> o}(F, X) 
  rec(X, Y, F) >= rec#(X, Y, F) 

With these choices, we have:

  1] rec#(s(X), Y, /\x./\y.yap(F(x), y)) >= @_{o -> o}(F(X), _|_)  because [2], by (Star) 
  2] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= @_{o -> o}(F(X), _|_)  because rec# > @_{o -> o}, [3] and [10], by (Copy) 
  3] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= F(X)  because [4], by (Select) 
  4] /\x.yap(F(rec#*(s(X), Y, /\y./\z.yap(F(y), z))), x) >= F(X)  because [5], by (Eta)[Kop13:2] 
  5] F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(X)  because [6], by (Meta) 
  6] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= X  because [7], by (Select) 
  7] s(X) >= X  because [8], by (Star) 
  8] s*(X) >= X  because [9], by (Select) 
  9] X >= X  by (Meta) 
  10] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= _|_  by (Bot) 

  11] rec#(s(X), Y, /\x./\y.yap(F(x), y)) > rec#(X, Y, /\x./\y.yap(F(x), y))  because [12], by definition 
  12] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= rec#(X, Y, /\x./\y.yap(F(x), y))  because rec# in Mul, [13], [15] and [16], by (Stat) 
  13] s(X) > X  because [14], by definition 
  14] s*(X) >= X  because [9], by (Select) 
  15] Y >= Y  by (Meta) 
  16] /\x./\z.yap(F(x), z) >= /\x./\z.yap(F(x), z)  because [17], by (Abs) 
  17] /\z.yap(F(y), z) >= /\z.yap(F(y), z)  because [18], by (Abs) 
  18] yap(F(y), x) >= yap(F(y), x)  because yap in Mul, [19] and [21], by (Fun) 
  19] F(y) >= F(y)  because [20], by (Meta) 
  20] y >= y  by (Var) 
  21] x >= x  by (Var) 

  22] xplus(X, _|_) >= X  because [23], by (Star) 
  23] xplus*(X, _|_) >= X  because [24], by (Select) 
  24] X >= X  by (Meta) 

  25] xplus(X, s(Y)) >= s(xplus(X, Y))  because [26], by (Star) 
  26] xplus*(X, s(Y)) >= s(xplus(X, Y))  because xplus > s and [27], by (Copy) 
  27] xplus*(X, s(Y)) >= xplus(X, Y)  because xplus in Mul, [28] and [29], by (Stat) 
  28] X >= X  by (Meta) 
  29] s(Y) > Y  because [30], by definition 
  30] s*(Y) >= Y  because [31], by (Select) 
  31] Y >= Y  by (Meta) 

  32] rec(_|_, X, /\x./\y.yap(F(x), y)) >= X  because [33], by (Star) 
  33] rec*(_|_, X, /\x./\y.yap(F(x), y)) >= X  because [34], by (Select) 
  34] X >= X  by (Meta) 

  35] rec(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y)))  because [36], by (Star) 
  36] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y)))  because [37], by (Select) 
  37] yap(F(rec*(s(X), Y, /\x./\y.yap(F(x), y))), rec*(s(X), Y, /\z./\u.yap(F(z), u))) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y)))  because yap in Mul, [38] and [40], by (Fun) 
  38] F(rec*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(X)  because [39], by (Meta) 
  39] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= X  because [7], by (Select) 
  40] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= rec(X, Y, /\x./\y.yap(F(x), y))  because rec in Mul, [13], [15] and [16], by (Stat) 

  41] xtimes(X, Y) >= rec(Y, _|_, /\x./\y.xplus(X, y))  because [42], by (Star) 
  42] xtimes*(X, Y) >= rec(Y, _|_, /\x./\y.xplus(X, y))  because xtimes > rec, [43], [45] and [46], by (Copy) 
  43] xtimes*(X, Y) >= Y  because [44], by (Select) 
  44] Y >= Y  by (Meta) 
  45] xtimes*(X, Y) >= _|_  by (Bot) 
  46] xtimes*(X, Y) >= /\y./\z.xplus(X, z)  because [47], by (F-Abs) 
  47] xtimes*(X, Y, x) >= /\z.xplus(X, z)  because [48], by (F-Abs) 
  48] xtimes*(X, Y, x, y) >= xplus(X, y)  because xtimes > xplus, [49] and [51], by (Copy) 
  49] xtimes*(X, Y, x, y) >= X  because [50], by (Select) 
  50] X >= X  by (Meta) 
  51] xtimes*(X, Y, x, y) >= y  because [52], by (Select) 
  52] y >= y  by (Var) 

  53] yap(F, X) >= @_{o -> o}(F, X)  because [54], by (Star) 
  54] yap*(F, X) >= @_{o -> o}(F, X)  because yap > @_{o -> o}, [55] and [57], by (Copy) 
  55] yap*(F, X) >= F  because [56], by (Select) 
  56] F >= F  by (Meta) 
  57] yap*(F, X) >= X  because [58], by (Select) 
  58] X >= X  by (Meta) 

  59] rec(X, Y, F) >= rec#(X, Y, F)  because rec = rec#, rec in Mul, [60], [61] and [62], by (Fun) 
  60] X >= X  by (Meta) 
  61] Y >= Y  by (Meta) 
  62] F >= F  by (Meta) 

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

  rec#(s(X), Y, /\x./\y.yap(F(x), y)) =#> F(X)   

Thus, the original system is terminating if (P_6, R_0, minimal, all) is finite.

We consider the dependency pair problem (P_6, R_0, minimal, all).

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

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]] = _|_ 
  [[~c0]] = _|_ 

We choose Lex = {} and Mul = {@_{o -> o}, rec, rec#, s, xplus, xtimes, yap}, and the following precedence: yap > @_{o -> o} > xtimes > xplus > s > rec > rec#

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

  rec#(s(X), Y, /\x./\y.yap(F(x), y)) > @_{o -> o}(F(X), _|_) 
  xplus(X, _|_) >= X 
  xplus(X, s(Y)) >= s(xplus(X, Y)) 
  rec(_|_, X, /\x./\y.yap(F(x), y)) >= X 
  rec(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) 
  xtimes(X, Y) >= rec(Y, _|_, /\x./\y.xplus(X, y)) 
  yap(F, X) >= @_{o -> o}(F, X) 
  rec(X, Y, F) >= rec#(X, Y, F) 

With these choices, we have:

  1] rec#(s(X), Y, /\x./\y.yap(F(x), y)) > @_{o -> o}(F(X), _|_)  because [2], by definition 
  2] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= @_{o -> o}(F(X), _|_)  because [3], by (Select) 
  3] yap(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= @_{o -> o}(F(X), _|_)  because [4], by (Star) 
  4] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= @_{o -> o}(F(X), _|_)  because yap > @_{o -> o}, [5] and [11], by (Copy) 
  5] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= F(X)  because [6], by (Select) 
  6] F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(X)  because [7], by (Meta) 
  7] rec#*(s(X), Y, /\x./\y.yap(F(x), y)) >= X  because [8], by (Select) 
  8] s(X) >= X  because [9], by (Star) 
  9] s*(X) >= X  because [10], by (Select) 
  10] X >= X  by (Meta) 
  11] yap*(F(rec#*(s(X), Y, /\x./\y.yap(F(x), y))), rec#*(s(X), Y, /\z./\u.yap(F(z), u))) >= _|_  by (Bot) 

  12] xplus(X, _|_) >= X  because [13], by (Star) 
  13] xplus*(X, _|_) >= X  because [14], by (Select) 
  14] X >= X  by (Meta) 

  15] xplus(X, s(Y)) >= s(xplus(X, Y))  because [16], by (Star) 
  16] xplus*(X, s(Y)) >= s(xplus(X, Y))  because xplus > s and [17], by (Copy) 
  17] xplus*(X, s(Y)) >= xplus(X, Y)  because xplus in Mul, [18] and [19], by (Stat) 
  18] X >= X  by (Meta) 
  19] s(Y) > Y  because [20], by definition 
  20] s*(Y) >= Y  because [21], by (Select) 
  21] Y >= Y  by (Meta) 

  22] rec(_|_, X, /\x./\y.yap(F(x), y)) >= X  because [23], by (Star) 
  23] rec*(_|_, X, /\x./\y.yap(F(x), y)) >= X  because [24], by (Select) 
  24] X >= X  by (Meta) 

  25] rec(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y)))  because [26], by (Star) 
  26] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y)))  because [27], by (Select) 
  27] yap(F(rec*(s(X), Y, /\x./\y.yap(F(x), y))), rec*(s(X), Y, /\z./\u.yap(F(z), u))) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y)))  because yap in Mul, [28] and [30], by (Fun) 
  28] F(rec*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(X)  because [29], by (Meta) 
  29] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= X  because [8], by (Select) 
  30] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= rec(X, Y, /\x./\y.yap(F(x), y))  because rec in Mul, [31], [33] and [34], by (Stat) 
  31] s(X) > X  because [32], by definition 
  32] s*(X) >= X  because [10], by (Select) 
  33] Y >= Y  by (Meta) 
  34] /\x./\z.yap(F(x), z) >= /\x./\z.yap(F(x), z)  because [35], by (Abs) 
  35] /\z.yap(F(y), z) >= /\z.yap(F(y), z)  because [36], by (Abs) 
  36] yap(F(y), x) >= yap(F(y), x)  because yap in Mul, [37] and [39], by (Fun) 
  37] F(y) >= F(y)  because [38], by (Meta) 
  38] y >= y  by (Var) 
  39] x >= x  by (Var) 

  40] xtimes(X, Y) >= rec(Y, _|_, /\x./\y.xplus(X, y))  because [41], by (Star) 
  41] xtimes*(X, Y) >= rec(Y, _|_, /\x./\y.xplus(X, y))  because xtimes > rec, [42], [44] and [45], by (Copy) 
  42] xtimes*(X, Y) >= Y  because [43], by (Select) 
  43] Y >= Y  by (Meta) 
  44] xtimes*(X, Y) >= _|_  by (Bot) 
  45] xtimes*(X, Y) >= /\y./\z.xplus(X, z)  because [46], by (F-Abs) 
  46] xtimes*(X, Y, x) >= /\z.xplus(X, z)  because [47], by (F-Abs) 
  47] xtimes*(X, Y, x, y) >= xplus(X, y)  because xtimes > xplus, [48] and [50], by (Copy) 
  48] xtimes*(X, Y, x, y) >= X  because [49], by (Select) 
  49] X >= X  by (Meta) 
  50] xtimes*(X, Y, x, y) >= y  because [51], by (Select) 
  51] y >= y  by (Var) 

  52] yap(F, X) >= @_{o -> o}(F, X)  because [53], by (Star) 
  53] yap*(F, X) >= @_{o -> o}(F, X)  because yap > @_{o -> o}, [54] and [56], by (Copy) 
  54] yap*(F, X) >= F  because [55], by (Select) 
  55] F >= F  by (Meta) 
  56] yap*(F, X) >= X  because [57], by (Select) 
  57] X >= X  by (Meta) 

  58] rec(X, Y, F) >= rec#(X, Y, F)  because [59], by (Star) 
  59] rec*(X, Y, F) >= rec#(X, Y, F)  because rec > rec#, [60], [62] and [64], by (Copy) 
  60] rec*(X, Y, F) >= X  because [61], by (Select) 
  61] X >= X  by (Meta) 
  62] rec*(X, Y, F) >= Y  because [63], by (Select) 
  63] Y >= Y  by (Meta) 
  64] rec*(X, Y, F) >= F  because [65], by (Select) 
  65] F >= F  by (Meta) 

By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_6, 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:2]  C. Kop.  StarHorpo with an Eta-Rule.  Unpublished manuscript, http://cl-informatik.uibk.ac.at/users/kop/etahorpo.pdf, 2013.