We consider the system h49.

  Alphabet:

    0 : [] --> nat 
    mult : [nat * nat] --> nat 
    plus : [nat * nat] --> nat 
    plus3 : [nat] --> nat -> nat -> nat 
    rec : [nat * nat * nat -> nat -> nat] --> nat 
    s : [nat] --> nat 
    succ2 : [] --> nat -> nat -> nat 
    xap : [nat -> nat -> nat * nat] --> nat -> nat 
    yap : [nat -> nat * nat] --> nat 

  Rules:

    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))) 
    succ2 x y => s(y) 
    plus(x, y) => rec(x, y, succ2) 
    plus3(x) y z => plus(x, plus(y, z)) 
    mult(x, y) => rec(x, 0, plus3(y)) 
    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 
    mult : [nat * nat] --> nat 
    plus : [nat * nat] --> nat 
    plus3 : [nat] --> nat -> nat -> nat 
    rec : [nat * nat * nat -> nat -> nat] --> nat 
    s : [nat] --> nat 
    succ2 : [] --> nat -> nat -> nat 
    yap : [nat -> nat * nat] --> nat 

  Rules:

    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))) 
    succ2 X Y => s(Y) 
    plus(X, Y) => rec(X, Y, succ2) 
    plus3(X) Y Z => plus(X, plus(Y, Z)) 
    mult(X, Y) => rec(X, 0, plus3(Y)) 
    yap(F, X) => F X 

We use rule removal, following [Kop12, Theorem 2.23].

This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]):

  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))) 
  succ2 X Y >? s(Y) 
  plus(X, Y) >? rec(X, Y, succ2) 
  plus3(X) Y Z >? plus(X, plus(Y, Z)) 
  mult(X, Y) >? rec(X, 0, plus3(Y)) 
  yap(F, X) >? F X 

We use a recursive path ordering as defined in [Kop12, Chapter 5].

Argument functions:

  [[0]] = _|_ 

We choose Lex = {} and Mul = {@_{o -> o -> o}, @_{o -> o}, mult, plus, plus3, rec, s, succ2, yap}, and the following precedence: @_{o -> o -> o} > yap > s > mult = plus3 > plus > @_{o -> o} > succ2 > rec

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

  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))) 
  @_{o -> o}(@_{o -> o -> o}(succ2, X), Y) >= s(Y) 
  plus(X, Y) >= rec(X, Y, succ2) 
  @_{o -> o}(@_{o -> o -> o}(plus3(X), Y), Z) > plus(X, plus(Y, Z)) 
  mult(X, Y) >= rec(X, _|_, plus3(Y)) 
  yap(F, X) >= @_{o -> o}(F, X) 

