We consider the system 455.

  Alphabet:

    pi : [term * term] --> term 
    pi1 : [term] --> term 
    pi2 : [term] --> term 

  Rules:

    pi1(pi(X, Y)) => X 
    pi2(pi(X, Y)) => Y 
    pi(pi1(X), pi2(X)) => 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]):

  pi1(pi(X, Y)) >? X 
  pi2(pi(X, Y)) >? Y 
  pi(pi1(X), pi2(X)) >? X 

We use a recursive path ordering as defined in [Kop12, Chapter 5].

Argument functions:

  [[pi1(x_1)]] = x_1 

We choose Lex = {} and Mul = {pi, pi2}, and the following precedence: pi > pi2

Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows:

  pi(X, Y) > X 
  pi2(pi(X, Y)) > Y 
  pi(X, pi2(X)) >= X 

With these choices, we have:

  1] pi(X, Y) > X  because [2], by definition 
  2] pi*(X, Y) >= X  because [3], by (Select) 
  3] X >= X  by (Meta) 

  4] pi2(pi(X, Y)) > Y  because [5], by definition 
  5] pi2*(pi(X, Y)) >= Y  because [6], by (Select) 
  6] pi(X, Y) >= Y  because [7], by (Star) 
  7] pi*(X, Y) >= Y  because [8], by (Select) 
  8] Y >= Y  by (Meta) 

  9] pi(X, pi2(X)) >= X  because [10], by (Star) 
  10] pi*(X, pi2(X)) >= X  because [11], by (Select) 
  11] X >= X  by (Meta) 

We can thus remove the following rules:

  pi1(pi(X, Y)) => X 
  pi2(pi(X, Y)) => Y 

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

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

  pi(pi1(X), pi2(X)) >? X 

We use a recursive path ordering as defined in [Kop12, Chapter 5].

Argument functions:

  [[pi1(x_1)]] = x_1 
  [[pi2(x_1)]] = x_1 

We choose Lex = {} and Mul = {pi}, and the following precedence: pi

Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows:

  pi(X, X) > X 

With these choices, we have:

  1] pi(X, X) > X  because [2], by definition 
  2] pi*(X, X) >= X  because [3], by (Select) 
  3] X >= X  by (Meta) 

We can thus remove the following rules:

  pi(pi1(X), pi2(X)) => 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.