We consider the system 470.

  Alphabet:

    L : [o] --> o 
    P : [o * o -> o * o -> o] --> o 
    R : [o] --> o 

  Rules:

    P(L(X), /\x.Y(x), /\y.Z(y)) => Y(X) 
    P(R(X), /\x.Y(x), /\y.Z(y)) => Z(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]):

  P(L(X), /\x.Y(x), /\y.Z(y)) >? Y(X) 
  P(R(X), /\x.Y(x), /\y.Z(y)) >? Z(X) 

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

The following interpretation satisfies the requirements:

  L = \y0.3 + y0 
  P = \y0G1G2.3 + y0 + G1(0) + G2(y0) + y0G1(y0) 
  R = \y0.3 + y0 

Using this interpretation, the requirements translate to:

  [[P(L(_x0), /\x._x1(x), /\y._x2(y))]] = 6 + x0 + F1(0) + F2(3 + x0) + 3F1(3 + x0) + x0F1(3 + x0) > F1(x0) = [[_x1(_x0)]] 
  [[P(R(_x0), /\x._x1(x), /\y._x2(y))]] = 6 + x0 + F1(0) + F2(3 + x0) + 3F1(3 + x0) + x0F1(3 + x0) > F2(x0) = [[_x2(_x0)]] 

We can thus remove the following rules:

  P(L(X), /\x.Y(x), /\y.Z(y)) => Y(X) 
  P(R(X), /\x.Y(x), /\y.Z(y)) => Z(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.