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 use a recursive path ordering as defined in [Kop12, Chapter 5].

Argument functions:

  [[false]] = _|_ 
  [[nil]] = _|_ 
  [[true]] = _|_ 

We choose Lex = {} and Mul = {0, 0s, 1, 1s, cmp, decide}, and the following precedence: decide > 1s > 0s = 1 > cmp > 0

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

  decide(X) >= cmp(0s(X), 1s(X)) 
  0s(_|_) >= _|_ 
  0s(0(X)) >= 0(0s(X)) 
  0s(1(X)) >= 0s(X) 
  1s(_|_) > _|_ 
  1s(1(X)) > 1(1s(X)) 
  1s(0(X)) > 1s(X) 
  cmp(0(X), 1(Y)) > cmp(X, Y) 
  cmp(0(X), _|_) >= _|_ 
  cmp(_|_, X) > _|_ 

With these choices, we have:

  1] decide(X) >= cmp(0s(X), 1s(X))  because [2], by (Star) 
  2] decide*(X) >= cmp(0s(X), 1s(X))  because decide > cmp, [3] and [6], by (Copy) 
  3] decide*(X) >= 0s(X)  because decide > 0s and [4], by (Copy) 
  4] decide*(X) >= X  because [5], by (Select) 
  5] X >= X  by (Meta) 
  6] decide*(X) >= 1s(X)  because decide > 1s and [4], by (Copy) 

  7] 0s(_|_) >= _|_  by (Bot) 

  8] 0s(0(X)) >= 0(0s(X))  because [9], by (Star) 
  9] 0s*(0(X)) >= 0(0s(X))  because 0s > 0 and [10], by (Copy) 
  10] 0s*(0(X)) >= 0s(X)  because 0s in Mul and [11], by (Stat) 
  11] 0(X) > X  because [12], by definition 
  12] 0*(X) >= X  because [13], by (Select) 
  13] X >= X  by (Meta) 

  14] 0s(1(X)) >= 0s(X)  because [15], by (Star) 
  15] 0s*(1(X)) >= 0s(X)  because [16], by (Select) 
  16] 1(X) >= 0s(X)  because 1 = 0s, 1 in Mul and [17], by (Fun) 
  17] X >= X  by (Meta) 

  18] 1s(_|_) > _|_  because [19], by definition 
  19] 1s*(_|_) >= _|_  by (Bot) 

  20] 1s(1(X)) > 1(1s(X))  because [21], by definition 
  21] 1s*(1(X)) >= 1(1s(X))  because 1s > 1 and [22], by (Copy) 
  22] 1s*(1(X)) >= 1s(X)  because 1s in Mul and [23], by (Stat) 
  23] 1(X) > X  because [24], by definition 
  24] 1*(X) >= X  because [25], by (Select) 
  25] X >= X  by (Meta) 

  26] 1s(0(X)) > 1s(X)  because [27], by definition 
  27] 1s*(0(X)) >= 1s(X)  because 1s in Mul and [28], by (Stat) 
  28] 0(X) > X  because [29], by definition 
  29] 0*(X) >= X  because [30], by (Select) 
  30] X >= X  by (Meta) 

  31] cmp(0(X), 1(Y)) > cmp(X, Y)  because [32], by definition 
  32] cmp*(0(X), 1(Y)) >= cmp(X, Y)  because cmp in Mul, [33] and [36], by (Stat) 
  33] 0(X) >= X  because [34], by (Star) 
  34] 0*(X) >= X  because [35], by (Select) 
  35] X >= X  by (Meta) 
  36] 1(Y) > Y  because [37], by definition 
  37] 1*(Y) >= Y  because [38], by (Select) 
  38] Y >= Y  by (Meta) 

  39] cmp(0(X), _|_) >= _|_  by (Bot) 

  40] cmp(_|_, X) > _|_  because [41], by definition 
  41] cmp*(_|_, X) >= _|_  by (Bot) 

We can thus remove the following rules:

  1s(nil) => nil 
  1s(1(X)) => 1(1s(X)) 
  1s(0(X)) => 1s(X) 
  cmp(0(X), 1(Y)) => cmp(X, Y) 
  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) 
  cmp(0(X), nil) >? false 

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

Argument functions:

  [[0s(x_1)]] = x_1 
  [[1(x_1)]] = x_1 
  [[1s(x_1)]] = x_1 
  [[false]] = _|_ 
  [[nil]] = _|_ 

We choose Lex = {} and Mul = {0, cmp, decide}, and the following precedence: decide > 0 > cmp

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

  decide(X) >= cmp(X, X) 
  _|_ >= _|_ 
  0(X) >= 0(X) 
  X >= X 
  cmp(0(X), _|_) > _|_ 

