We consider the system 477.

  Alphabet:

    2 : [] --> int 
    altmap : [int -> int * list] --> list 
    cons : [int * list] --> list 
    mlt : [int * int] --> int 
    nil : [] --> list 
    pls : [int * int] --> int 
    plus : [int * int] --> int 
    star : [int * int] --> int 

  Rules:

    altmap(/\x.pls(x, X), cons(Y, Z)) => cons(pls(Y, X), altmap(/\y.mlt(y, X), Z)) 
    altmap(/\x.mlt(x, X), cons(Y, Z)) => cons(mlt(Y, X), altmap(/\y.pls(y, X), Z)) 
    altmap(/\x.X(x), nil) => nil 
    pls(X, Y) => plus(X, Y) 
    mlt(X, Y) => star(X, Y) 
    pls(2, 2) => mlt(2, 2) 

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

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

  altmap(/\x.pls(x, X), cons(Y, Z)) >? cons(pls(Y, X), altmap(/\y.mlt(y, X), Z)) 
  altmap(/\x.mlt(x, X), cons(Y, Z)) >? cons(mlt(Y, X), altmap(/\y.pls(y, X), Z)) 
  altmap(/\x.X(x), nil) >? nil 
  pls(X, Y) >? plus(X, Y) 
  mlt(X, Y) >? star(X, Y) 
  pls(2, 2) >? mlt(2, 2) 

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

Argument functions:

  [[nil]] = _|_ 

We choose Lex = {} and Mul = {2, altmap, cons, mlt, pls, plus, star}, and the following precedence: 2 > altmap > cons > mlt = pls = plus > star

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

  altmap(/\x.pls(x, X), cons(Y, Z)) >= cons(pls(Y, X), altmap(/\x.mlt(x, X), Z)) 
  altmap(/\x.mlt(x, X), cons(Y, Z)) >= cons(mlt(Y, X), altmap(/\x.pls(x, X), Z)) 
  altmap(/\x.X(x), _|_) > _|_ 
  pls(X, Y) >= plus(X, Y) 
  mlt(X, Y) >= star(X, Y) 
  pls(2, 2) >= mlt(2, 2) 

