We consider the system 429.

  Alphabet:

    asort : [natlist] --> natlist 
    cons : [nat * natlist] --> natlist 
    dsort : [natlist] --> natlist 
    insert : [nat * natlist * nat -> nat -> nat * nat -> nat -> nat] --> natlist 
    max : [nat * nat] --> nat 
    min : [nat * nat] --> nat 
    nil : [] --> natlist 
    sort : [natlist * nat -> nat -> nat * nat -> nat -> nat] --> natlist 

  Rules:

    insert(X, nil, /\x./\y.Y(x, y), /\z./\u.Z(z, u)) => cons(X, nil) 
    insert(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) => cons(U(X, Y), insert(V(X, Y), Z, /\v./\w.U(v, w), /\x'./\y'.V(x', y'))) 
    sort(nil, /\x./\y.X(x, y), /\z./\u.Y(z, u)) => nil 
    sort(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) => insert(X, sort(Y, /\v./\w.Z(v, w), /\x'./\y'.U(x', y')), /\z'./\u'.Z(z', u'), /\v'./\w'.U(v', w')) 
    asort(X) => sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u)) 
    dsort(X) => sort(X, /\x./\y.max(x, y), /\z./\u.min(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]):

  insert(X, nil, /\x./\y.Y(x, y), /\z./\u.Z(z, u)) >? cons(X, nil) 
  insert(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >? cons(U(X, Y), insert(V(X, Y), Z, /\v./\w.U(v, w), /\x'./\y'.V(x', y'))) 
  sort(nil, /\x./\y.X(x, y), /\z./\u.Y(z, u)) >? nil 
  sort(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) >? insert(X, sort(Y, /\v./\w.Z(v, w), /\x'./\y'.U(x', y')), /\z'./\u'.Z(z', u'), /\v'./\w'.U(v', w')) 
  asort(X) >? sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u)) 
  dsort(X) >? sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u)) 

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

Argument functions:

  [[insert(x_1, x_2, x_3, x_4)]] = insert(x_2, x_4, x_3, x_1) 
  [[nil]] = _|_ 

We choose Lex = {insert} and Mul = {asort, cons, dsort, max, min, sort}, and the following precedence: dsort > asort > max > sort > min > insert > cons

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

  insert(X, _|_, /\x./\y.Y(x, y), /\z./\u.Z(z, u)) >= cons(X, _|_) 
  insert(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= cons(U(X, Y), insert(V(X, Y), Z, /\x./\y.U(x, y), /\z./\u.V(z, u))) 
  sort(_|_, /\x./\y.X(x, y), /\z./\u.Y(z, u)) > _|_ 
  sort(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) > insert(X, sort(Y, /\x./\y.Z(x, y), /\z./\u.U(z, u)), /\v./\w.Z(v, w), /\x'./\y'.U(x', y')) 
  asort(X) > sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u)) 
  dsort(X) >= sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u)) 