With these choices, we have:

  1] decide(X) >= cmp(X, X)  because [2], by (Star) 
  2] decide*(X) >= cmp(X, X)  because decide > cmp, [3] and [5], by (Copy) 
  3] decide*(X) >= X  because [4], by (Select) 
  4] X >= X  by (Meta) 
  5] decide*(X) >= X  because [4], by (Select) 

  6] _|_ >= _|_  by (Bot) 

  7] 0(X) >= 0(X)  because 0 in Mul and [8], by (Fun) 
  8] X >= X  by (Meta) 

  9] X >= X  by (Meta) 

  10] cmp(0(X), _|_) > _|_  because [11], by definition 
  11] cmp*(0(X), _|_) >= _|_  by (Bot) 

We can thus remove the following rules:

  cmp(0(X), nil) => false 

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) 

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

Argument functions:

  [[1s(x_1)]] = x_1 
  [[nil]] = _|_ 

We choose Lex = {} and Mul = {0, 0s, 1, cmp, decide}, and the following precedence: decide > 0s > 1 > 0 > cmp

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

  decide(X) >= cmp(0s(X), X) 
  0s(_|_) >= _|_ 
  0s(0(X)) > 0(0s(X)) 
  0s(1(X)) >= 0s(X) 

With these choices, we have:

  1] decide(X) >= cmp(0s(X), X)  because [2], by (Star) 
  2] decide*(X) >= cmp(0s(X), X)  because decide > cmp, [3] and [6], by (Copy) 
  3] decide*(X) >= 0s(X)  because decide > 0s and [4], by (Copy) 
  4] decide*(X) >= X  because [5], by (Select) 
  5] X >= X  by (Meta) 
  6] decide*(X) >= X  because [5], by (Select) 

  7] 0s(_|_) >= _|_  by (Bot) 

  8] 0s(0(X)) > 0(0s(X))  because [9], by definition 
  9] 0s*(0(X)) >= 0(0s(X))  because 0s > 0 and [10], by (Copy) 
  10] 0s*(0(X)) >= 0s(X)  because 0s in Mul and [11], by (Stat) 
  11] 0(X) > X  because [12], by definition 
  12] 0*(X) >= X  because [13], by (Select) 
  13] X >= X  by (Meta) 

  14] 0s(1(X)) >= 0s(X)  because 0s in Mul and [15], by (Fun) 
  15] 1(X) >= X  because [16], by (Star) 
  16] 1*(X) >= X  because [17], by (Select) 
  17] X >= X  by (Meta) 

We can thus remove the following rules:

  0s(0(X)) => 0(0s(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]):

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

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

Argument functions:

  [[0s(x_1)]] = x_1 

We choose Lex = {} and Mul = {1, 1s, cmp, decide, nil}, and the following precedence: 1 > decide > nil > 1s > cmp

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

  decide(X) >= cmp(X, 1s(X)) 
  nil >= nil 
  1(X) > X 

With these choices, we have:

  1] decide(X) >= cmp(X, 1s(X))  because [2], by (Star) 
  2] decide*(X) >= cmp(X, 1s(X))  because decide > cmp, [3] and [5], by (Copy) 
  3] decide*(X) >= X  because [4], by (Select) 
  4] X >= X  by (Meta) 
  5] decide*(X) >= 1s(X)  because decide > 1s and [3], by (Copy) 

  6] nil >= nil  by (Fun) 

  7] 1(X) > X  because [8], by definition 
  8] 1*(X) >= X  because [9], by (Select) 
  9] X >= X  by (Meta) 

We can thus remove the following rules:

  0s(1(X)) => 0s(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]):

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

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

Argument functions:

  [[1s(x_1)]] = x_1 

We choose Lex = {} and Mul = {0s, cmp, decide, nil}, and the following precedence: decide > 0s > cmp > nil

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

  decide(X) >= cmp(0s(X), X) 
  0s(nil) > nil 

With these choices, we have:

  1] decide(X) >= cmp(0s(X), X)  because [2], by (Star) 
  2] decide*(X) >= cmp(0s(X), X)  because decide > cmp, [3] and [6], by (Copy) 
  3] decide*(X) >= 0s(X)  because decide > 0s and [4], by (Copy) 
  4] decide*(X) >= X  because [5], by (Select) 
  5] X >= X  by (Meta) 
  6] decide*(X) >= X  because [5], by (Select) 

  7] 0s(nil) > nil  because [8], by definition 
  8] 0s*(nil) >= nil  because 0s > nil, by (Copy) 

We can thus remove the following rules:

  0s(nil) => nil 

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)) 

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

Argument functions:

  [[0s(x_1)]] = x_1 

We choose Lex = {} and Mul = {1s, cmp, decide}, and the following precedence: decide > cmp > 1s

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

  decide(X) > cmp(X, 1s(X)) 

With these choices, we have:

  1] decide(X) > cmp(X, 1s(X))  because [2], by definition 
  2] decide*(X) >= cmp(X, 1s(X))  because decide > cmp, [3] and [5], by (Copy) 
  3] decide*(X) >= X  because [4], by (Select) 
  4] X >= X  by (Meta) 
  5] decide*(X) >= 1s(X)  because decide > 1s and [3], by (Copy) 

We can thus remove the following rules:

  decide(X) => cmp(0s(X), 1s(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 +++

[Kop12]  C. Kop.  Higher Order Termination.  PhD Thesis, 2012.