With these choices, we have:

  1] altmap(/\x.pls(x, X), cons(Y, Z)) >= cons(pls(Y, X), altmap(/\x.mlt(x, X), Z))  because [2], by (Star) 
  2] altmap*(/\x.pls(x, X), cons(Y, Z)) >= cons(pls(Y, X), altmap(/\x.mlt(x, X), Z))  because [3], by (Select) 
  3] pls(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= cons(pls(Y, X), altmap(/\x.mlt(x, X), Z))  because [4], by (Star) 
  4] pls*(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= cons(pls(Y, X), altmap(/\x.mlt(x, X), Z))  because [5], by (Select) 
  5] altmap*(/\x.pls(x, X), cons(Y, Z)) >= cons(pls(Y, X), altmap(/\x.mlt(x, X), Z))  because altmap > cons, [6] and [24], by (Copy) 
  6] altmap*(/\x.pls(x, X), cons(Y, Z)) >= pls(Y, X)  because altmap > pls, [7] and [17], by (Copy) 
  7] altmap*(/\x.pls(x, X), cons(Y, Z)) >= Y  because [8], by (Select) 
  8] pls(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= Y  because [9], by (Star) 
  9] pls*(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= Y  because [10], by (Select) 
  10] altmap*(/\x.pls(x, X), cons(Y, Z)) >= Y  because [11], by (Select) 
  11] pls(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= Y  because [12], by (Star) 
  12] pls*(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= Y  because [13], by (Select) 
  13] altmap*(/\x.pls(x, X), cons(Y, Z)) >= Y  because [14], by (Select) 
  14] cons(Y, Z) >= Y  because [15], by (Star) 
  15] cons*(Y, Z) >= Y  because [16], by (Select) 
  16] Y >= Y  by (Meta) 
  17] altmap*(/\x.pls(x, X), cons(Y, Z)) >= X  because [18], by (Select) 
  18] pls(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= X  because [19], by (Star) 
  19] pls*(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= X  because [20], by (Select) 
  20] altmap*(/\x.pls(x, X), cons(Y, Z)) >= X  because [21], by (Select) 
  21] pls(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= X  because [22], by (Star) 
  22] pls*(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= X  because [23], by (Select) 
  23] X >= X  by (Meta) 
  24] altmap*(/\x.pls(x, X), cons(Y, Z)) >= altmap(/\x.mlt(x, X), Z)  because altmap in Mul, [25] and [29], by (Stat) 
  25] /\y.pls(y, X) >= /\y.mlt(y, X)  because [26], by (Abs) 
  26] pls(x, X) >= mlt(x, X)  because pls = mlt, pls in Mul, [27] and [28], by (Fun) 
  27] x >= x  by (Var) 
  28] X >= X  by (Meta) 
  29] cons(Y, Z) > Z  because [30], by definition 
  30] cons*(Y, Z) >= Z  because [31], by (Select) 
  31] Z >= Z  by (Meta) 

  32] altmap(/\x.mlt(x, X), cons(Y, Z)) >= cons(mlt(Y, X), altmap(/\x.pls(x, X), Z))  because [33], by (Star) 
  33] altmap*(/\x.mlt(x, X), cons(Y, Z)) >= cons(mlt(Y, X), altmap(/\x.pls(x, X), Z))  because altmap > cons, [34] and [43], by (Copy) 
  34] altmap*(/\x.mlt(x, X), cons(Y, Z)) >= mlt(Y, X)  because altmap > mlt, [35] and [39], by (Copy) 
  35] altmap*(/\x.mlt(x, X), cons(Y, Z)) >= Y  because [36], by (Select) 
  36] cons(Y, Z) >= Y  because [37], by (Star) 
  37] cons*(Y, Z) >= Y  because [38], by (Select) 
  38] Y >= Y  by (Meta) 
  39] altmap*(/\x.mlt(x, X), cons(Y, Z)) >= X  because [40], by (Select) 
  40] mlt(altmap*(/\x.mlt(x, X), cons(Y, Z)), X) >= X  because [41], by (Star) 
  41] mlt*(altmap*(/\x.mlt(x, X), cons(Y, Z)), X) >= X  because [42], by (Select) 
  42] X >= X  by (Meta) 
  43] altmap*(/\x.mlt(x, X), cons(Y, Z)) >= altmap(/\x.pls(x, X), Z)  because altmap in Mul, [44] and [48], by (Stat) 
  44] /\y.mlt(y, X) >= /\y.pls(y, X)  because [45], by (Abs) 
  45] mlt(x, X) >= pls(x, X)  because mlt = pls, mlt in Mul, [46] and [47], by (Fun) 
  46] x >= x  by (Var) 
  47] X >= X  by (Meta) 
  48] cons(Y, Z) > Z  because [49], by definition 
  49] cons*(Y, Z) >= Z  because [50], by (Select) 
  50] Z >= Z  by (Meta) 

  51] altmap(/\x.X(x), _|_) > _|_  because [52], by definition 
  52] altmap*(/\x.X(x), _|_) >= _|_  by (Bot) 

  53] pls(X, Y) >= plus(X, Y)  because pls = plus, pls in Mul, [54] and [55], by (Fun) 
  54] X >= X  by (Meta) 
  55] Y >= Y  by (Meta) 

  56] mlt(X, Y) >= star(X, Y)  because [57], by (Star) 
  57] mlt*(X, Y) >= star(X, Y)  because mlt > star, [58] and [60], by (Copy) 
  58] mlt*(X, Y) >= X  because [59], by (Select) 
  59] X >= X  by (Meta) 
  60] mlt*(X, Y) >= Y  because [61], by (Select) 
  61] Y >= Y  by (Meta) 

  62] pls(2, 2) >= mlt(2, 2)  because pls = mlt, pls in Mul, [63] and [63], by (Fun) 
  63] 2 >= 2  by (Fun) 

We can thus remove the following rules:

  altmap(/\x.X(x), nil) => nil 

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

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

  altmap(/\x.pls(x, X), cons(Y, Z)) >? cons(pls(Y, X), altmap(/\y.mlt(y, X), Z)) 
  altmap(/\x.mlt(x, X), cons(Y, Z)) >? cons(mlt(Y, X), altmap(/\y.pls(y, X), Z)) 
  pls(X, Y) >? plus(X, Y) 
  mlt(X, Y) >? star(X, Y) 
  pls(2, 2) >? mlt(2, 2) 

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

We choose Lex = {} and Mul = {2, altmap, cons, mlt, pls, plus, star}, and the following precedence: altmap > cons > mlt = pls = plus > star > 2