With these choices, we have:

  1] rec(_|_, X, /\x./\y.yap(F(x), y)) > X  because [2], by definition 
  2] rec*(_|_, X, /\x./\y.yap(F(x), y)) >= X  because [3], by (Select) 
  3] X >= X  by (Meta) 

  4] rec(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y)))  because [5], by (Star) 
  5] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y)))  because [6], by (Select) 
  6] 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, [7] and [12], by (Fun) 
  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] 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 [11], 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] @_{o -> o}(@_{o -> o -> o}(succ2, X), Y) >= s(Y)  because [23], by (Star) 
  23] @_{o -> o}*(@_{o -> o -> o}(succ2, X), Y) >= s(Y)  because [24], by (Select) 
  24] @_{o -> o -> o}(succ2, X) @_{o -> o}*(@_{o -> o -> o}(succ2, X), Y) >= s(Y)  because [25] 
  25] @_{o -> o -> o}*(succ2, X, @_{o -> o}*(@_{o -> o -> o}(succ2, X), Y)) >= s(Y)  because @_{o -> o -> o} > s and [26], by (Copy) 
  26] @_{o -> o -> o}*(succ2, X, @_{o -> o}*(@_{o -> o -> o}(succ2, X), Y)) >= Y  because [27], by (Select) 
  27] @_{o -> o}*(@_{o -> o -> o}(succ2, X), Y) >= Y  because [28], by (Select) 
  28] Y >= Y  by (Meta) 

  29] plus(X, Y) >= rec(X, Y, succ2)  because [30], by (Star) 
  30] plus*(X, Y) >= rec(X, Y, succ2)  because plus > rec, [31], [33] and [35], by (Copy) 
  31] plus*(X, Y) >= X  because [32], by (Select) 
  32] X >= X  by (Meta) 
  33] plus*(X, Y) >= Y  because [34], by (Select) 
  34] Y >= Y  by (Meta) 
  35] plus*(X, Y) >= succ2  because plus > succ2, by (Copy) 

  36] @_{o -> o}(@_{o -> o -> o}(plus3(X), Y), Z) > plus(X, plus(Y, Z))  because [37], by definition 
  37] @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= plus(X, plus(Y, Z))  because [38], by (Select) 
  38] @_{o -> o -> o}(plus3(X), Y) @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= plus(X, plus(Y, Z))  because [39] 
  39] @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= plus(X, plus(Y, Z))  because [40], by (Select) 
  40] plus3(X) @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= plus(X, plus(Y, Z))  because [41] 
  41] plus3*(X, @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)), @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z))) >= plus(X, plus(Y, Z))  because plus3 > plus, [42] and [44], by (Copy) 
  42] plus3*(X, @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)), @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z))) >= X  because [43], by (Select) 
  43] X >= X  by (Meta) 
  44] plus3*(X, @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)), @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z))) >= plus(Y, Z)  because plus3 > plus, [45] and [48], by (Copy) 
  45] plus3*(X, @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)), @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z))) >= Y  because [46], by (Select) 
  46] @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= Y  because [47], by (Select) 
  47] Y >= Y  by (Meta) 
  48] plus3*(X, @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)), @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z))) >= Z  because [49], by (Select) 
  49] @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= Z  because [50], by (Select) 
  50] @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= Z  because [51], by (Select) 
  51] Z >= Z  by (Meta) 

  52] mult(X, Y) >= rec(X, _|_, plus3(Y))  because [53], by (Star) 
  53] mult*(X, Y) >= rec(X, _|_, plus3(Y))  because mult > rec, [54], [56] and [57], by (Copy) 
  54] mult*(X, Y) >= X  because [55], by (Select) 
  55] X >= X  by (Meta) 
  56] mult*(X, Y) >= _|_  by (Bot) 
  57] mult*(X, Y) >= plus3(Y)  because mult = plus3, mult in Mul and [58], by (Stat) 
  58] Y >= Y  by (Meta) 

  59] yap(F, X) >= @_{o -> o}(F, X)  because [60], by (Star) 
  60] yap*(F, X) >= @_{o -> o}(F, X)  because yap > @_{o -> o}, [61] and [63], by (Copy) 
  61] yap*(F, X) >= F  because [62], by (Select) 
  62] F >= F  by (Meta) 
  63] yap*(F, X) >= X  because [64], by (Select) 
  64] X >= X  by (Meta) 

We can thus remove the following rules:

  rec(0, X, /\x./\y.yap(F(x), y)) => X 
  plus3(X) Y Z => plus(X, plus(Y, Z)) 

We use rule removal, following [Kop12, Theorem 2.23].

This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]):

  rec(s(X), Y, /\x./\y.yap(F(x), y)) >? yap(F(X), rec(X, Y, /\z./\u.yap(F(z), u))) 
  succ2 X Y >? s(Y) 
  plus(X, Y) >? rec(X, Y, succ2) 
  mult(X, Y) >? rec(X, 0, plus3(Y)) 
  yap(F, X) >? F X 

We use a recursive path ordering as defined in [Kop12, Chapter 5].

Argument functions:

  [[0]] = _|_ 
  [[succ2]] = _|_ 

We choose Lex = {} and Mul = {@_{o -> o -> o}, @_{o -> o}, mult, plus, plus3, rec, s, yap}, and the following precedence: mult > plus > rec > yap > plus3 > @_{o -> o} = s > @_{o -> 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)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) 
  @_{o -> o}(@_{o -> o -> o}(_|_, X), Y) >= s(Y) 
  plus(X, Y) > rec(X, Y, _|_) 
  mult(X, Y) >= rec(X, _|_, plus3(Y)) 
  yap(F, X) >= @_{o -> o}(F, X) 

