We consider the system 520.

  Alphabet:

    0 : [string] --> string 
    1 : [string] --> string 
    false : [] --> bool 
    fold : [bool -> bool * bool -> bool * bool * string] --> bool 
    nil : [] --> string 
    not : [bool] --> bool 
    true : [] --> bool 

  Rules:

    not(true) => false 
    not(false) => true 
    fold(/\x.X(x), /\y.Y(y), Z, nil) => Z 
    fold(/\x.X(x), /\y.Y(y), Z, 0(U)) => fold(/\z.X(z), /\u.Y(u), X(Z), U) 
    fold(/\x.X(x), /\y.Y(y), Z, 1(U)) => fold(/\z.X(z), /\u.Y(u), Y(Z), U) 
    0(1(X)) => 1(0(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]):

  not(true) >? false 
  not(false) >? true 
  fold(/\x.X(x), /\y.Y(y), Z, nil) >? Z 
  fold(/\x.X(x), /\y.Y(y), Z, 0(U)) >? fold(/\z.X(z), /\u.Y(u), X(Z), U) 
  fold(/\x.X(x), /\y.Y(y), Z, 1(U)) >? fold(/\z.X(z), /\u.Y(u), Y(Z), U) 
  0(1(X)) >? 1(0(X)) 

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

Argument functions:

  [[false]] = _|_ 
  [[fold(x_1, x_2, x_3, x_4)]] = fold(x_4, x_3, x_1, x_2) 
  [[true]] = _|_ 

We choose Lex = {fold} and Mul = {0, 1, nil, not}, and the following precedence: 0 > 1 > fold > nil > not

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

  not(_|_) >= _|_ 
  not(_|_) >= _|_ 
  fold(/\x.X(x), /\y.Y(y), Z, nil) >= Z 
  fold(/\x.X(x), /\y.Y(y), Z, 0(U)) > fold(/\x.X(x), /\y.Y(y), X(Z), U) 
  fold(/\x.X(x), /\y.Y(y), Z, 1(U)) > fold(/\x.X(x), /\y.Y(y), Y(Z), U) 
  0(1(X)) >= 1(0(X)) 

