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 the dependency pair framework as described in [Kop12, Ch. 6/7], with dynamic dependency pairs.

We thus obtain the following dependency pair problem (P_0, R_0, minimal, formative):

  Dependency Pairs P_0:

    0] P#(L(X), /\x.Y(x), /\y.Z(y)) =#> Y(X)   
    1] P#(R(X), /\x.Y(x), /\y.Z(y)) =#> Z(X)   

  Rules R_0:

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

Thus, the original system is terminating if (P_0, R_0, minimal, formative) is finite.

We consider the dependency pair problem (P_0, R_0, minimal, formative).

We will use the reduction pair processor [Kop12, Thm. 7.16].  As the system is abstraction-simple and the formative flag is set, it suffices to find a tagged reduction pair [Kop12, Def. 6.70].  Thus, we must orient:

  P#(L(X), /\x.Y(x), /\y.Z(y)) >? Y(X) 
  P#(R(X), /\x.Y(x), /\y.Z(y)) >? Z(X) 
  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.G2(y0) + y0G1(y0) 
  P# = \y0G1G2.3 + G2(y0) + y0G1(y0) 
  R = \y0.3 + y0 

Using this interpretation, the requirements translate to:

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

By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_0, R_0) by ({}, R_0).  By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed.

As all dependency pair problems were succesfully simplified with sound (and complete) processors until nothing remained, we conclude termination.


+++ Citations +++

[Kop12]  C. Kop.  Higher Order Termination.  PhD Thesis, 2012.