With these choices, we have:

  1] rec(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(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)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y)))  because rec > yap, [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)) >= rec(X, Y, /\x./\y.yap(F(x), y))  because rec in Mul, [11], [13] and [14], by (Stat) 
  11] s(X) > X  because [12], by definition 
  12] s*(X) >= X  because [9], by (Select) 
  13] Y >= Y  by (Meta) 
  14] /\x./\z.yap(F(x), z) >= /\x./\z.yap(F(x), z)  because [15], by (Abs) 
  15] /\z.yap(F(y), z) >= /\z.yap(F(y), z)  because [16], by (Abs) 
  16] yap(F(y), x) >= yap(F(y), x)  because yap in Mul, [17] and [19], by (Fun) 
  17] F(y) >= F(y)  because [18], by (Meta) 
  18] y >= y  by (Var) 
  19] x >= x  by (Var) 

  20] @_{o -> o}(@_{o -> o -> o}(_|_, X), Y) >= s(Y)  because [21], by (Star) 
  21] @_{o -> o}*(@_{o -> o -> o}(_|_, X), Y) >= s(Y)  because @_{o -> o} = s, @_{o -> o} in Mul and [22], by (Stat) 
  22] Y >= Y  by (Meta) 

  23] plus(X, Y) > rec(X, Y, _|_)  because [24], by definition 
  24] plus*(X, Y) >= rec(X, Y, _|_)  because plus > rec, [25], [27] and [29], by (Copy) 
  25] plus*(X, Y) >= X  because [26], by (Select) 
  26] X >= X  by (Meta) 
  27] plus*(X, Y) >= Y  because [28], by (Select) 
  28] Y >= Y  by (Meta) 
  29] plus*(X, Y) >= _|_  by (Bot) 

  30] mult(X, Y) >= rec(X, _|_, plus3(Y))  because [31], by (Star) 
  31] mult*(X, Y) >= rec(X, _|_, plus3(Y))  because mult > rec, [32], [34] and [35], by (Copy) 
  32] mult*(X, Y) >= X  because [33], by (Select) 
  33] X >= X  by (Meta) 
  34] mult*(X, Y) >= _|_  by (Bot) 
  35] mult*(X, Y) >= plus3(Y)  because mult > plus3 and [36], by (Copy) 
  36] mult*(X, Y) >= Y  because [37], by (Select) 
  37] Y >= Y  by (Meta) 

  38] yap(F, X) >= @_{o -> o}(F, X)  because [39], by (Star) 
  39] yap*(F, X) >= @_{o -> o}(F, X)  because yap > @_{o -> o}, [40] and [42], by (Copy) 
  40] yap*(F, X) >= F  because [41], by (Select) 
  41] F >= F  by (Meta) 
  42] yap*(F, X) >= X  because [43], by (Select) 
  43] X >= X  by (Meta) 

We can thus remove the following rules:

  plus(X, Y) => rec(X, Y, succ2) 

We use rule removal, following [Kop12, Theorem 2.23].

This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]):

  rec(s(X), Y, /\x./\y.yap(F(x), y)) >? yap(F(X), rec(X, Y, /\z./\u.yap(F(z), u))) 
  succ2(X, Y) >? s(Y) 
  mult(X, Y) >? rec(X, 0, plus3(Y)) 
  yap(F, X) >? F X 

We use a recursive path ordering as defined in [Kop12, Chapter 5].

Argument functions:

  [[0]] = _|_ 

We choose Lex = {} and Mul = {@_{o -> o}, mult, plus3, rec, s, succ2, yap}, and the following precedence: mult > rec > succ2 > plus3 > s > 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)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) 
  succ2(X, Y) >= s(Y) 
  mult(X, Y) >= rec(X, _|_, plus3(Y)) 
  yap(F, X) > @_{o -> o}(F, X) 

With these choices, we have:

  1] rec(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(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)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y)))  because rec > yap, [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)) >= rec(X, Y, /\x./\y.yap(F(x), y))  because rec in Mul, [11], [13] and [14], by (Stat) 
  11] s(X) > X  because [12], by definition 
  12] s*(X) >= X  because [9], by (Select) 
  13] Y >= Y  by (Meta) 
  14] /\x./\z.yap(F(x), z) >= /\x./\z.yap(F(x), z)  because [15], by (Abs) 
  15] /\z.yap(F(y), z) >= /\z.yap(F(y), z)  because [16], by (Abs) 
  16] yap(F(y), x) >= yap(F(y), x)  because yap in Mul, [17] and [19], by (Fun) 
  17] F(y) >= F(y)  because [18], by (Meta) 
  18] y >= y  by (Var) 
  19] x >= x  by (Var) 

  20] succ2(X, Y) >= s(Y)  because [21], by (Star) 
  21] succ2*(X, Y) >= s(Y)  because succ2 > s and [22], by (Copy) 
  22] succ2*(X, Y) >= Y  because [23], by (Select) 
  23] Y >= Y  by (Meta) 

  24] mult(X, Y) >= rec(X, _|_, plus3(Y))  because [25], by (Star) 
  25] mult*(X, Y) >= rec(X, _|_, plus3(Y))  because mult > rec, [26], [28] and [29], by (Copy) 
  26] mult*(X, Y) >= X  because [27], by (Select) 
  27] X >= X  by (Meta) 
  28] mult*(X, Y) >= _|_  by (Bot) 
  29] mult*(X, Y) >= plus3(Y)  because mult > plus3 and [30], by (Copy) 
  30] mult*(X, Y) >= Y  because [31], by (Select) 
  31] Y >= Y  by (Meta) 

  32] yap(F, X) > @_{o -> o}(F, X)  because [33], by definition 
  33] yap*(F, X) >= @_{o -> o}(F, X)  because yap > @_{o -> o}, [34] and [36], by (Copy) 
  34] yap*(F, X) >= F  because [35], by (Select) 
  35] F >= F  by (Meta) 
  36] yap*(F, X) >= X  because [37], by (Select) 
  37] X >= X  by (Meta) 