With these choices, we have:

  1] not(_|_) >= _|_  by (Bot) 

  2] not(_|_) >= _|_  by (Bot) 

  3] fold(/\x.X(x), /\y.Y(y), Z, nil) >= Z  because [4], by (Star) 
  4] fold*(/\x.X(x), /\y.Y(y), Z, nil) >= Z  because [5], by (Select) 
  5] Z >= Z  by (Meta) 

  6] fold(/\x.X(x), /\y.Y(y), Z, 0(U)) > fold(/\x.X(x), /\y.Y(y), X(Z), U)  because [7], by definition 
  7] fold*(/\x.X(x), /\y.Y(y), Z, 0(U)) >= fold(/\x.X(x), /\y.Y(y), X(Z), U)  because [8], [11], [15], [19] and [23], by (Stat) 
  8] 0(U) > U  because [9], by definition 
  9] 0*(U) >= U  because [10], by (Select) 
  10] U >= U  by (Meta) 
  11] fold*(/\x.X(x), /\y.Y(y), Z, 0(U)) >= /\x.X(x)  because [12], by (Select) 
  12] /\y.X(y) >= /\y.X(y)  because [13], by (Abs) 
  13] X(x) >= X(x)  because [14], by (Meta) 
  14] x >= x  by (Var) 
  15] fold*(/\y.X(y), /\z.Y(z), Z, 0(U)) >= /\y.Y(y)  because [16], by (Select) 
  16] /\z.Y(z) >= /\z.Y(z)  because [17], by (Abs) 
  17] Y(y) >= Y(y)  because [18], by (Meta) 
  18] y >= y  by (Var) 
  19] fold*(/\z.X(z), /\u.Y(u), Z, 0(U)) >= X(Z)  because [20], by (Select) 
  20] X(fold*(/\z.X(z), /\u.Y(u), Z, 0(U))) >= X(Z)  because [21], by (Meta) 
  21] fold*(/\z.X(z), /\u.Y(u), Z, 0(U)) >= Z  because [22], by (Select) 
  22] Z >= Z  by (Meta) 
  23] fold*(/\z.X(z), /\u.Y(u), Z, 0(U)) >= U  because [24], by (Select) 
  24] 0(U) >= U  because [9], by (Star) 

  25] fold(/\x.X(x), /\y.Y(y), Z, 1(U)) > fold(/\x.X(x), /\y.Y(y), Y(Z), U)  because [26], by definition 
  26] fold*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= fold(/\x.X(x), /\y.Y(y), Y(Z), U)  because [27], [30], [35], [39] and [43], by (Stat) 
  27] 1(U) > U  because [28], by definition 
  28] 1*(U) >= U  because [29], by (Select) 
  29] U >= U  by (Meta) 
  30] fold*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= /\x.X(x)  because [31], by (F-Abs) 
  31] fold*(/\x.X(x), /\y.Y(y), Z, 1(U), z) >= X(z)  because [32], by (Select) 
  32] X(fold*(/\x.X(x), /\y.Y(y), Z, 1(U), z)) >= X(z)  because [33], by (Meta) 
  33] fold*(/\x.X(x), /\y.Y(y), Z, 1(U), z) >= z  because [34], by (Select) 
  34] z >= z  by (Var) 
  35] fold*(/\x.X(x), /\y.Y(y), Z, 1(U)) >= /\x.Y(x)  because [36], by (Select) 
  36] /\y.Y(y) >= /\y.Y(y)  because [37], by (Abs) 
  37] Y(x) >= Y(x)  because [38], by (Meta) 
  38] x >= x  by (Var) 
  39] fold*(/\y.X(y), /\u.Y(u), Z, 1(U)) >= Y(Z)  because [40], by (Select) 
  40] Y(fold*(/\y.X(y), /\u.Y(u), Z, 1(U))) >= Y(Z)  because [41], by (Meta) 
  41] fold*(/\y.X(y), /\u.Y(u), Z, 1(U)) >= Z  because [42], by (Select) 
  42] Z >= Z  by (Meta) 
  43] fold*(/\y.X(y), /\u.Y(u), Z, 1(U)) >= U  because [44], by (Select) 
  44] 1(U) >= U  because [28], by (Star) 

  45] 0(1(X)) >= 1(0(X))  because [46], by (Star) 
  46] 0*(1(X)) >= 1(0(X))  because 0 > 1 and [47], by (Copy) 
  47] 0*(1(X)) >= 0(X)  because 0 in Mul and [48], by (Stat) 
  48] 1(X) > X  because [49], by definition 
  49] 1*(X) >= X  because [50], by (Select) 
  50] X >= X  by (Meta) 

We can thus remove the following rules:

  fold(/\x.X(x), /\y.Y(y), Z, 0(U)) => fold(/\z.X(z), /\u.Y(u), X(Z), U) 
  fold(/\x.X(x), /\y.Y(y), Z, 1(U)) => fold(/\z.X(z), /\u.Y(u), Y(Z), U) 

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

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

  not(true) >? false 
  not(false) >? true 
  fold(/\x.X(x), /\y.Y(y), Z, nil) >? Z 
  0(1(X)) >? 1(0(X)) 

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

The following interpretation satisfies the requirements:

  0 = \y0.3y0 
  1 = \y0.3 + y0 
  false = 0 
  fold = \G0G1y2y3.3 + y2 + y3 + G0(0) + G1(0) 
  nil = 3 
  not = \y0.3 + 3y0 
  true = 0 

Using this interpretation, the requirements translate to:

  [[not(true)]] = 3 > 0 = [[false]] 
  [[not(false)]] = 3 > 0 = [[true]] 
  [[fold(/\x._x0(x), /\y._x1(y), _x2, nil)]] = 6 + x2 + F0(0) + F1(0) > x2 = [[_x2]] 
  [[0(1(_x0))]] = 9 + 3x0 > 3 + 3x0 = [[1(0(_x0))]] 

We can thus remove the following rules:

  not(true) => false 
  not(false) => true 
  fold(/\x.X(x), /\y.Y(y), Z, nil) => Z 
  0(1(X)) => 1(0(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.