We consider the system 521.

  Alphabet:

    0 : [string] --> string 
    0s : [string] --> string 
    1 : [string] --> string 
    1s : [string] --> string 
    cmp : [string * string] --> bool 
    decide : [string] --> bool 
    false : [] --> bool 
    nil : [] --> string 
    true : [] --> bool 

  Rules:

    decide(X) => cmp(0s(X), 1s(X)) 
    0s(nil) => nil 
    0s(0(X)) => 0(0s(X)) 
    0s(1(X)) => 0s(X) 
    1s(nil) => nil 
    1s(1(X)) => 1(1s(X)) 
    1s(0(X)) => 1s(X) 
    cmp(0(X), 1(Y)) => cmp(X, Y) 
    cmp(0(X), nil) => false 
    cmp(nil, X) => true 

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

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

  decide(X) >? cmp(0s(X), 1s(X)) 
  0s(nil) >? nil 
  0s(0(X)) >? 0(0s(X)) 
  0s(1(X)) >? 0s(X) 
  1s(nil) >? nil 
  1s(1(X)) >? 1(1s(X)) 
  1s(0(X)) >? 1s(X) 
  cmp(0(X), 1(Y)) >? cmp(X, Y) 
  cmp(0(X), nil) >? false 
  cmp(nil, X) >? true 

We orient these requirements with a polynomial interpretation in the natural numbers.

The following interpretation satisfies the requirements:

  0 = \y0.2y0 
  0s = \y0.y0 
  1 = \y0.3 + 2y0 
  1s = \y0.2 + 2y0 
  cmp = \y0y1.y0 + y1 
  decide = \y0.3 + 3y0 
  false = 0 
  nil = 0 
  true = 0 

Using this interpretation, the requirements translate to:

  [[decide(_x0)]] = 3 + 3x0 > 2 + 3x0 = [[cmp(0s(_x0), 1s(_x0))]] 
  [[0s(nil)]] = 0 >= 0 = [[nil]] 
  [[0s(0(_x0))]] = 2x0 >= 2x0 = [[0(0s(_x0))]] 
  [[0s(1(_x0))]] = 3 + 2x0 > x0 = [[0s(_x0)]] 
  [[1s(nil)]] = 2 > 0 = [[nil]] 
  [[1s(1(_x0))]] = 8 + 4x0 > 7 + 4x0 = [[1(1s(_x0))]] 
  [[1s(0(_x0))]] = 2 + 4x0 >= 2 + 2x0 = [[1s(_x0)]] 
  [[cmp(0(_x0), 1(_x1))]] = 3 + 2x0 + 2x1 > x0 + x1 = [[cmp(_x0, _x1)]] 
  [[cmp(0(_x0), nil)]] = 2x0 >= 0 = [[false]] 
  [[cmp(nil, _x0)]] = x0 >= 0 = [[true]] 

We can thus remove the following rules:

  decide(X) => cmp(0s(X), 1s(X)) 
  0s(1(X)) => 0s(X) 
  1s(nil) => nil 
  1s(1(X)) => 1(1s(X)) 
  cmp(0(X), 1(Y)) => cmp(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]):

  0s(nil) >? nil 
  0s(0(X)) >? 0(0s(X)) 
  1s(0(X)) >? 1s(X) 
  cmp(0(X), nil) >? false 
  cmp(nil, X) >? true 

We orient these requirements with a polynomial interpretation in the natural numbers.

The following interpretation satisfies the requirements:

  0 = \y0.3 + y0 
  0s = \y0.2 + 3y0 
  1s = \y0.y0 
  cmp = \y0y1.3 + 3y0 + 3y1 
  false = 0 
  nil = 0 
  true = 0 

Using this interpretation, the requirements translate to:

  [[0s(nil)]] = 2 > 0 = [[nil]] 
  [[0s(0(_x0))]] = 11 + 3x0 > 5 + 3x0 = [[0(0s(_x0))]] 
  [[1s(0(_x0))]] = 3 + x0 > x0 = [[1s(_x0)]] 
  [[cmp(0(_x0), nil)]] = 12 + 3x0 > 0 = [[false]] 
  [[cmp(nil, _x0)]] = 3 + 3x0 > 0 = [[true]] 

We can thus remove the following rules:

  0s(nil) => nil 
  0s(0(X)) => 0(0s(X)) 
  1s(0(X)) => 1s(X) 
  cmp(0(X), nil) => false 
  cmp(nil, X) => true 

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.