With these choices, we have:

  1] altmap(/\x.pls(x, X), cons(Y, Z)) >= cons(pls(Y, X), altmap(/\x.mlt(x, X), Z))  because [2], by (Star) 
  2] altmap*(/\x.pls(x, X), cons(Y, Z)) >= cons(pls(Y, X), altmap(/\x.mlt(x, X), Z))  because [3], by (Select) 
  3] pls(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= cons(pls(Y, X), altmap(/\x.mlt(x, X), Z))  because [4], by (Star) 
  4] pls*(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= cons(pls(Y, X), altmap(/\x.mlt(x, X), Z))  because [5], by (Select) 
  5] altmap*(/\x.pls(x, X), cons(Y, Z)) >= cons(pls(Y, X), altmap(/\x.mlt(x, X), Z))  because altmap > cons, [6] and [15], by (Copy) 
  6] altmap*(/\x.pls(x, X), cons(Y, Z)) >= pls(Y, X)  because altmap > pls, [7] and [11], by (Copy) 
  7] altmap*(/\x.pls(x, X), cons(Y, Z)) >= Y  because [8], by (Select) 
  8] cons(Y, Z) >= Y  because [9], by (Star) 
  9] cons*(Y, Z) >= Y  because [10], by (Select) 
  10] Y >= Y  by (Meta) 
  11] altmap*(/\x.pls(x, X), cons(Y, Z)) >= X  because [12], by (Select) 
  12] pls(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= X  because [13], by (Star) 
  13] pls*(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= X  because [14], by (Select) 
  14] X >= X  by (Meta) 
  15] altmap*(/\x.pls(x, X), cons(Y, Z)) >= altmap(/\x.mlt(x, X), Z)  because [16], by (Select) 
  16] pls(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= altmap(/\x.mlt(x, X), Z)  because [17], by (Star) 
  17] pls*(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= altmap(/\x.mlt(x, X), Z)  because [18], by (Select) 
  18] altmap*(/\x.pls(x, X), cons(Y, Z)) >= altmap(/\x.mlt(x, X), Z)  because altmap in Mul, [19] and [23], by (Stat) 
  19] /\y.pls(y, X) >= /\y.mlt(y, X)  because [20], by (Abs) 
  20] pls(x, X) >= mlt(x, X)  because pls = mlt, pls in Mul, [21] and [22], by (Fun) 
  21] x >= x  by (Var) 
  22] X >= X  by (Meta) 
  23] cons(Y, Z) > Z  because [24], by definition 
  24] cons*(Y, Z) >= Z  because [25], by (Select) 
  25] Z >= Z  by (Meta) 

  26] altmap(/\x.mlt(x, X), cons(Y, Z)) >= cons(mlt(Y, X), altmap(/\x.pls(x, X), Z))  because [27], by (Star) 
  27] altmap*(/\x.mlt(x, X), cons(Y, Z)) >= cons(mlt(Y, X), altmap(/\x.pls(x, X), Z))  because altmap > cons, [28] and [38], by (Copy) 
  28] altmap*(/\x.mlt(x, X), cons(Y, Z)) >= mlt(Y, X)  because [29], by (Select) 
  29] mlt(altmap*(/\x.mlt(x, X), cons(Y, Z)), X) >= mlt(Y, X)  because mlt in Mul, [30] and [37], by (Fun) 
  30] altmap*(/\x.mlt(x, X), cons(Y, Z)) >= Y  because [31], by (Select) 
  31] mlt(altmap*(/\x.mlt(x, X), cons(Y, Z)), X) >= Y  because [32], by (Star) 
  32] mlt*(altmap*(/\x.mlt(x, X), cons(Y, Z)), X) >= Y  because [33], by (Select) 
  33] altmap*(/\x.mlt(x, X), cons(Y, Z)) >= Y  because [34], by (Select) 
  34] cons(Y, Z) >= Y  because [35], by (Star) 
  35] cons*(Y, Z) >= Y  because [36], by (Select) 
  36] Y >= Y  by (Meta) 
  37] X >= X  by (Meta) 
  38] altmap*(/\x.mlt(x, X), cons(Y, Z)) >= altmap(/\x.pls(x, X), Z)  because altmap in Mul, [39] and [42], by (Stat) 
  39] /\y.mlt(y, X) >= /\y.pls(y, X)  because [40], by (Abs) 
  40] mlt(x, X) >= pls(x, X)  because mlt = pls, mlt in Mul, [41] and [37], by (Fun) 
  41] x >= x  by (Var) 
  42] cons(Y, Z) > Z  because [43], by definition 
  43] cons*(Y, Z) >= Z  because [44], by (Select) 
  44] Z >= Z  by (Meta) 

  45] pls(X, Y) >= plus(X, Y)  because pls = plus, pls in Mul, [46] and [47], by (Fun) 
  46] X >= X  by (Meta) 
  47] Y >= Y  by (Meta) 

  48] mlt(X, Y) > star(X, Y)  because [49], by definition 
  49] mlt*(X, Y) >= star(X, Y)  because mlt > star, [50] and [52], by (Copy) 
  50] mlt*(X, Y) >= X  because [51], by (Select) 
  51] X >= X  by (Meta) 
  52] mlt*(X, Y) >= Y  because [53], by (Select) 
  53] Y >= Y  by (Meta) 

  54] pls(2, 2) >= mlt(2, 2)  because pls = mlt, pls in Mul, [55] and [55], by (Fun) 
  55] 2 >= 2  by (Fun) 