With these choices, we have:

  1] insert(X, _|_, /\x./\y.Y(x, y), /\z./\u.Z(z, u)) >= cons(X, _|_)  because [2], by (Star) 
  2] insert*(X, _|_, /\x./\y.Y(x, y), /\z./\u.Z(z, u)) >= cons(X, _|_)  because insert > cons, [3] and [5], by (Copy) 
  3] insert*(X, _|_, /\x./\y.Y(x, y), /\z./\u.Z(z, u)) >= X  because [4], by (Select) 
  4] X >= X  by (Meta) 
  5] insert*(X, _|_, /\x./\y.Y(x, y), /\z./\u.Z(z, u)) >= _|_  by (Bot) 

  6] insert(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= cons(U(X, Y), insert(V(X, Y), Z, /\x./\y.U(x, y), /\z./\u.V(z, u)))  because [7], by (Star) 
  7] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= cons(U(X, Y), insert(V(X, Y), Z, /\x./\y.U(x, y), /\z./\u.V(z, u)))  because insert > cons, [8] and [16], by (Copy) 
  8] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= U(X, Y)  because [9], by (Select) 
  9] U(insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)), insert*(X, cons(Y, Z), /\v./\w.U(v, w), /\x'./\y'.V(x', y'))) >= U(X, Y)  because [10] and [12], by (Meta) 
  10] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= X  because [11], by (Select) 
  11] X >= X  by (Meta) 
  12] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= Y  because [13], by (Select) 
  13] cons(Y, Z) >= Y  because [14], by (Star) 
  14] cons*(Y, Z) >= Y  because [15], by (Select) 
  15] Y >= Y  by (Meta) 
  16] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= insert(V(X, Y), Z, /\x./\y.U(x, y), /\z./\u.V(z, u))  because [17], [20], [22], [24] and [31], by (Stat) 
  17] cons(Y, Z) > Z  because [18], by definition 
  18] cons*(Y, Z) >= Z  because [19], by (Select) 
  19] Z >= Z  by (Meta) 
  20] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= V(X, Y)  because [21], by (Select) 
  21] V(insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)), insert*(X, cons(Y, Z), /\v./\w.U(v, w), /\x'./\y'.V(x', y'))) >= V(X, Y)  because [10] and [12], by (Meta) 
  22] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= Z  because [23], by (Select) 
  23] cons(Y, Z) >= Z  because [18], by (Star) 
  24] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= /\x./\y.U(x, y)  because [25], by (F-Abs) 
  25] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u), v) >= /\x.U(v, x)  because [26], by (Select) 
  26] /\x.U(insert*(X, cons(Y, Z), /\y./\z.U(y, z), /\u./\x'.V(u, x'), v), x) >= /\x.U(v, x)  because [27], by (Abs) 
  27] U(insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u), v), w) >= U(v, w)  because [28] and [30], by (Meta) 
  28] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u), v) >= v  because [29], by (Select) 
  29] v >= v  by (Var) 
  30] w >= w  by (Var) 
  31] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= /\x./\y.V(x, y)  because [32], by (F-Abs) 
  32] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u), x') >= /\x.V(x', x)  because [33], by (Select) 
  33] /\x.V(insert*(X, cons(Y, Z), /\y./\z.U(y, z), /\u./\z'.V(u, z'), x'), x) >= /\x.V(x', x)  because [34], by (Abs) 
  34] V(insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u), x'), y') >= V(x', y')  because [35] and [37], by (Meta) 
  35] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u), x') >= x'  because [36], by (Select) 
  36] x' >= x'  by (Var) 
  37] y' >= y'  by (Var) 

  38] sort(_|_, /\x./\y.X(x, y), /\z./\u.Y(z, u)) > _|_  because [39], by definition 
  39] sort*(_|_, /\x./\y.X(x, y), /\z./\u.Y(z, u)) >= _|_  by (Bot) 

  40] sort(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) > insert(X, sort(Y, /\x./\y.Z(x, y), /\z./\u.U(z, u)), /\v./\w.Z(v, w), /\x'./\y'.U(x', y'))  because [41], by definition 
  41] sort*(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) >= insert(X, sort(Y, /\x./\y.Z(x, y), /\z./\u.U(z, u)), /\v./\w.Z(v, w), /\x'./\y'.U(x', y'))  because sort > insert, [42], [46], [60] and [61], by (Copy) 
  42] sort*(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) >= X  because [43], by (Select) 
  43] cons(X, Y) >= X  because [44], by (Star) 
  44] cons*(X, Y) >= X  because [45], by (Select) 
  45] X >= X  by (Meta) 
  46] sort*(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) >= sort(Y, /\x./\y.Z(x, y), /\z./\u.U(z, u))  because sort in Mul, [47], [50] and [55], by (Stat) 
  47] cons(X, Y) > Y  because [48], by definition 
  48] cons*(X, Y) >= Y  because [49], by (Select) 
  49] Y >= Y  by (Meta) 
  50] /\x./\z.Z(x, z) >= /\x./\z.Z(x, z)  because [51], by (Abs) 
  51] /\z.Z(y, z) >= /\z.Z(y, z)  because [52], by (Abs) 
  52] Z(y, x) >= Z(y, x)  because [53] and [54], by (Meta) 
  53] y >= y  by (Var) 
  54] x >= x  by (Var) 
  55] /\z./\v.U(z, v) >= /\z./\v.U(z, v)  because [56], by (Abs) 
  56] /\v.U(u, v) >= /\v.U(u, v)  because [57], by (Abs) 
  57] U(u, z) >= U(u, z)  because [58] and [59], by (Meta) 
  58] u >= u  by (Var) 
  59] z >= z  by (Var) 
  60] sort*(cons(X, Y), /\v./\w.Z(v, w), /\x'./\y'.U(x', y')) >= /\v./\w.Z(v, w)  because [50], by (Select) 
  61] sort*(cons(X, Y), /\v./\w.Z(v, w), /\x'./\y'.U(x', y')) >= /\v./\w.U(v, w)  because [55], by (Select) 

  62] asort(X) > sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u))  because [63], by definition 
  63] asort*(X) >= sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u))  because asort > sort, [64], [66] and [73], by (Copy) 
  64] asort*(X) >= X  because [65], by (Select) 
  65] X >= X  by (Meta) 
  66] asort*(X) >= /\y./\z.min(y, z)  because [67], by (F-Abs) 
  67] asort*(X, x) >= /\z.min(x, z)  because [68], by (F-Abs) 
  68] asort*(X, x, y) >= min(x, y)  because asort > min, [69] and [71], by (Copy) 
  69] asort*(X, x, y) >= x  because [70], by (Select) 
  70] x >= x  by (Var) 
  71] asort*(X, x, y) >= y  because [72], by (Select) 
  72] y >= y  by (Var) 
  73] asort*(X) >= /\u./\v.max(u, v)  because [74], by (F-Abs) 
  74] asort*(X, z) >= /\v.max(z, v)  because [75], by (F-Abs) 
  75] asort*(X, z, u) >= max(z, u)  because asort > max, [76] and [78], by (Copy) 
  76] asort*(X, z, u) >= z  because [77], by (Select) 
  77] z >= z  by (Var) 
  78] asort*(X, z, u) >= u  because [79], by (Select) 
  79] u >= u  by (Var) 

  80] dsort(X) >= sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u))  because [81], by (Star) 
  81] dsort*(X) >= sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u))  because dsort > sort, [82], [84] and [91], by (Copy) 
  82] dsort*(X) >= X  because [83], by (Select) 
  83] X >= X  by (Meta) 
  84] dsort*(X) >= /\y./\z.max(y, z)  because [85], by (F-Abs) 
  85] dsort*(X, x) >= /\z.max(x, z)  because [86], by (F-Abs) 
  86] dsort*(X, x, y) >= max(x, y)  because dsort > max, [87] and [89], by (Copy) 
  87] dsort*(X, x, y) >= x  because [88], by (Select) 
  88] x >= x  by (Var) 
  89] dsort*(X, x, y) >= y  because [90], by (Select) 
  90] y >= y  by (Var) 
  91] dsort*(X) >= /\u./\v.min(u, v)  because [92], by (F-Abs) 
  92] dsort*(X, z) >= /\v.min(z, v)  because [93], by (F-Abs) 
  93] dsort*(X, z, u) >= min(z, u)  because dsort > min, [94] and [96], by (Copy) 
  94] dsort*(X, z, u) >= z  because [95], by (Select) 
  95] z >= z  by (Var) 
  96] dsort*(X, z, u) >= u  because [97], by (Select) 
  97] u >= u  by (Var) 