We can thus remove the following rules:

  yap(F, X) => F X 

We use rule removal, following [Kop12, Theorem 2.23].

This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]):

  rec(s(X), Y, /\x./\y.yap(F(x), y)) >? yap(F(X), rec(X, Y, /\z./\u.yap(F(z), u))) 
  succ2(X, Y) >? s(Y) 
  mult(X, Y) >? rec(X, 0, plus3(Y)) 

We use a recursive path ordering as defined in [Kop12, Chapter 5].

Argument functions:

  [[0]] = _|_ 

We choose Lex = {} and Mul = {mult, plus3, rec, s, succ2, yap}, and the following precedence: succ2 > s > yap > mult > plus3 > 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)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) 
  succ2(X, Y) >= s(Y) 
  mult(X, Y) > rec(X, _|_, plus3(Y)) 

With these choices, we have:

  1] rec(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(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)) >= yap(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))) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y)))  because yap in Mul, [4] and [9], by (Fun) 
  4] F(rec*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(X)  because [5], by (Meta) 
  5] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= X  because [6], by (Select) 
  6] s(X) >= X  because [7], by (Star) 
  7] s*(X) >= X  because [8], by (Select) 
  8] X >= X  by (Meta) 
  9] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= rec(X, Y, /\x./\y.yap(F(x), y))  because rec in Mul, [10], [12] and [13], by (Stat) 
  10] s(X) > X  because [11], by definition 
  11] s*(X) >= X  because [8], by (Select) 
  12] Y >= Y  by (Meta) 
  13] /\x./\z.yap(F(x), z) >= /\x./\z.yap(F(x), z)  because [14], by (Abs) 
  14] /\z.yap(F(y), z) >= /\z.yap(F(y), z)  because [15], by (Abs) 
  15] yap(F(y), x) >= yap(F(y), x)  because yap in Mul, [16] and [18], by (Fun) 
  16] F(y) >= F(y)  because [17], by (Meta) 
  17] y >= y  by (Var) 
  18] x >= x  by (Var) 

  19] succ2(X, Y) >= s(Y)  because [20], by (Star) 
  20] succ2*(X, Y) >= s(Y)  because succ2 > s and [21], by (Copy) 
  21] succ2*(X, Y) >= Y  because [22], by (Select) 
  22] Y >= Y  by (Meta) 

  23] mult(X, Y) > rec(X, _|_, plus3(Y))  because [24], by definition 
  24] mult*(X, Y) >= rec(X, _|_, plus3(Y))  because mult > rec, [25], [27] and [28], by (Copy) 
  25] mult*(X, Y) >= X  because [26], by (Select) 
  26] X >= X  by (Meta) 
  27] mult*(X, Y) >= _|_  by (Bot) 
  28] mult*(X, Y) >= plus3(Y)  because mult > plus3 and [29], by (Copy) 
  29] mult*(X, Y) >= Y  because [30], by (Select) 
  30] Y >= Y  by (Meta) 

We can thus remove the following rules:

  mult(X, Y) => rec(X, 0, plus3(Y)) 

We use rule removal, following [Kop12, Theorem 2.23].

This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]):

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

We orient these requirements with a polynomial interpretation in the natural numbers.

The following interpretation satisfies the requirements:

  rec = \y0y1G2.y0 + 2y1 + G2(y1,y1) + 2y0y0G2(y0,y0) + 2y0y1G2(y0,y1) + 2G2(y0,y0) 
  s = \y0.1 + 3y0 
  succ2 = \y0y1.3 + y0 + 3y1 
  yap = \G0y1.y1 + G0(0) 

Using this interpretation, the requirements translate to:

  [[rec(s(_x0), _x1, /\x./\y.yap(_F2(x), y))]] = 5 + 2x1x1 + 3x1 + 6x0x1x1 + 27x0 + 54x0x0 + 54x0x0x0 + F2(x1,0) + 2x1F2(1 + 3x0,0) + 4F2(1 + 3x0,0) + 6x0x1F2(1 + 3x0,0) + 12x0F2(1 + 3x0,0) + 18x0x0F2(1 + 3x0,0) > 2x0x0x0 + 2x0x1x1 + 3x0 + 3x1 + F2(x1,0) + 2x0x0F2(x0,0) + 2x0x1F2(x0,0) + 3F2(x0,0) = [[yap(_F2(_x0), rec(_x0, _x1, /\x./\y.yap(_F2(x), y)))]] 
  [[succ2(_x0, _x1)]] = 3 + x0 + 3x1 > 1 + 3x1 = [[s(_x1)]] 

We can thus remove the following rules:

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

All rules were succesfully removed.  Thus, termination of the original system has been reduced to termination of the beta-rule, which is well-known to hold.


+++ 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.