We consider the system 428.

  Alphabet:

    0 : [] --> nat 
    a : [nat * nat] --> nat 
    s : [nat] --> nat 
    sum : [nat * nat -> nat] --> nat 

  Rules:

    sum(0, /\x.X(x)) => X(0) 
    sum(s(X), /\x.Y(x)) => a(sum(X, /\y.Y(y)), Y(s(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]):

  sum(0, /\x.X(x)) >? X(0) 
  sum(s(X), /\x.Y(x)) >? a(sum(X, /\y.Y(y)), Y(s(X))) 

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

The following interpretation satisfies the requirements:

  0 = 2 
  a = \y0y1.y0 + y1 
  s = \y0.3 + 3y0 
  sum = \y0G1.3y0 + G1(0) + G1(y0) + 2y0G1(y0) 

Using this interpretation, the requirements translate to:

  [[sum(0, /\x._x0(x))]] = 6 + F0(0) + 5F0(2) > F0(2) = [[_x0(0)]] 
  [[sum(s(_x0), /\x._x1(x))]] = 9 + 9x0 + F1(0) + 6x0F1(3 + 3x0) + 7F1(3 + 3x0) > 3x0 + F1(0) + F1(x0) + F1(3 + 3x0) + 2x0F1(x0) = [[a(sum(_x0, /\x._x1(x)), _x1(s(_x0)))]] 

We can thus remove the following rules:

  sum(0, /\x.X(x)) => X(0) 
  sum(s(X), /\x.Y(x)) => a(sum(X, /\y.Y(y)), Y(s(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.