We can thus remove the following rules:

  mlt(X, Y) => star(X, 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]):

  altmap(/\x.pls(x, X), cons(Y, Z)) >? cons(pls(Y, X), altmap(/\y.mlt(y, X), Z)) 
  altmap(/\x.mlt(x, X), cons(Y, Z)) >? cons(mlt(Y, X), altmap(/\y.pls(y, X), Z)) 
  pls(X, Y) >? plus(X, Y) 
  pls(2, 2) >? mlt(2, 2) 

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

We choose Lex = {} and Mul = {2, altmap, cons, mlt, pls, plus}, and the following precedence: mlt = pls > 2 > cons > altmap > plus

With these choices, we have:

  1] altmap(/\x.pls(x, X), cons(Y, Z)) >= cons(pls(Y, X), altmap(/\x.mlt(x, X), Z))  because [2], by (Star) 
  2] altmap*(/\x.pls(x, X), cons(Y, Z)) >= cons(pls(Y, X), altmap(/\x.mlt(x, X), Z))  because [3], by (Select) 
  3] pls(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= cons(pls(Y, X), altmap(/\x.mlt(x, X), Z))  because [4], by (Star) 
  4] pls*(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= cons(pls(Y, X), altmap(/\x.mlt(x, X), Z))  because pls > cons, [5] and [13], by (Copy) 
  5] pls*(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= pls(Y, X)  because [6], by (Select) 
  6] altmap*(/\x.pls(x, X), cons(Y, Z)) >= pls(Y, X)  because [7], by (Select) 
  7] pls(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= pls(Y, X)  because pls in Mul, [8] and [12], by (Fun) 
  8] altmap*(/\x.pls(x, X), cons(Y, Z)) >= Y  because [9], by (Select) 
  9] cons(Y, Z) >= Y  because [10], by (Star) 
  10] cons*(Y, Z) >= Y  because [11], by (Select) 
  11] Y >= Y  by (Meta) 
  12] X >= X  by (Meta) 
  13] pls*(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= altmap(/\x.mlt(x, X), Z)  because [14], by (Select) 
  14] altmap*(/\x.pls(x, X), cons(Y, Z)) >= altmap(/\x.mlt(x, X), Z)  because altmap in Mul, [15] and [18], by (Stat) 
  15] /\y.pls(y, X) >= /\y.mlt(y, X)  because [16], by (Abs) 
  16] pls(x, X) >= mlt(x, X)  because pls = mlt, pls in Mul, [17] and [12], by (Fun) 
  17] x >= x  by (Var) 
  18] cons(Y, Z) > Z  because [19], by definition 
  19] cons*(Y, Z) >= Z  because [20], by (Select) 
  20] Z >= Z  by (Meta) 

  21] altmap(/\x.mlt(x, X), cons(Y, Z)) >= cons(mlt(Y, X), altmap(/\x.pls(x, X), Z))  because [22], by (Star) 
  22] altmap*(/\x.mlt(x, X), cons(Y, Z)) >= cons(mlt(Y, X), altmap(/\x.pls(x, X), Z))  because [23], by (Select) 
  23] mlt(altmap*(/\x.mlt(x, X), cons(Y, Z)), X) >= cons(mlt(Y, X), altmap(/\x.pls(x, X), Z))  because [24], by (Star) 
  24] mlt*(altmap*(/\x.mlt(x, X), cons(Y, Z)), X) >= cons(mlt(Y, X), altmap(/\x.pls(x, X), Z))  because mlt > cons, [25] and [33], by (Copy) 
  25] mlt*(altmap*(/\x.mlt(x, X), cons(Y, Z)), X) >= mlt(Y, X)  because [26], by (Select) 
  26] altmap*(/\x.mlt(x, X), cons(Y, Z)) >= mlt(Y, X)  because [27], by (Select) 
  27] mlt(altmap*(/\x.mlt(x, X), cons(Y, Z)), X) >= mlt(Y, X)  because mlt in Mul, [28] and [32], by (Fun) 
  28] altmap*(/\x.mlt(x, X), cons(Y, Z)) >= Y  because [29], by (Select) 
  29] cons(Y, Z) >= Y  because [30], by (Star) 
  30] cons*(Y, Z) >= Y  because [31], by (Select) 
  31] Y >= Y  by (Meta) 
  32] X >= X  by (Meta) 
  33] mlt*(altmap*(/\x.mlt(x, X), cons(Y, Z)), X) >= altmap(/\x.pls(x, X), Z)  because [34], by (Select) 
  34] altmap*(/\x.mlt(x, X), cons(Y, Z)) >= altmap(/\x.pls(x, X), Z)  because altmap in Mul, [35] and [38], by (Stat) 
  35] /\y.mlt(y, X) >= /\y.pls(y, X)  because [36], by (Abs) 
  36] mlt(x, X) >= pls(x, X)  because mlt = pls, mlt in Mul, [37] and [32], by (Fun) 
  37] x >= x  by (Var) 
  38] cons(Y, Z) > Z  because [39], by definition 
  39] cons*(Y, Z) >= Z  because [40], by (Select) 
  40] Z >= Z  by (Meta) 

  41] pls(X, Y) > plus(X, Y)  because [42], by definition 
  42] pls*(X, Y) >= plus(X, Y)  because pls > plus, [43] and [45], by (Copy) 
  43] pls*(X, Y) >= X  because [44], by (Select) 
  44] X >= X  by (Meta) 
  45] pls*(X, Y) >= Y  because [46], by (Select) 
  46] Y >= Y  by (Meta) 

  47] pls(2, 2) >= mlt(2, 2)  because pls = mlt, pls in Mul, [48] and [48], by (Fun) 
  48] 2 >= 2  by (Fun) 

