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

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

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}(_|_, X), Y) > s(Y) 
  plus(X, Y) >= rec(X, Y, _|_) 
  @_{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}(_|_, X), Y) > s(Y)  because [23], by definition 
  23] @_{o -> o}*(@_{o -> o -> o}(_|_, X), Y) >= s(Y)  because [24], by (Select) 
  24] @_{o -> o -> o}(_|_, X) @_{o -> o}*(@_{o -> o -> o}(_|_, X), Y) >= s(Y)  because [25] 
  25] @_{o -> o -> o}*(_|_, X, @_{o -> o}*(@_{o -> o -> o}(_|_, X), Y)) >= s(Y)  because @_{o -> o -> o} > s and [26], by (Copy) 
  26] @_{o -> o -> o}*(_|_, X, @_{o -> o}*(@_{o -> o -> o}(_|_, X), Y)) >= Y  because [27], by (Select) 
  27] @_{o -> o}*(@_{o -> o -> o}(_|_, X), Y) >= Y  because [28], by (Select) 
  28] Y >= Y  by (Meta) 

  29] plus(X, Y) >= rec(X, Y, _|_)  because [30], by (Star) 
  30] plus*(X, Y) >= rec(X, Y, _|_)  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) >= _|_  by (Bot) 

  36] @_{o -> o}(@_{o -> o -> o}(plus3(X), Y), Z) >= plus(X, plus(Y, Z))  because [37], by (Star) 
  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 [45], by (Select) 
  45] @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= plus(Y, Z)  because @_{o -> o -> o} > plus, [46] and [48], by (Copy) 
  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] @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= Z  because [49], by (Select) 
  49] @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= Z  because [50], by (Select) 
  50] Z >= Z  by (Meta) 

  51] mult(X, Y) >= rec(X, _|_, plus3(Y))  because [52], by (Star) 
  52] mult*(X, Y) >= rec(X, _|_, plus3(Y))  because mult > rec, [53], [55] and [56], by (Copy) 
  53] mult*(X, Y) >= X  because [54], by (Select) 
  54] X >= X  by (Meta) 
  55] mult*(X, Y) >= _|_  by (Bot) 
  56] mult*(X, Y) >= plus3(Y)  because mult > plus3 and [57], by (Copy) 
  57] mult*(X, Y) >= Y  because [58], by (Select) 
  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 
  succ2 X Y => s(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))) 
  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]] = _|_ 
  [[succ2]] = _|_ 

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

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))) 
  plus(X, Y) >= rec(X, Y, _|_) 
  @_{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(s(X), Y, /\x./\y.yap(F(x), y)) > yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y)))  because [2], by definition 
  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] plus(X, Y) >= rec(X, Y, _|_)  because [20], by (Star) 
  20] plus*(X, Y) >= rec(X, Y, _|_)  because plus > rec, [21], [23] and [25], by (Copy) 
  21] plus*(X, Y) >= X  because [22], by (Select) 
  22] X >= X  by (Meta) 
  23] plus*(X, Y) >= Y  because [24], by (Select) 
  24] Y >= Y  by (Meta) 
  25] plus*(X, Y) >= _|_  by (Bot) 

  26] @_{o -> o}(@_{o -> o -> o}(plus3(X), Y), Z) >= plus(X, plus(Y, Z))  because [27], by (Star) 
  27] @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= plus(X, plus(Y, Z))  because @_{o -> o} > plus, [28] and [37], by (Copy) 
  28] @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= X  because [29], by (Select) 
  29] @_{o -> o -> o}(plus3(X), Y) @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= X  because [30] 
  30] @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= X  because [31], by (Select) 
  31] @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= X  because [32], by (Select) 
  32] @_{o -> o -> o}(plus3(X), Y) @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= X  because [33] 
  33] @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= X  because [34], by (Select) 
  34] 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 [35] 
  35] 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 [36], by (Select) 
  36] X >= X  by (Meta) 
  37] @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= plus(Y, Z)  because @_{o -> o} > plus, [38] and [45], by (Copy) 
  38] @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= Y  because [39], by (Select) 
  39] @_{o -> o -> o}(plus3(X), Y) @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= Y  because [40] 
  40] @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= Y  because [41], by (Select) 
  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)) >= Y  because [42] 
  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))) >= Y  because [43], by (Select) 
  43] @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= Y  because [44], by (Select) 
  44] Y >= Y  by (Meta) 
  45] @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= Z  because [46], by (Select) 
  46] @_{o -> o -> o}(plus3(X), Y) @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= Z  because [47] 
  47] @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= Z  because [48], by (Select) 
  48] @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= Z  because [49], by (Select) 
  49] Z >= Z  by (Meta) 

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

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

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

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

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

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

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

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

  plus(X, Y) >= rec(X, Y, _|_) 
  @_{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] plus(X, Y) >= rec(X, Y, _|_)  because [2], by (Star) 
  2] plus*(X, Y) >= rec(X, Y, _|_)  because plus > rec, [3], [5] and [7], by (Copy) 
  3] plus*(X, Y) >= X  because [4], by (Select) 
  4] X >= X  by (Meta) 
  5] plus*(X, Y) >= Y  because [6], by (Select) 
  6] Y >= Y  by (Meta) 
  7] plus*(X, Y) >= _|_  by (Bot) 

  8] @_{o -> o}(@_{o -> o -> o}(plus3(X), Y), Z) > plus(X, plus(Y, Z))  because [9], by definition 
  9] @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= plus(X, plus(Y, Z))  because @_{o -> o} > plus, [10] and [16], by (Copy) 
  10] @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= X  because [11], by (Select) 
  11] @_{o -> o -> o}(plus3(X), Y) @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= X  because [12] 
  12] @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= X  because [13], by (Select) 
  13] 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 [14] 
  14] 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 [15], by (Select) 
  15] X >= X  by (Meta) 
  16] @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= plus(Y, Z)  because @_{o -> o} > plus, [17] and [21], by (Copy) 
  17] @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= Y  because [18], by (Select) 
  18] @_{o -> o -> o}(plus3(X), Y) @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= Y  because [19] 
  19] @_{o -> o -> o}*(plus3(X), Y, @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z)) >= Y  because [20], by (Select) 
  20] Y >= Y  by (Meta) 
  21] @_{o -> o}*(@_{o -> o -> o}(plus3(X), Y), Z) >= Z  because [22], by (Select) 
  22] Z >= Z  by (Meta) 

  23] mult(X, Y) >= rec(X, _|_, plus3(Y))  because [24], by (Star) 
  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) 

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

