We consider the system 476.

  Alphabet:

    f : [a * a -> a] --> a 
    h : [a * a -> a] --> a 
    i : [a] --> a 

  Rules:

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

  f(X, /\x.x) >? h(X, /\y.y) 
  h(f(X, /\x.x), /\y.y) >? f(i(X), /\z.z) 

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

The following interpretation satisfies the requirements:

  f = \y0G1.2 + 3y0 + 2G1(0) + 2G1(y0) + 3y0G1(y0) 
  h = \y0G1.3y0 + G1(0) 
  i = \y0.y0 

Using this interpretation, the requirements translate to:

  [[f(_x0, /\x.x)]] = 2 + 3x0x0 + 5x0 > 3x0 = [[h(_x0, /\x.x)]] 
  [[h(f(_x0, /\x.x), /\y.y)]] = 6 + 9x0x0 + 15x0 > 2 + 3x0x0 + 5x0 = [[f(i(_x0), /\x.x)]] 

We can thus remove the following rules:

  f(X, /\x.x) => h(X, /\y.y) 
  h(f(X, /\x.x), /\y.y) => f(i(X), /\z.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.