We consider the system 472.

  Alphabet:

    f : [o -> o] --> o 
    g : [o] --> o 
    h : [] --> o 
    i : [o] --> o 

  Rules:

    f(/\x.X(x)) => g(X(h)) 
    g(X) => i(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]):

  f(/\x.X(x)) >? g(X(h)) 
  g(X) >? i(X) 

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

The following interpretation satisfies the requirements:

  f = \G0.3 + 3G0(0) 
  g = \y0.y0 
  h = 0 
  i = \y0.y0 

Using this interpretation, the requirements translate to:

  [[f(/\x._x0(x))]] = 3 + 3F0(0) > F0(0) = [[g(_x0(h))]] 
  [[g(_x0)]] = x0 >= x0 = [[i(_x0)]] 

We can thus remove the following rules:

  f(/\x.X(x)) => g(X(h)) 

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

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

  g(X) >? i(X) 

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

The following interpretation satisfies the requirements:

  g = \y0.3 + 3y0 
  i = \y0.y0 

Using this interpretation, the requirements translate to:

  [[g(_x0)]] = 3 + 3x0 > x0 = [[i(_x0)]] 

We can thus remove the following rules:

  g(X) => i(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.