We can thus remove the following rules:

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

  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}, mult, plus, plus3, rec, yap}, and the following precedence: mult > plus > rec > yap > @_{o -> o} > plus3

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

  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] plus(X, Y) >= rec(X, Y, _|_)  because [2], by (Star) 
  2] plus*(X, Y) >= rec(X, Y, _|_)  because plus > rec, [3], [5] and [7], by (Copy) 
  3] plus*(X, Y) >= X  because [4], by (Select) 
  4] X >= X  by (Meta) 
  5] plus*(X, Y) >= Y  because [6], by (Select) 
  6] Y >= Y  by (Meta) 
  7] plus*(X, Y) >= _|_  by (Bot) 

  8] mult(X, Y) > rec(X, _|_, plus3(Y))  because [9], by definition 
  9] mult*(X, Y) >= rec(X, _|_, plus3(Y))  because mult > rec, [10], [12] and [13], by (Copy) 
  10] mult*(X, Y) >= X  because [11], by (Select) 
  11] X >= X  by (Meta) 
  12] mult*(X, Y) >= _|_  by (Bot) 
  13] mult*(X, Y) >= plus3(Y)  because mult > plus3 and [14], by (Copy) 
  14] mult*(X, Y) >= Y  because [15], by (Select) 
  15] Y >= Y  by (Meta) 

  16] yap(F, X) >= @_{o -> o}(F, X)  because [17], by (Star) 
  17] yap*(F, X) >= @_{o -> o}(F, X)  because yap > @_{o -> o}, [18] and [20], by (Copy) 
  18] yap*(F, X) >= F  because [19], by (Select) 
  19] F >= F  by (Meta) 
  20] yap*(F, X) >= X  because [21], by (Select) 
  21] X >= X  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]):

  plus(X, Y) >? rec(X, Y, succ2) 
  yap(F, X) >? F X 

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

Argument functions:

  [[succ2]] = _|_ 

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

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

  plus(X, Y) > rec(X, Y, _|_) 
  yap(F, X) >= @_{o -> o}(F, X) 

With these choices, we have:

  1] plus(X, Y) > rec(X, Y, _|_)  because [2], by definition 
  2] plus*(X, Y) >= rec(X, Y, _|_)  because plus > rec, [3], [5] and [7], by (Copy) 
  3] plus*(X, Y) >= X  because [4], by (Select) 
  4] X >= X  by (Meta) 
  5] plus*(X, Y) >= Y  because [6], by (Select) 
  6] Y >= Y  by (Meta) 
  7] plus*(X, Y) >= _|_  by (Bot) 

  8] yap(F, X) >= @_{o -> o}(F, X)  because yap = @_{o -> o}, yap in Mul, [9] and [10], by (Fun) 
  9] F >= F  by (Meta) 
  10] 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]):

  yap(F, X) >? F X 

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

We choose Lex = {} and Mul = {@_{o -> o}, yap}, and the following precedence: yap > @_{o -> o}

With these choices, we have:

  1] yap(F, X) > @_{o -> o}(F, X)  because [2], by definition 
  2] yap*(F, X) >= @_{o -> o}(F, X)  because yap > @_{o -> o}, [3] and [5], by (Copy) 
  3] yap*(F, X) >= F  because [4], by (Select) 
  4] F >= F  by (Meta) 
  5] yap*(F, X) >= X  because [6], by (Select) 
  6] X >= X  by (Meta) 

We can thus remove the following rules:

  yap(F, X) => F X 

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.