We can thus remove the following rules:

  sort(nil, /\x./\y.X(x, y), /\z./\u.Y(z, u)) => nil 
  sort(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) => insert(X, sort(Y, /\v./\w.Z(v, w), /\x'./\y'.U(x', y')), /\z'./\u'.Z(z', u'), /\v'./\w'.U(v', w')) 
  asort(X) => sort(X, /\x./\y.min(x, y), /\z./\u.max(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]):

  insert(X, nil, /\x./\y.Y(x, y), /\z./\u.Z(z, u)) >? cons(X, nil) 
  insert(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >? cons(U(X, Y), insert(V(X, Y), Z, /\v./\w.U(v, w), /\x'./\y'.V(x', y'))) 
  dsort(X) >? sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u)) 

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

Argument functions:

  [[insert(x_1, x_2, x_3, x_4)]] = insert(x_2, x_3, x_1, x_4) 
  [[nil]] = _|_ 

We choose Lex = {insert} and Mul = {cons, dsort, max, min, sort}, and the following precedence: insert > cons > dsort > min > sort > max

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

  insert(X, _|_, /\x./\y.Y(x, y), /\z./\u.Z(z, u)) > cons(X, _|_) 
  insert(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= cons(U(X, Y), insert(V(X, Y), Z, /\x./\y.U(x, y), /\z./\u.V(z, u))) 
  dsort(X) >= sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u)) 

