We consider the system 730.

  Alphabet:

    get : [S] --> V 
    put : [S * V] --> S 

  Rules:

    put(X, get(X)) => X 
    get(put(X, Y)) => Y 
    put(put(X, Y), Y) => put(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]):

  put(X, get(X)) >? X 
  get(put(X, Y)) >? Y 
  put(put(X, Y), Y) >? put(X, Y) 

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

We choose Lex = {} and Mul = {get, put}, and the following precedence: put > get

With these choices, we have:

  1] put(X, get(X)) > X  because [2], by definition 
  2] put*(X, get(X)) >= X  because [3], by (Select) 
  3] X >= X  by (Meta) 

  4] get(put(X, Y)) >= Y  because [5], by (Star) 
  5] get*(put(X, Y)) >= Y  because [6], by (Select) 
  6] put(X, Y) >= Y  because [7], by (Star) 
  7] put*(X, Y) >= Y  because [8], by (Select) 
  8] Y >= Y  by (Meta) 

  9] put(put(X, Y), Y) >= put(X, Y)  because put in Mul, [10] and [13], by (Fun) 
  10] put(X, Y) >= X  because [11], by (Star) 
  11] put*(X, Y) >= X  because [12], by (Select) 
  12] X >= X  by (Meta) 
  13] Y >= Y  by (Meta) 

We can thus remove the following rules:

  put(X, get(X)) => 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]):

  get(put(X, Y)) >? Y 
  put(put(X, Y), Y) >? put(X, Y) 

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

We choose Lex = {} and Mul = {get, put}, and the following precedence: get > put

With these choices, we have:

  1] get(put(X, Y)) >= Y  because [2], by (Star) 
  2] get*(put(X, Y)) >= Y  because [3], by (Select) 
  3] put(X, Y) >= Y  because [4], by (Star) 
  4] put*(X, Y) >= Y  because [5], by (Select) 
  5] Y >= Y  by (Meta) 

  6] put(put(X, Y), Y) > put(X, Y)  because [7], by definition 
  7] put*(put(X, Y), Y) >= put(X, Y)  because [8], by (Select) 
  8] put(X, Y) >= put(X, Y)  because put in Mul, [9] and [10], by (Fun) 
  9] X >= X  by (Meta) 
  10] Y >= Y  by (Meta) 

We can thus remove the following rules:

  put(put(X, Y), Y) => put(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]):

  get(put(X, Y)) >? Y 

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

Argument functions:

  [[get(x_1)]] = x_1 

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

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

  put(X, Y) > Y 

With these choices, we have:

  1] put(X, Y) > Y  because [2], by definition 
  2] put*(X, Y) >= Y  because [3], by (Select) 
  3] Y >= Y  by (Meta) 

We can thus remove the following rules:

  get(put(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.