We consider the system kop11cai2.

  Alphabet:

    pair : [nat -> nat * nat] --> nat 
    split : [nat] --> nat 

  Rules:

    split(f x) => pair(f, x) 

Using the transformations described in [Kop11], this system can be brought in a form without leading free variables in the left-hand side, and where the left-hand side of a variable is always a functional term or application headed by a functional term.

We now transform the resulting AFS into an AFSM by replacing all free variables by meta-variables (with arity 0).  This leads to the following AFSM:

  Alphabet:

    pair : [nat -> nat * nat] --> nat 
    split : [nat] --> nat 
    ~AP1 : [nat -> nat * nat] --> nat 

  Rules:

    split(~AP1(F, X)) => pair(F, X) 
    ~AP1(F, X) => F 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]):

  split(~AP1(F, X)) >? pair(F, X) 
  ~AP1(F, X) >? F X 

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

We choose Lex = {} and Mul = {@_{o -> o}, pair, split, ~AP1}, and the following precedence: split > @_{o -> o} = pair = ~AP1

With these choices, we have:

  1] split(~AP1(F, X)) > pair(F, X)  because [2], by definition 
  2] split*(~AP1(F, X)) >= pair(F, X)  because [3], by (Select) 
  3] ~AP1(F, X) >= pair(F, X)  because ~AP1 = pair, ~AP1 in Mul, [4] and [5], by (Fun) 
  4] F >= F  by (Meta) 
  5] X >= X  by (Meta) 

  6] ~AP1(F, X) >= @_{o -> o}(F, X)  because ~AP1 = @_{o -> o}, ~AP1 in Mul, [7] and [8], by (Fun) 
  7] F >= F  by (Meta) 
  8] X >= X  by (Meta) 

We can thus remove the following rules:

  split(~AP1(F, X)) => pair(F, 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]):

  ~AP1(F, X) >? F X 

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

We choose Lex = {} and Mul = {@_{o -> o}, ~AP1}, and the following precedence: ~AP1 > @_{o -> o}

With these choices, we have:

  1] ~AP1(F, X) > @_{o -> o}(F, X)  because [2], by definition 
  2] ~AP1*(F, X) >= @_{o -> o}(F, X)  because ~AP1 > @_{o -> o}, [3] and [5], by (Copy) 
  3] ~AP1*(F, X) >= F  because [4], by (Select) 
  4] F >= F  by (Meta) 
  5] ~AP1*(F, X) >= X  because [6], by (Select) 
  6] X >= X  by (Meta) 

We can thus remove the following rules:

  ~AP1(F, X) => F 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 +++

[Kop11]  C. Kop.  Simplifying Algebraic Functional Systems.  In Proceedings of CAI 2011, volume 6742 of LNCS.  201--215, Springer, 2011.
[Kop12]  C. Kop.  Higher Order Termination.  PhD Thesis, 2012.