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 orient these requirements with a polynomial interpretation in the natural numbers.

The following interpretation satisfies the requirements:

  2 = 0 
  altmap = \G0y1.3y1 + 2y1G0(y1) + 2G0(0) 
  cons = \y0y1.3 + y0 + y1 
  mlt = \y0y1.y0 + 2y1 
  nil = 1 
  pls = \y0y1.y0 + 2y1 
  plus = \y0y1.y0 + y1 
  star = \y0y1.y0 + y1 

Using this interpretation, the requirements translate to:

  [[altmap(/\x.pls(x, _x0), cons(_x1, _x2))]] = 27 + 2x1x1 + 2x2x2 + 4x0x1 + 4x0x2 + 4x1x2 + 15x1 + 15x2 + 16x0 > 3 + x1 + 2x2x2 + 3x2 + 4x0x2 + 6x0 = [[cons(pls(_x1, _x0), altmap(/\x.mlt(x, _x0), _x2))]] 
  [[altmap(/\x.mlt(x, _x0), cons(_x1, _x2))]] = 27 + 2x1x1 + 2x2x2 + 4x0x1 + 4x0x2 + 4x1x2 + 15x1 + 15x2 + 16x0 > 3 + x1 + 2x2x2 + 3x2 + 4x0x2 + 6x0 = [[cons(mlt(_x1, _x0), altmap(/\x.pls(x, _x0), _x2))]] 
  [[altmap(/\x._x0(x), nil)]] = 3 + 2F0(0) + 2F0(1) > 1 = [[nil]] 
  [[pls(_x0, _x1)]] = x0 + 2x1 >= x0 + x1 = [[plus(_x0, _x1)]] 
  [[mlt(_x0, _x1)]] = x0 + 2x1 >= x0 + x1 = [[star(_x0, _x1)]] 
  [[pls(2, 2)]] = 0 >= 0 = [[mlt(2, 2)]] 

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

  pls(X, Y) >? plus(X, Y) 
  mlt(X, Y) >? star(X, Y) 
  pls(2, 2) >? mlt(2, 2) 

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

The following interpretation satisfies the requirements:

  2 = 3 
  mlt = \y0y1.y0 + y1 
  pls = \y0y1.3 + 3y0 + 3y1 
  plus = \y0y1.y0 + y1 
  star = \y0y1.y0 + y1 

Using this interpretation, the requirements translate to:

  [[pls(_x0, _x1)]] = 3 + 3x0 + 3x1 > x0 + x1 = [[plus(_x0, _x1)]] 
  [[mlt(_x0, _x1)]] = x0 + x1 >= x0 + x1 = [[star(_x0, _x1)]] 
  [[pls(2, 2)]] = 21 > 6 = [[mlt(2, 2)]] 

We can thus remove the following rules:

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

  mlt(X, Y) >? star(X, Y) 

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

The following interpretation satisfies the requirements:

  mlt = \y0y1.3 + 3y0 + 3y1 
  star = \y0y1.y0 + y1 

Using this interpretation, the requirements translate to:

  [[mlt(_x0, _x1)]] = 3 + 3x0 + 3x1 > x0 + x1 = [[star(_x0, _x1)]] 

We can thus remove the following rules:

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