We can thus remove the following rules:

  pls(X, Y) => plus(X, 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]):

  altmap(/\x.pls(x, X), cons(Y, Z)) >? cons(pls(Y, X), altmap(/\y.mlt(y, X), Z)) 
  altmap(/\x.mlt(x, X), cons(Y, Z)) >? cons(mlt(Y, X), altmap(/\y.pls(y, X), Z)) 
  pls(2, 2) >? mlt(2, 2) 

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

We choose Lex = {} and Mul = {2, altmap, cons, mlt, pls}, and the following precedence: mlt = pls > altmap > 2 > cons

With these choices, we have:

  1] altmap(/\x.pls(x, X), cons(Y, Z)) >= cons(pls(Y, X), altmap(/\x.mlt(x, X), Z))  because [2], by (Star) 
  2] altmap*(/\x.pls(x, X), cons(Y, Z)) >= cons(pls(Y, X), altmap(/\x.mlt(x, X), Z))  because altmap > cons, [3] and [10], by (Copy) 
  3] altmap*(/\x.pls(x, X), cons(Y, Z)) >= pls(Y, X)  because [4], by (Select) 
  4] pls(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= pls(Y, X)  because pls in Mul, [5] and [9], by (Fun) 
  5] altmap*(/\x.pls(x, X), cons(Y, Z)) >= Y  because [6], by (Select) 
  6] cons(Y, Z) >= Y  because [7], by (Star) 
  7] cons*(Y, Z) >= Y  because [8], by (Select) 
  8] Y >= Y  by (Meta) 
  9] X >= X  by (Meta) 
  10] altmap*(/\x.pls(x, X), cons(Y, Z)) >= altmap(/\x.mlt(x, X), Z)  because altmap in Mul, [11] and [14], by (Stat) 
  11] /\y.pls(y, X) >= /\y.mlt(y, X)  because [12], by (Abs) 
  12] pls(x, X) >= mlt(x, X)  because pls = mlt, pls in Mul, [13] and [9], by (Fun) 
  13] x >= x  by (Var) 
  14] cons(Y, Z) > Z  because [15], by definition 
  15] cons*(Y, Z) >= Z  because [16], by (Select) 
  16] Z >= Z  by (Meta) 

  17] altmap(/\x.mlt(x, X), cons(Y, Z)) > cons(mlt(Y, X), altmap(/\x.pls(x, X), Z))  because [18], by definition 
  18] altmap*(/\x.mlt(x, X), cons(Y, Z)) >= cons(mlt(Y, X), altmap(/\x.pls(x, X), Z))  because altmap > cons, [19] and [26], by (Copy) 
  19] altmap*(/\x.mlt(x, X), cons(Y, Z)) >= mlt(Y, X)  because [20], by (Select) 
  20] mlt(altmap*(/\x.mlt(x, X), cons(Y, Z)), X) >= mlt(Y, X)  because mlt in Mul, [21] and [25], by (Fun) 
  21] altmap*(/\x.mlt(x, X), cons(Y, Z)) >= Y  because [22], by (Select) 
  22] cons(Y, Z) >= Y  because [23], by (Star) 
  23] cons*(Y, Z) >= Y  because [24], by (Select) 
  24] Y >= Y  by (Meta) 
  25] X >= X  by (Meta) 
  26] altmap*(/\x.mlt(x, X), cons(Y, Z)) >= altmap(/\x.pls(x, X), Z)  because altmap in Mul, [27] and [30], by (Stat) 
  27] /\y.mlt(y, X) >= /\y.pls(y, X)  because [28], by (Abs) 
  28] mlt(x, X) >= pls(x, X)  because mlt = pls, mlt in Mul, [29] and [25], by (Fun) 
  29] x >= x  by (Var) 
  30] cons(Y, Z) > Z  because [31], by definition 
  31] cons*(Y, Z) >= Z  because [32], by (Select) 
  32] Z >= Z  by (Meta) 

  33] pls(2, 2) >= mlt(2, 2)  because pls = mlt, pls in Mul, [34] and [34], by (Fun) 
  34] 2 >= 2  by (Fun) 

