We consider the system 476.

  Alphabet:

    f : [a * a -> a] --> a 
    h : [a * a -> a] --> a 
    i : [a] --> a 

  Rules:

    f(X, /\x.x) => h(X, /\y.y) 
    h(f(X, /\x.x), /\y.y) => f(i(X), /\z.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]):

  f(X, /\x.x) >? h(X, /\y.y) 
  h(f(X, /\x.x), /\y.y) >? f(i(X), /\z.z) 

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

Argument functions:

  [[i(x_1)]] = x_1 

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

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

  f(X, /\x.x) >= h(X, /\x.x) 
  h(f(X, /\x.x), /\y.y) > f(X, /\x.x) 

With these choices, we have:

  1] f(X, /\x.x) >= h(X, /\x.x)  because f = h, f in Mul, [2] and [3], by (Fun) 
  2] X >= X  by (Meta) 
  3] /\y.y >= /\y.y  because [4], by (Abs) 
  4] x >= x  by (Var) 

  5] h(f(X, /\x.x), /\y.y) > f(X, /\x.x)  because [6], by definition 
  6] h*(f(X, /\x.x), /\y.y) >= f(X, /\x.x)  because [7], by (Select) 
  7] f(X, /\x.x) >= f(X, /\x.x)  because f in Mul, [8] and [3], by (Fun) 
  8] X >= X  by (Meta) 

We can thus remove the following rules:

  h(f(X, /\x.x), /\y.y) => f(i(X), /\z.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]):

  f(X, /\x.x) >? h(X, /\y.y) 

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

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

With these choices, we have:

  1] f(X, /\x.x) > h(X, /\x.x)  because [2], by definition 
  2] f*(X, /\x.x) >= h(X, /\x.x)  because f > h, [3] and [5], by (Copy) 
  3] f*(X, /\x.x) >= X  because [4], by (Select) 
  4] X >= X  by (Meta) 
  5] f*(X, /\x.x) >= /\x.x  because [6], by (Select) 
  6] /\y.y >= /\y.y  because [7], by (Abs) 
  7] x >= x  by (Var) 

We can thus remove the following rules:

  f(X, /\x.x) => h(X, /\y.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.