With these choices, we have:

  1] insert(X, _|_, /\x./\y.Y(x, y), /\z./\u.Z(z, u)) > cons(X, _|_)  because [2], by definition 
  2] insert*(X, _|_, /\x./\y.Y(x, y), /\z./\u.Z(z, u)) >= cons(X, _|_)  because insert > cons, [3] and [5], by (Copy) 
  3] insert*(X, _|_, /\x./\y.Y(x, y), /\z./\u.Z(z, u)) >= X  because [4], by (Select) 
  4] X >= X  by (Meta) 
  5] insert*(X, _|_, /\x./\y.Y(x, y), /\z./\u.Z(z, u)) >= _|_  by (Bot) 

  6] insert(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= cons(U(X, Y), insert(V(X, Y), Z, /\x./\y.U(x, y), /\z./\u.V(z, u)))  because [7], by (Star) 
  7] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= cons(U(X, Y), insert(V(X, Y), Z, /\x./\y.U(x, y), /\z./\u.V(z, u)))  because insert > cons, [8] and [16], by (Copy) 
  8] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= U(X, Y)  because [9], by (Select) 
  9] U(insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)), insert*(X, cons(Y, Z), /\v./\w.U(v, w), /\x'./\y'.V(x', y'))) >= U(X, Y)  because [10] and [12], by (Meta) 
  10] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= X  because [11], by (Select) 
  11] X >= X  by (Meta) 
  12] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= Y  because [13], by (Select) 
  13] cons(Y, Z) >= Y  because [14], by (Star) 
  14] cons*(Y, Z) >= Y  because [15], by (Select) 
  15] Y >= Y  by (Meta) 
  16] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= insert(V(X, Y), Z, /\x./\y.U(x, y), /\z./\u.V(z, u))  because [17], [20], [22], [24] and [30], by (Stat) 
  17] cons(Y, Z) > Z  because [18], by definition 
  18] cons*(Y, Z) >= Z  because [19], by (Select) 
  19] Z >= Z  by (Meta) 
  20] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= V(X, Y)  because [21], by (Select) 
  21] V(insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)), insert*(X, cons(Y, Z), /\v./\w.U(v, w), /\x'./\y'.V(x', y'))) >= V(X, Y)  because [10] and [12], by (Meta) 
  22] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= Z  because [23], by (Select) 
  23] cons(Y, Z) >= Z  because [18], by (Star) 
  24] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= /\x./\y.U(x, y)  because [25], by (Select) 
  25] /\x./\z.U(x, z) >= /\x./\z.U(x, z)  because [26], by (Abs) 
  26] /\z.U(y, z) >= /\z.U(y, z)  because [27], by (Abs) 
  27] U(y, x) >= U(y, x)  because [28] and [29], by (Meta) 
  28] y >= y  by (Var) 
  29] x >= x  by (Var) 
  30] insert*(X, cons(Y, Z), /\z./\u.U(z, u), /\v./\w.V(v, w)) >= /\z./\u.V(z, u)  because [31], by (Select) 
  31] /\z./\v.V(z, v) >= /\z./\v.V(z, v)  because [32], by (Abs) 
  32] /\v.V(u, v) >= /\v.V(u, v)  because [33], by (Abs) 
  33] V(u, z) >= V(u, z)  because [34] and [35], by (Meta) 
  34] u >= u  by (Var) 
  35] z >= z  by (Var) 

  36] dsort(X) >= sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u))  because [37], by (Star) 
  37] dsort*(X) >= sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u))  because dsort > sort, [38], [40] and [47], by (Copy) 
  38] dsort*(X) >= X  because [39], by (Select) 
  39] X >= X  by (Meta) 
  40] dsort*(X) >= /\y./\z.max(y, z)  because [41], by (F-Abs) 
  41] dsort*(X, x) >= /\z.max(x, z)  because [42], by (F-Abs) 
  42] dsort*(X, x, y) >= max(x, y)  because dsort > max, [43] and [45], by (Copy) 
  43] dsort*(X, x, y) >= x  because [44], by (Select) 
  44] x >= x  by (Var) 
  45] dsort*(X, x, y) >= y  because [46], by (Select) 
  46] y >= y  by (Var) 
  47] dsort*(X) >= /\u./\v.min(u, v)  because [48], by (F-Abs) 
  48] dsort*(X, z) >= /\v.min(z, v)  because [49], by (F-Abs) 
  49] dsort*(X, z, u) >= min(z, u)  because dsort > min, [50] and [52], by (Copy) 
  50] dsort*(X, z, u) >= z  because [51], by (Select) 
  51] z >= z  by (Var) 
  52] dsort*(X, z, u) >= u  because [53], by (Select) 
  53] u >= u  by (Var) 