We can thus remove the following rules:

  altmap(/\x.mlt(x, X), cons(Y, Z)) => cons(mlt(Y, X), altmap(/\y.pls(y, X), 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]):

  altmap(/\x.pls(x, X), cons(Y, Z)) >? cons(pls(Y, X), altmap(/\y.mlt(y, X), Z)) 
  pls(2, 2) >? mlt(2, 2) 

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

We choose Lex = {} and Mul = {2, altmap, cons, mlt, pls}, and the following precedence: 2 > altmap > cons > pls > mlt

With these choices, we have:

  1] altmap(/\x.pls(x, X), cons(Y, Z)) >= cons(pls(Y, X), altmap(/\x.mlt(x, X), Z))  because [2], by (Star) 
  2] altmap*(/\x.pls(x, X), cons(Y, Z)) >= cons(pls(Y, X), altmap(/\x.mlt(x, X), Z))  because altmap > cons, [3] and [15], by (Copy) 
  3] altmap*(/\x.pls(x, X), cons(Y, Z)) >= pls(Y, X)  because altmap > pls, [4] and [8], by (Copy) 
  4] altmap*(/\x.pls(x, X), cons(Y, Z)) >= Y  because [5], by (Select) 
  5] cons(Y, Z) >= Y  because [6], by (Star) 
  6] cons*(Y, Z) >= Y  because [7], by (Select) 
  7] Y >= Y  by (Meta) 
  8] altmap*(/\x.pls(x, X), cons(Y, Z)) >= X  because [9], by (Select) 
  9] pls(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= X  because [10], by (Star) 
  10] pls*(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= X  because [11], by (Select) 
  11] altmap*(/\x.pls(x, X), cons(Y, Z)) >= X  because [12], by (Select) 
  12] pls(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= X  because [13], by (Star) 
  13] pls*(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= X  because [14], by (Select) 
  14] X >= X  by (Meta) 
  15] altmap*(/\x.pls(x, X), cons(Y, Z)) >= altmap(/\x.mlt(x, X), Z)  because altmap in Mul, [16] and [22], by (Stat) 
  16] /\x.pls(x, X) > /\x.mlt(x, X)  because [17], by definition 
  17] /\y.pls*(y, X) >= /\y.mlt(y, X)  because [18], by (Abs) 
  18] pls*(x, X) >= mlt(x, X)  because pls > mlt, [19] and [21], by (Copy) 
  19] pls*(x, X) >= x  because [20], by (Select) 
  20] x >= x  by (Var) 
  21] pls*(x, X) >= X  because [14], by (Select) 
  22] cons(Y, Z) >= Z  because [23], by (Star) 
  23] cons*(Y, Z) >= Z  because [24], by (Select) 
  24] Z >= Z  by (Meta) 

  25] pls(2, 2) > mlt(2, 2)  because [26], by definition 
  26] pls*(2, 2) >= mlt(2, 2)  because pls > mlt, [27] and [27], by (Copy) 
  27] pls*(2, 2) >= 2  because [28], by (Select) 
  28] 2 >= 2  by (Fun) 

