We consider the system 482.

  Alphabet:

    apply : [o -> o * o] --> o 
    compo : [o -> o * o -> o * o] --> o 

  Rules:

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

  compo(/\x.X(x), /\y.Y(y), Z) >? X(Y(Z)) 
  apply(/\x.X(x), Y) >? X(Y) 

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

We choose Lex = {} and Mul = {apply, compo}, and the following precedence: apply > compo

With these choices, we have:

  1] compo(/\x.X(x), /\y.Y(y), Z) > X(Y(Z))  because [2], by definition 
  2] compo*(/\x.X(x), /\y.Y(y), Z) >= X(Y(Z))  because [3], by (Select) 
  3] X(compo*(/\x.X(x), /\y.Y(y), Z)) >= X(Y(Z))  because [4], by (Meta) 
  4] compo*(/\x.X(x), /\y.Y(y), Z) >= Y(Z)  because [5], by (Select) 
  5] Y(compo*(/\x.X(x), /\y.Y(y), Z)) >= Y(Z)  because [6], by (Meta) 
  6] compo*(/\x.X(x), /\y.Y(y), Z) >= Z  because [7], by (Select) 
  7] Z >= Z  by (Meta) 

  8] apply(/\x.X(x), Y) >= X(Y)  because [9], by (Star) 
  9] apply*(/\x.X(x), Y) >= X(Y)  because [10], by (Select) 
  10] X(apply*(/\x.X(x), Y)) >= X(Y)  because [11], by (Meta) 
  11] apply*(/\x.X(x), Y) >= Y  because [12], by (Select) 
  12] Y >= Y  by (Meta) 

We can thus remove the following rules:

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

  apply(/\x.X(x), Y) >? X(Y) 

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

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

With these choices, we have:

  1] apply(/\x.X(x), Y) > X(Y)  because [2], by definition 
  2] apply*(/\x.X(x), Y) >= X(Y)  because [3], by (Select) 
  3] X(apply*(/\x.X(x), Y)) >= X(Y)  because [4], by (Meta) 
  4] apply*(/\x.X(x), Y) >= Y  because [5], by (Select) 
  5] Y >= Y  by (Meta) 

We can thus remove the following rules:

  apply(/\x.X(x), Y) => X(Y) 

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.