We can thus remove the following rules:

  insert(X, nil, /\x./\y.Y(x, y), /\z./\u.Z(z, u)) => cons(X, 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]):

  insert(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >? cons(U(X, Y), insert(V(X, Y), Z, /\v./\w.U(v, w), /\x'./\y'.V(x', y'))) 
  dsort(X) >? sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u)) 

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

Argument functions:

  [[insert(x_1, x_2, x_3, x_4)]] = insert(x_2, x_3, x_4, x_1) 

We choose Lex = {insert} and Mul = {cons, dsort, max, min, sort}, and the following precedence: dsort > max > min > insert > sort > cons

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

  insert(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= cons(U(X, Y), insert(V(X, Y), Z, /\x./\y.U(x, y), /\z./\u.V(z, u))) 
  dsort(X) > sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u)) 

With these choices, we have:

  1] insert(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= cons(U(X, Y), insert(V(X, Y), Z, /\x./\y.U(x, y), /\z./\u.V(z, u)))  because [2], by (Star) 
  2] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= cons(U(X, Y), insert(V(X, Y), Z, /\x./\y.U(x, y), /\z./\u.V(z, u)))  because insert > cons, [3] and [11], by (Copy) 
  3] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= U(X, Y)  because [4], by (Select) 
  4] U(insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)), insert*(X, cons(Y, Z), /\v./\w.U(v, w), /\x'./\y'.V(x', y'))) >= U(X, Y)  because [5] and [7], by (Meta) 
  5] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= X  because [6], by (Select) 
  6] X >= X  by (Meta) 
  7] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= Y  because [8], by (Select) 
  8] cons(Y, Z) >= Y  because [9], by (Star) 
  9] cons*(Y, Z) >= Y  because [10], by (Select) 
  10] Y >= Y  by (Meta) 
  11] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= insert(V(X, Y), Z, /\x./\y.U(x, y), /\z./\u.V(z, u))  because [12], [15], [17], [19] and [25], by (Stat) 
  12] cons(Y, Z) > Z  because [13], by definition 
  13] cons*(Y, Z) >= Z  because [14], by (Select) 
  14] Z >= Z  by (Meta) 
  15] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= V(X, Y)  because [16], by (Select) 
  16] V(insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)), insert*(X, cons(Y, Z), /\v./\w.U(v, w), /\x'./\y'.V(x', y'))) >= V(X, Y)  because [5] and [7], by (Meta) 
  17] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= Z  because [18], by (Select) 
  18] cons(Y, Z) >= Z  because [13], by (Star) 
  19] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= /\x./\y.U(x, y)  because [20], by (Select) 
  20] /\x./\z.U(x, z) >= /\x./\z.U(x, z)  because [21], by (Abs) 
  21] /\z.U(y, z) >= /\z.U(y, z)  because [22], by (Abs) 
  22] U(y, x) >= U(y, x)  because [23] and [24], by (Meta) 
  23] y >= y  by (Var) 
  24] x >= x  by (Var) 
  25] insert*(X, cons(Y, Z), /\z./\u.U(z, u), /\v./\w.V(v, w)) >= /\z./\u.V(z, u)  because [26], by (Select) 
  26] /\z./\v.V(z, v) >= /\z./\v.V(z, v)  because [27], by (Abs) 
  27] /\v.V(u, v) >= /\v.V(u, v)  because [28], by (Abs) 
  28] V(u, z) >= V(u, z)  because [29] and [30], by (Meta) 
  29] u >= u  by (Var) 
  30] z >= z  by (Var) 

  31] dsort(X) > sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u))  because [32], by definition 
  32] dsort*(X) >= sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u))  because dsort > sort, [33], [35] and [42], by (Copy) 
  33] dsort*(X) >= X  because [34], by (Select) 
  34] X >= X  by (Meta) 
  35] dsort*(X) >= /\y./\z.max(y, z)  because [36], by (F-Abs) 
  36] dsort*(X, x) >= /\z.max(x, z)  because [37], by (F-Abs) 
  37] dsort*(X, x, y) >= max(x, y)  because dsort > max, [38] and [40], by (Copy) 
  38] dsort*(X, x, y) >= x  because [39], by (Select) 
  39] x >= x  by (Var) 
  40] dsort*(X, x, y) >= y  because [41], by (Select) 
  41] y >= y  by (Var) 
  42] dsort*(X) >= /\u./\v.min(u, v)  because [43], by (F-Abs) 
  43] dsort*(X, z) >= /\v.min(z, v)  because [44], by (F-Abs) 
  44] dsort*(X, z, u) >= min(z, u)  because dsort > min, [45] and [47], by (Copy) 
  45] dsort*(X, z, u) >= z  because [46], by (Select) 
  46] z >= z  by (Var) 
  47] dsort*(X, z, u) >= u  because [48], by (Select) 
  48] u >= u  by (Var) 