We can thus remove the following rules:

  pls(2, 2) => mlt(2, 2) 

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

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

  altmap(/\x.pls(x, X), cons(Y, Z)) >? cons(pls(Y, X), altmap(/\y.mlt(y, X), Z)) 

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

We choose Lex = {} and Mul = {altmap, cons, mlt, pls}, and the following precedence: pls > cons > altmap > mlt

With these choices, we have:

  1] altmap(/\x.pls(x, X), cons(Y, Z)) > cons(pls(Y, X), altmap(/\x.mlt(x, X), Z))  because [2], by definition 
  2] altmap*(/\x.pls(x, X), cons(Y, Z)) >= cons(pls(Y, X), altmap(/\x.mlt(x, X), Z))  because [3], by (Select) 
  3] pls(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= cons(pls(Y, X), altmap(/\x.mlt(x, X), Z))  because [4], by (Star) 
  4] pls*(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= cons(pls(Y, X), altmap(/\x.mlt(x, X), Z))  because pls > cons, [5] and [16], by (Copy) 
  5] pls*(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= pls(Y, X)  because [6], by (Select) 
  6] altmap*(/\x.pls(x, X), cons(Y, Z)) >= pls(Y, X)  because [7], by (Select) 
  7] pls(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= pls(Y, X)  because pls in Mul, [8] and [15], by (Fun) 
  8] altmap*(/\x.pls(x, X), cons(Y, Z)) >= Y  because [9], by (Select) 
  9] pls(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= Y  because [10], by (Star) 
  10] pls*(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= Y  because [11], by (Select) 
  11] altmap*(/\x.pls(x, X), cons(Y, Z)) >= Y  because [12], by (Select) 
  12] cons(Y, Z) >= Y  because [13], by (Star) 
  13] cons*(Y, Z) >= Y  because [14], by (Select) 
  14] Y >= Y  by (Meta) 
  15] X >= X  by (Meta) 
  16] pls*(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= altmap(/\x.mlt(x, X), Z)  because pls > altmap, [17] and [26], by (Copy) 
  17] pls*(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= /\x.mlt(x, X)  because [18], by (F-Abs) 
  18] pls*(altmap*(/\x.pls(x, X), cons(Y, Z)), X, y) >= mlt(y, X)  because pls > mlt, [19] and [21], by (Copy) 
  19] pls*(altmap*(/\x.pls(x, X), cons(Y, Z)), X, y) >= y  because [20], by (Select) 
  20] y >= y  by (Var) 
  21] pls*(altmap*(/\x.pls(x, X), cons(Y, Z)), X, y) >= X  because [22], by (Select) 
  22] altmap*(/\x.pls(x, X), cons(Y, Z)) >= X  because [23], by (Select) 
  23] pls(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= X  because [24], by (Star) 
  24] pls*(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= X  because [25], by (Select) 
  25] X >= X  by (Meta) 
  26] pls*(altmap*(/\x.pls(x, X), cons(Y, Z)), X) >= Z  because [27], by (Select) 
  27] altmap*(/\x.pls(x, X), cons(Y, Z)) >= Z  because [28], by (Select) 
  28] cons(Y, Z) >= Z  because [29], by (Star) 
  29] cons*(Y, Z) >= Z  because [30], by (Select) 
  30] Z >= Z  by (Meta) 

We can thus remove the following rules:

  altmap(/\x.pls(x, X), cons(Y, Z)) => cons(pls(Y, X), altmap(/\y.mlt(y, X), Z)) 

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.