We consider the system 454.

  Alphabet:

    a : [] --> o 
    f : [o] --> o 
    g : [o -> o] --> o 
    h : [o] --> o 
    hprime : [o] --> o 

  Rules:

    f(g(/\x.X(x))) => f(X(X(a))) 
    g(/\x.hprime(x)) => h(h(a)) 
    h(X) => hprime(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]):

  f(g(/\x.X(x))) >? f(X(X(a))) 
  g(/\x.hprime(x)) >? h(h(a)) 
  h(X) >? hprime(X) 

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

Argument functions:

  [[a]] = _|_ 

We choose Lex = {} and Mul = {f, g, h, hprime}, and the following precedence: g > h > hprime > f

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

  f(g(/\x.X(x))) >= f(X(X(_|_))) 
  g(/\x.hprime(x)) > h(h(_|_)) 
  h(X) >= hprime(X) 

With these choices, we have:

  1] f(g(/\x.X(x))) >= f(X(X(_|_)))  because f in Mul and [2], by (Fun) 
  2] g(/\x.X(x)) >= X(X(_|_))  because [3], by (Star) 
  3] g*(/\x.X(x)) >= X(X(_|_))  because [4], by (Select) 
  4] X(g*(/\x.X(x))) >= X(X(_|_))  because [5], by (Meta) 
  5] g*(/\x.X(x)) >= X(_|_)  because [6], by (Select) 
  6] X(g*(/\x.X(x))) >= X(_|_)  because [7], by (Meta) 
  7] g*(/\x.X(x)) >= _|_  by (Bot) 

  8] g(/\x.hprime(x)) > h(h(_|_))  because [9], by definition 
  9] g*(/\x.hprime(x)) >= h(h(_|_))  because g > h and [10], by (Copy) 
  10] g*(/\x.hprime(x)) >= h(_|_)  because g > h and [11], by (Copy) 
  11] g*(/\x.hprime(x)) >= _|_  by (Bot) 

  12] h(X) >= hprime(X)  because [13], by (Star) 
  13] h*(X) >= hprime(X)  because h > hprime and [14], by (Copy) 
  14] h*(X) >= X  because [15], by (Select) 
  15] X >= X  by (Meta) 

We can thus remove the following rules:

  g(/\x.hprime(x)) => h(h(a)) 

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(g(/\x.X(x))) >? f(X(X(a))) 
  h(X) >? hprime(X) 

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

Argument functions:

  [[a]] = _|_ 
  [[hprime(x_1)]] = x_1 

We choose Lex = {} and Mul = {f, g, h}, and the following precedence: g > f > h

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

  f(g(/\x.X(x))) >= f(X(X(_|_))) 
  h(X) > X 

With these choices, we have:

  1] f(g(/\x.X(x))) >= f(X(X(_|_)))  because f in Mul and [2], by (Fun) 
  2] g(/\x.X(x)) >= X(X(_|_))  because [3], by (Star) 
  3] g*(/\x.X(x)) >= X(X(_|_))  because [4], by (Select) 
  4] X(g*(/\x.X(x))) >= X(X(_|_))  because [5], by (Meta) 
  5] g*(/\x.X(x)) >= X(_|_)  because [6], by (Select) 
  6] X(g*(/\x.X(x))) >= X(_|_)  because [7], by (Meta) 
  7] g*(/\x.X(x)) >= _|_  by (Bot) 

  8] h(X) > X  because [9], by definition 
  9] h*(X) >= X  because [10], by (Select) 
  10] X >= X  by (Meta) 

We can thus remove the following rules:

  h(X) => hprime(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]):

  f(g(/\x.X(x))) >? f(X(X(a))) 

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

Argument functions:

  [[a]] = _|_ 

We choose Lex = {} and Mul = {f, g}, and the following precedence: g > f

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

  f(g(/\x.X(x))) > f(X(X(_|_))) 

With these choices, we have:

  1] f(g(/\x.X(x))) > f(X(X(_|_)))  because [2], by definition 
  2] f*(g(/\x.X(x))) >= f(X(X(_|_)))  because [3], by (Select) 
  3] g(/\x.X(x)) >= f(X(X(_|_)))  because [4], by (Star) 
  4] g*(/\x.X(x)) >= f(X(X(_|_)))  because g > f and [5], by (Copy) 
  5] g*(/\x.X(x)) >= X(X(_|_))  because [6], by (Select) 
  6] X(g*(/\x.X(x))) >= X(X(_|_))  because [7], by (Meta) 
  7] g*(/\x.X(x)) >= X(_|_)  because [8], by (Select) 
  8] X(g*(/\x.X(x))) >= X(_|_)  because [9], by (Meta) 
  9] g*(/\x.X(x)) >= _|_  by (Bot) 

We can thus remove the following rules:

  f(g(/\x.X(x))) => f(X(X(a))) 

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.