We can thus remove the following rules:

  dsort(X) => sort(X, /\x./\y.max(x, y), /\z./\u.min(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]):

  insert(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >? cons(U(X, Y), insert(V(X, Y), Z, /\v./\w.U(v, w), /\x'./\y'.V(x', y'))) 

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

Argument functions:

  [[insert(x_1, x_2, x_3, x_4)]] = insert(x_2, x_3, x_1, x_4) 

We choose Lex = {insert} and Mul = {cons}, and the following precedence: insert > cons

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

  insert(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) > cons(U(X, Y), insert(V(X, Y), Z, /\x./\y.U(x, y), /\z./\u.V(z, u))) 

With these choices, we have:

  1] insert(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) > cons(U(X, Y), insert(V(X, Y), Z, /\x./\y.U(x, y), /\z./\u.V(z, u)))  because [2], by definition 
  2] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= cons(U(X, Y), insert(V(X, Y), Z, /\x./\y.U(x, y), /\z./\u.V(z, u)))  because insert > cons, [3] and [11], by (Copy) 
  3] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= U(X, Y)  because [4], by (Select) 
  4] U(insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)), insert*(X, cons(Y, Z), /\v./\w.U(v, w), /\x'./\y'.V(x', y'))) >= U(X, Y)  because [5] and [7], by (Meta) 
  5] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= X  because [6], by (Select) 
  6] X >= X  by (Meta) 
  7] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= Y  because [8], by (Select) 
  8] cons(Y, Z) >= Y  because [9], by (Star) 
  9] cons*(Y, Z) >= Y  because [10], by (Select) 
  10] Y >= Y  by (Meta) 
  11] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= insert(V(X, Y), Z, /\x./\y.U(x, y), /\z./\u.V(z, u))  because [12], [15], [17], [19] and [25], by (Stat) 
  12] cons(Y, Z) > Z  because [13], by definition 
  13] cons*(Y, Z) >= Z  because [14], by (Select) 
  14] Z >= Z  by (Meta) 
  15] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= V(X, Y)  because [16], by (Select) 
  16] V(insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)), insert*(X, cons(Y, Z), /\v./\w.U(v, w), /\x'./\y'.V(x', y'))) >= V(X, Y)  because [5] and [7], by (Meta) 
  17] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= Z  because [18], by (Select) 
  18] cons(Y, Z) >= Z  because [13], by (Star) 
  19] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= /\x./\y.U(x, y)  because [20], by (Select) 
  20] /\x./\z.U(x, z) >= /\x./\z.U(x, z)  because [21], by (Abs) 
  21] /\z.U(y, z) >= /\z.U(y, z)  because [22], by (Abs) 
  22] U(y, x) >= U(y, x)  because [23] and [24], by (Meta) 
  23] y >= y  by (Var) 
  24] x >= x  by (Var) 
  25] insert*(X, cons(Y, Z), /\z./\u.U(z, u), /\v./\w.V(v, w)) >= /\z./\u.V(z, u)  because [26], by (Select) 
  26] /\z./\v.V(z, v) >= /\z./\v.V(z, v)  because [27], by (Abs) 
  27] /\v.V(u, v) >= /\v.V(u, v)  because [28], by (Abs) 
  28] V(u, z) >= V(u, z)  because [29] and [30], by (Meta) 
  29] u >= u  by (Var) 
  30] z >= z  by (Var) 

We can thus remove the following rules:

  insert(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) => cons(U(X, Y), insert(V(X, Y), Z, /\v./\w.U(v, w), /\x'./\y'.V(x', 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.