We consider the system 04arrow.

  Alphabet:

    and : [c * c] --> c 
    arrow : [t * t] --> t 
    lessthan : [t * t] --> c 

  Rules:

    lessthan(arrow(x, y), arrow(z, u)) => and(lessthan(z, x), lessthan(y, u)) 

This AFS is converted to an AFSM simply by replacing all free variables by meta-variables (with arity 0).

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

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

  lessthan(arrow(X, Y), arrow(Z, U)) >? and(lessthan(Z, X), lessthan(Y, U)) 

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

We choose Lex = {} and Mul = {and, arrow, lessthan}, and the following precedence: lessthan > and > arrow

With these choices, we have:

  1] lessthan(arrow(X, Y), arrow(Z, U)) > and(lessthan(Z, X), lessthan(Y, U))  because [2], by definition 
  2] lessthan*(arrow(X, Y), arrow(Z, U)) >= and(lessthan(Z, X), lessthan(Y, U))  because lessthan > and, [3] and [10], by (Copy) 
  3] lessthan*(arrow(X, Y), arrow(Z, U)) >= lessthan(Z, X)  because lessthan in Mul, [4] and [7], by (Stat) 
  4] arrow(X, Y) >= X  because [5], by (Star) 
  5] arrow*(X, Y) >= X  because [6], by (Select) 
  6] X >= X  by (Meta) 
  7] arrow(Z, U) > Z  because [8], by definition 
  8] arrow*(Z, U) >= Z  because [9], by (Select) 
  9] Z >= Z  by (Meta) 
  10] lessthan*(arrow(X, Y), arrow(Z, U)) >= lessthan(Y, U)  because lessthan in Mul, [11] and [14], by (Stat) 
  11] arrow(X, Y) >= Y  because [12], by (Star) 
  12] arrow*(X, Y) >= Y  because [13], by (Select) 
  13] Y >= Y  by (Meta) 
  14] arrow(Z, U) > U  because [15], by definition 
  15] arrow*(Z, U) >= U  because [16], by (Select) 
  16] U >= U  by (Meta) 

We can thus remove the following rules:

  lessthan(arrow(X, Y), arrow(Z, U)) => and(lessthan(Z, X), lessthan(Y, U)) 

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.