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 the dependency pair framework as described in [Kop12, Ch. 6/7], with dynamic dependency pairs.

We thus obtain the following dependency pair problem (P_0, R_0, minimal, formative):

  Dependency Pairs P_0:

    0] insert#(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) =#> U(X, Y)   
    1] insert#(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) =#> insert#(V(X, Y), Z, /\v./\w.U(v, w), /\x'./\y'.V(x', y'))   
    2] insert#(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) =#> V(X, Y)   
    3] insert#(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) =#> U(v, w)   
    4] insert#(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) =#> V(v, w)   
    5] 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'))   
    6] sort#(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) =#> sort#(Y, /\v./\w.Z(v, w), /\x'./\y'.U(x', y'))   
    7] sort#(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) =#> Z(v, w)   
    8] sort#(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) =#> U(v, w)   
    9] sort#(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) =#> Z(v, w)   
    10] sort#(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) =#> U(v, w)   
    11] asort#(X) =#> sort#(X, /\x./\y.min(x, y), /\z./\u.max(z, u))   
    12] dsort#(X) =#> sort#(X, /\x./\y.max(x, y), /\z./\u.min(z, u))   

  Rules R_0:

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

Thus, the original system is terminating if (P_0, R_0, minimal, formative) is finite.

We consider the dependency pair problem (P_0, R_0, minimal, formative).

We will use the reduction pair processor [Kop12, Thm. 7.16].  As the system is abstraction-simple and the formative flag is set, it suffices to find a tagged reduction pair [Kop12, Def. 6.70].  Thus, we must orient:

  insert#(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >? U(X, Y) 
  insert#(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >? insert#(V(X, Y), Z, /\v./\w.U(v, w), /\x'./\y'.V(x', y')) 
  insert#(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >? V(X, Y) 
  insert#(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >? U(~c0, ~c1) 
  insert#(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >? V(~c2, ~c3) 
  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')) 
  sort#(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) >? sort#(Y, /\v./\w.Z(v, w), /\x'./\y'.U(x', y')) 
  sort#(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) >? Z(~c4, ~c5) 
  sort#(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) >? U(~c6, ~c7) 
  sort#(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) >? Z(~c8, ~c9) 
  sort#(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) >? U(~c10, ~c11) 
  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)) 
  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)) 
  max-(X, Y) >= max(X, Y) 
  min-(X, Y) >= min(X, Y) 

We apply [Kop12, Thm. 6.75] and use the following argument functions:

  pi( asort(X) ) = #argfun-asort#(sort(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u))) 
  pi( asort#(X) ) = #argfun-asort##(sort#(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u))) 
  pi( dsort(X) ) = #argfun-dsort#(sort(X, /\x./\y.max-(x, y), /\z./\u.min-(z, u))) 
  pi( dsort#(X) ) = #argfun-dsort##(sort#(X, /\x./\y.max-(x, y), /\z./\u.min-(z, u))) 

Since this representation is not advantageous for the higher-order recursive path ordering, we present the strict requirements in their unextended form, which is not problematic since for any F, s and substituion gamma: (F s)gamma beta-reduces to F(s)gamma.)

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

Argument functions:

  [[#argfun-dsort##(x_1)]] = x_1 
  [[asort(x_1)]] = x_1 
  [[asort#(x_1)]] = x_1 
  [[dsort(x_1)]] = x_1 
  [[dsort#(x_1)]] = x_1 
  [[insert(x_1, x_2, x_3, x_4)]] = insert(x_3, x_2, x_4, x_1) 
  [[insert#(x_1, x_2, x_3, x_4)]] = insert#(x_3, x_2, x_4, x_1) 
  [[max(x_1, x_2)]] = x_2 
  [[min(x_1, x_2)]] = _|_ 
  [[nil]] = _|_ 
  [[~c0]] = _|_ 
  [[~c1]] = _|_ 
  [[~c10]] = _|_ 
  [[~c11]] = _|_ 
  [[~c2]] = _|_ 
  [[~c3]] = _|_ 
  [[~c4]] = _|_ 
  [[~c5]] = _|_ 
  [[~c6]] = _|_ 
  [[~c7]] = _|_ 
  [[~c8]] = _|_ 
  [[~c9]] = _|_ 

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

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

With these choices, we have:

  1] insert#(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) > U(X, Y)  because [2], by definition 
  2] insert#*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= U(X, Y)  because [3], by (Select) 
  3] 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 [4] and [6], by (Meta) 
  4] insert#*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= X  because [5], by (Select) 
  5] X >= X  by (Meta) 
  6] insert#*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= Y  because [7], by (Select) 
  7] cons(Y, Z) >= Y  because [8], by (Star) 
  8] cons*(Y, Z) >= Y  because [9], by (Select) 
  9] Y >= Y  by (Meta) 

  10] 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 [11], by (Star) 
  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], [20], [22], [24] 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] /\x./\z.U(x, z) >= /\x./\z.U(x, z)  because [16], by (Abs) 
  16] /\z.U(y, z) >= /\z.U(y, z)  because [17], by (Abs) 
  17] U(y, x) >= U(y, x)  because [18] and [19], by (Meta) 
  18] y >= y  by (Var) 
  19] x >= x  by (Var) 
  20] insert#*(X, cons(Y, Z), /\z./\u.U(z, u), /\v./\w.V(v, w)) >= V(X, Y)  because [21], by (Select) 
  21] V(insert#*(X, cons(Y, Z), /\z./\u.U(z, u), /\v./\w.V(v, w)), insert#*(X, cons(Y, Z), /\x'./\y'.U(x', y'), /\z'./\u'.V(z', u'))) >= V(X, Y)  because [4] and [6], by (Meta) 
  22] insert#*(X, cons(Y, Z), /\z./\u.U(z, u), /\v./\w.V(v, w)) >= Z  because [23], by (Select) 
  23] cons(Y, Z) >= Z  because [13], by (Star) 
  24] insert#*(X, cons(Y, Z), /\z./\u.U(z, u), /\v./\w.V(v, w)) >= /\z./\u.U(z, u)  because [15], by (Select) 
  25] insert#*(X, cons(Y, Z), /\z./\u.U(z, u), /\v./\w.V(v, w)) >= /\z./\u.V(z, u)  because [26], by (F-Abs) 
  26] insert#*(X, cons(Y, Z), /\z./\u.U(z, u), /\v./\w.V(v, w), x') >= /\z.V(x', z)  because [27], by (F-Abs) 
  27] insert#*(X, cons(Y, Z), /\z./\u.U(z, u), /\v./\w.V(v, w), x', y') >= V(x', y')  because [28], by (Select) 
  28] V(insert#*(X, cons(Y, Z), /\z./\u.U(z, u), /\v./\w.V(v, w), x', y'), insert#*(X, cons(Y, Z), /\z'./\u'.U(z', u'), /\v'./\w'.V(v', w'), x', y')) >= V(x', y')  because [29] and [31], by (Meta) 
  29] insert#*(X, cons(Y, Z), /\z./\u.U(z, u), /\v./\w.V(v, w), x', y') >= x'  because [30], by (Select) 
  30] x' >= x'  by (Var) 
  31] insert#*(X, cons(Y, Z), /\z./\u.U(z, u), /\v./\w.V(v, w), x', y') >= y'  because [32], by (Select) 
  32] y' >= y'  by (Var) 

  33] insert#(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) > V(X, Y)  because [34], by definition 
  34] insert#*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= V(X, Y)  because [35], by (Select) 
  35] 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 [4] and [6], by (Meta) 

  36] insert#(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) > U(_|_, _|_)  because [37], by definition 
  37] insert#*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= U(_|_, _|_)  because [38], by (Select) 
  38] 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(_|_, _|_)  because [39] and [40], by (Meta) 
  39] insert#*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= _|_  by (Bot) 
  40] insert#*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= _|_  by (Bot) 

  41] insert#(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) > V(_|_, _|_)  because [42], by definition 
  42] insert#*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= V(_|_, _|_)  because [43], by (Select) 
  43] 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(_|_, _|_)  because [44] and [45], by (Meta) 
  44] insert#*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= _|_  by (Bot) 
  45] insert#*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= _|_  by (Bot) 

  46] 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 [47], by (Star) 
  47] 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#, [48], [52], [57] and [63], by (Copy) 
  48] sort#*(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) >= X  because [49], by (Select) 
  49] cons(X, Y) >= X  because [50], by (Star) 
  50] cons*(X, Y) >= X  because [51], by (Select) 
  51] X >= X  by (Meta) 
  52] 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# > sort, [53], [57] and [63], by (Copy) 
  53] sort#*(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) >= Y  because [54], by (Select) 
  54] cons(X, Y) >= Y  because [55], by (Star) 
  55] cons*(X, Y) >= Y  because [56], by (Select) 
  56] Y >= Y  by (Meta) 
  57] sort#*(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) >= /\x./\y.Z(x, y)  because [58], by (Select) 
  58] /\x./\z.Z(x, z) >= /\x./\z.Z(x, z)  because [59], by (Abs) 
  59] /\z.Z(y, z) >= /\z.Z(y, z)  because [60], by (Abs) 
  60] Z(y, x) >= Z(y, x)  because [61] and [62], by (Meta) 
  61] y >= y  by (Var) 
  62] x >= x  by (Var) 
  63] sort#*(cons(X, Y), /\z./\u.Z(z, u), /\v./\w.U(v, w)) >= /\z./\u.U(z, u)  because [64], by (Select) 
  64] /\z./\v.U(z, v) >= /\z./\v.U(z, v)  because [65], by (Abs) 
  65] /\v.U(u, v) >= /\v.U(u, v)  because [66], by (Abs) 
  66] U(u, z) >= U(u, z)  because [67] and [68], by (Meta) 
  67] u >= u  by (Var) 
  68] z >= z  by (Var) 

  69] 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 [70], by (Star) 
  70] 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, [71], [73] and [74], by (Stat) 
  71] cons(X, Y) > Y  because [72], by definition 
  72] cons*(X, Y) >= Y  because [56], by (Select) 
  73] /\x./\z.Z(x, z) >= /\x./\z.Z(x, z)  because [59], by (Abs) 
  74] /\x./\u.U(x, u) >= /\x./\u.U(x, u)  because [65], by (Abs) 

  75] sort#(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) > Z(_|_, _|_)  because [76], by definition 
  76] sort#*(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) >= Z(_|_, _|_)  because [77], by (Select) 
  77] Z(sort#*(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)), sort#*(cons(X, Y), /\v./\w.Z(v, w), /\x'./\y'.U(x', y'))) >= Z(_|_, _|_)  because [78] and [79], by (Meta) 
  78] sort#*(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) >= _|_  by (Bot) 
  79] sort#*(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) >= _|_  by (Bot) 

  80] sort#(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) > U(_|_, _|_)  because [81], by definition 
  81] sort#*(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) >= U(_|_, _|_)  because [82], by (Select) 
  82] U(sort#*(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)), sort#*(cons(X, Y), /\v./\w.Z(v, w), /\x'./\y'.U(x', y'))) >= U(_|_, _|_)  because [83] and [84], by (Meta) 
  83] sort#*(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) >= _|_  by (Bot) 
  84] sort#*(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) >= _|_  by (Bot) 

  85] sort#(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) > Z(_|_, _|_)  because [86], by definition 
  86] sort#*(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) >= Z(_|_, _|_)  because [87], by (Select) 
  87] Z(sort#*(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)), sort#*(cons(X, Y), /\v./\w.Z(v, w), /\x'./\y'.U(x', y'))) >= Z(_|_, _|_)  because [88] and [89], by (Meta) 
  88] sort#*(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) >= _|_  by (Bot) 
  89] sort#*(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) >= _|_  by (Bot) 

  90] sort#(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) > U(_|_, _|_)  because [91], by definition 
  91] sort#*(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) >= U(_|_, _|_)  because [92], by (Select) 
  92] U(sort#*(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)), sort#*(cons(X, Y), /\v./\w.Z(v, w), /\x'./\y'.U(x', y'))) >= U(_|_, _|_)  because [93] and [94], by (Meta) 
  93] sort#*(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) >= _|_  by (Bot) 
  94] sort#*(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) >= _|_  by (Bot) 

  95] #argfun-asort##(sort#(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u))) >= sort#(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u))  because [96], by (Star) 
  96] #argfun-asort##*(sort#(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u))) >= sort#(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u))  because #argfun-asort## > sort#, [97], [101] and [108], by (Copy) 
  97] #argfun-asort##*(sort#(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u))) >= X  because [98], by (Select) 
  98] sort#(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u)) >= X  because [99], by (Star) 
  99] sort#*(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u)) >= X  because [100], by (Select) 
  100] X >= X  by (Meta) 
  101] #argfun-asort##*(sort#(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u))) >= /\x./\y.min-(x, y)  because [102], by (F-Abs) 
  102] #argfun-asort##*(sort#(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u)), v) >= /\x.min-(v, x)  because [103], by (F-Abs) 
  103] #argfun-asort##*(sort#(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u)), v, w) >= min-(v, w)  because #argfun-asort## > min-, [104] and [106], by (Copy) 
  104] #argfun-asort##*(sort#(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u)), v, w) >= v  because [105], by (Select) 
  105] v >= v  by (Var) 
  106] #argfun-asort##*(sort#(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u)), v, w) >= w  because [107], by (Select) 
  107] w >= w  by (Var) 
  108] #argfun-asort##*(sort#(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u))) >= /\x./\y.max-(x, y)  because [109], by (F-Abs) 
  109] #argfun-asort##*(sort#(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u)), x') >= /\x.max-(x', x)  because [110], by (F-Abs) 
  110] #argfun-asort##*(sort#(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u)), x', y') >= max-(x', y')  because #argfun-asort## > max-, [111] and [113], by (Copy) 
  111] #argfun-asort##*(sort#(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u)), x', y') >= x'  because [112], by (Select) 
  112] x' >= x'  by (Var) 
  113] #argfun-asort##*(sort#(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u)), x', y') >= y'  because [114], by (Select) 
  114] y' >= y'  by (Var) 

  115] sort#(X, /\x./\y.max-(x, y), /\z./\u.min-(z, u)) >= sort#(X, /\x./\y.max-(x, y), /\z./\u.min-(z, u))  because sort# in Mul, [116], [117] and [122], by (Fun) 
  116] X >= X  by (Meta) 
  117] /\x./\z.max-(x, z) >= /\x./\z.max-(x, z)  because [118], by (Abs) 
  118] /\z.max-(y, z) >= /\z.max-(y, z)  because [119], by (Abs) 
  119] max-(y, x) >= max-(y, x)  because max- in Mul, [120] and [121], by (Fun) 
  120] y >= y  by (Var) 
  121] x >= x  by (Var) 
  122] /\z./\v.min-(z, v) >= /\z./\v.min-(z, v)  because [123], by (Abs) 
  123] /\v.min-(u, v) >= /\v.min-(u, v)  because [124], by (Abs) 
  124] min-(u, z) >= min-(u, z)  because min- in Mul, [125] and [126], by (Fun) 
  125] u >= u  by (Var) 
  126] z >= z  by (Var) 

  127] insert(X, _|_, /\x./\y.Y(x, y), /\z./\u.Z(z, u)) >= cons(X, _|_)  because [128], by (Star) 
  128] insert*(X, _|_, /\x./\y.Y(x, y), /\z./\u.Z(z, u)) >= cons(X, _|_)  because insert > cons, [129] and [131], by (Copy) 
  129] insert*(X, _|_, /\x./\y.Y(x, y), /\z./\u.Z(z, u)) >= X  because [130], by (Select) 
  130] X >= X  by (Meta) 
  131] insert*(X, _|_, /\x./\y.Y(x, y), /\z./\u.Z(z, u)) >= _|_  by (Bot) 

  132] 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 [133], by (Star) 
  133] 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, [134] and [138], by (Copy) 
  134] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= U(X, Y)  because [135], by (Select) 
  135] 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 [136] and [137], by (Meta) 
  136] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= X  because [5], by (Select) 
  137] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= Y  because [7], by (Select) 
  138] 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], [139], [141], [142] and [149], by (Stat) 
  139] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= V(X, Y)  because [140], by (Select) 
  140] 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 [136] and [137], by (Meta) 
  141] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= Z  because [23], by (Select) 
  142] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= /\x./\y.U(x, y)  because [143], by (F-Abs) 
  143] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u), v) >= /\x.U(v, x)  because [144], by (Select) 
  144] /\x.U(insert*(X, cons(Y, Z), /\y./\z.U(y, z), /\u./\x'.V(u, x'), v), x) >= /\x.U(v, x)  because [145], by (Abs) 
  145] U(insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u), v), w) >= U(v, w)  because [146] and [148], by (Meta) 
  146] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u), v) >= v  because [147], by (Select) 
  147] v >= v  by (Var) 
  148] w >= w  by (Var) 
  149] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u)) >= /\x./\y.V(x, y)  because [150], by (F-Abs) 
  150] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u), x') >= /\x.V(x', x)  because [151], by (F-Abs) 
  151] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u), x', y') >= V(x', y')  because [152], by (Select) 
  152] V(insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u), x', y'), insert*(X, cons(Y, Z), /\z'./\u'.U(z', u'), /\v'./\w'.V(v', w'), x', y')) >= V(x', y')  because [153] and [155], by (Meta) 
  153] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u), x', y') >= x'  because [154], by (Select) 
  154] x' >= x'  by (Var) 
  155] insert*(X, cons(Y, Z), /\x./\y.U(x, y), /\z./\u.V(z, u), x', y') >= y'  because [156], by (Select) 
  156] y' >= y'  by (Var) 

  157] sort(_|_, /\x./\y.X(x, y), /\z./\u.Y(z, u)) >= _|_  by (Bot) 

  158] 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 [159], by (Star) 
  159] 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, [160], [161], [162] and [163], by (Copy) 
  160] sort*(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) >= X  because [49], by (Select) 
  161] 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, [71], [73] and [74], by (Stat) 
  162] sort*(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) >= /\x./\y.Z(x, y)  because [73], by (Select) 
  163] sort*(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) >= /\x./\y.U(x, y)  because [74], by (Select) 

  164] #argfun-asort#(sort(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u))) >= sort(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u))  because [165], by (Star) 
  165] #argfun-asort#*(sort(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u))) >= sort(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u))  because #argfun-asort# > sort, [166], [169] and [176], by (Copy) 
  166] #argfun-asort#*(sort(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u))) >= X  because [167], by (Select) 
  167] sort(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u)) >= X  because [168], by (Star) 
  168] sort*(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u)) >= X  because [100], by (Select) 
  169] #argfun-asort#*(sort(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u))) >= /\x./\y.min-(x, y)  because [170], by (F-Abs) 
  170] #argfun-asort#*(sort(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u)), v) >= /\x.min-(v, x)  because [171], by (F-Abs) 
  171] #argfun-asort#*(sort(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u)), v, w) >= min-(v, w)  because #argfun-asort# > min-, [172] and [174], by (Copy) 
  172] #argfun-asort#*(sort(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u)), v, w) >= v  because [173], by (Select) 
  173] v >= v  by (Var) 
  174] #argfun-asort#*(sort(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u)), v, w) >= w  because [175], by (Select) 
  175] w >= w  by (Var) 
  176] #argfun-asort#*(sort(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u))) >= /\x./\y.max-(x, y)  because [177], by (F-Abs) 
  177] #argfun-asort#*(sort(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u)), x') >= /\x.max-(x', x)  because [178], by (F-Abs) 
  178] #argfun-asort#*(sort(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u)), x', y') >= max-(x', y')  because #argfun-asort# > max-, [179] and [181], by (Copy) 
  179] #argfun-asort#*(sort(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u)), x', y') >= x'  because [180], by (Select) 
  180] x' >= x'  by (Var) 
  181] #argfun-asort#*(sort(X, /\x./\y.min-(x, y), /\z./\u.max-(z, u)), x', y') >= y'  because [182], by (Select) 
  182] y' >= y'  by (Var) 

  183] #argfun-dsort#(sort(X, /\x./\y.max-(x, y), /\z./\u.min-(z, u))) >= sort(X, /\x./\y.max-(x, y), /\z./\u.min-(z, u))  because [184], by (Star) 
  184] #argfun-dsort#*(sort(X, /\x./\y.max-(x, y), /\z./\u.min-(z, u))) >= sort(X, /\x./\y.max-(x, y), /\z./\u.min-(z, u))  because #argfun-dsort# > sort, [185], [188] and [195], by (Copy) 
  185] #argfun-dsort#*(sort(X, /\x./\y.max-(x, y), /\z./\u.min-(z, u))) >= X  because [186], by (Select) 
  186] sort(X, /\x./\y.max-(x, y), /\z./\u.min-(z, u)) >= X  because [187], by (Star) 
  187] sort*(X, /\x./\y.max-(x, y), /\z./\u.min-(z, u)) >= X  because [116], by (Select) 
  188] #argfun-dsort#*(sort(X, /\x./\y.max-(x, y), /\z./\u.min-(z, u))) >= /\x./\y.max-(x, y)  because [189], by (F-Abs) 
  189] #argfun-dsort#*(sort(X, /\x./\y.max-(x, y), /\z./\u.min-(z, u)), v) >= /\x.max-(v, x)  because [190], by (F-Abs) 
  190] #argfun-dsort#*(sort(X, /\x./\y.max-(x, y), /\z./\u.min-(z, u)), v, w) >= max-(v, w)  because #argfun-dsort# > max-, [191] and [193], by (Copy) 
  191] #argfun-dsort#*(sort(X, /\x./\y.max-(x, y), /\z./\u.min-(z, u)), v, w) >= v  because [192], by (Select) 
  192] v >= v  by (Var) 
  193] #argfun-dsort#*(sort(X, /\x./\y.max-(x, y), /\z./\u.min-(z, u)), v, w) >= w  because [194], by (Select) 
  194] w >= w  by (Var) 
  195] #argfun-dsort#*(sort(X, /\x./\y.max-(x, y), /\z./\u.min-(z, u))) >= /\x./\y.min-(x, y)  because [196], by (F-Abs) 
  196] #argfun-dsort#*(sort(X, /\x./\y.max-(x, y), /\z./\u.min-(z, u)), x') >= /\x.min-(x', x)  because [197], by (F-Abs) 
  197] #argfun-dsort#*(sort(X, /\x./\y.max-(x, y), /\z./\u.min-(z, u)), x', y') >= min-(x', y')  because #argfun-dsort# > min-, [198] and [200], by (Copy) 
  198] #argfun-dsort#*(sort(X, /\x./\y.max-(x, y), /\z./\u.min-(z, u)), x', y') >= x'  because [199], by (Select) 
  199] x' >= x'  by (Var) 
  200] #argfun-dsort#*(sort(X, /\x./\y.max-(x, y), /\z./\u.min-(z, u)), x', y') >= y'  because [201], by (Select) 
  201] y' >= y'  by (Var) 

  202] max-(X, Y) >= Y  because [203], by (Star) 
  203] max-*(X, Y) >= Y  because [204], by (Select) 
  204] Y >= Y  by (Meta) 

  205] min-(X, Y) >= _|_  by (Bot) 

By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_0, R_0, minimal, formative) by (P_1, R_0, minimal, formative), where P_1 consists of:

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

Thus, the original system is terminating if (P_1, R_0, minimal, formative) is finite.

We consider the dependency pair problem (P_1, R_0, minimal, formative).

We place the elements of P in a dependency graph approximation G (see e.g. [Kop12, Thm. 7.27, 7.29], as follows:

    * 0 : 0 
    * 1 : 0 
    * 2 : 1, 2 
    * 3 : 1, 2 
    * 4 : 1, 2 

This graph has the following strongly connected components:

  P_2:

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

  P_3:

    sort#(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u)) =#> sort#(Y, /\v./\w.Z(v, w), /\x'./\y'.U(x', y'))   

By [Kop12, Thm. 7.31], we may replace any dependency pair problem (P_1, R_0, m, f) by (P_2, R_0, m, f) and (P_3, R_0, m, f).

Thus, the original system is terminating if each of (P_2, R_0, minimal, formative) and (P_3, R_0, minimal, formative) is finite.

We consider the dependency pair problem (P_3, R_0, minimal, formative).

We apply the subterm criterion with the following projection function:

  nu(sort#) = 1 

Thus, we can orient the dependency pairs as follows:

  nu(sort#(cons(X, Y), /\x./\y.Z(x, y), /\z./\u.U(z, u))) = cons(X, Y) |> Y = nu(sort#(Y, /\v./\w.Z(v, w), /\x'./\y'.U(x', y'))) 

By [FuhKop19, Thm. 61], we may replace a dependency pair problem (P_3, R_0, minimal, f) by ({}, R_0, minimal, f).  By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed.

Thus, the original system is terminating if (P_2, R_0, minimal, formative) is finite.

We consider the dependency pair problem (P_2, R_0, minimal, formative).

We apply the subterm criterion with the following projection function:

  nu(insert#) = 2 

Thus, we can orient the dependency pairs as follows:

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

By [FuhKop19, Thm. 61], we may replace a dependency pair problem (P_2, R_0, minimal, f) by ({}, R_0, minimal, f).  By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed.

As all dependency pair problems were succesfully simplified with sound (and complete) processors until nothing remained, we conclude termination.


+++ Citations +++

[FuhKop19]  C. Fuhs, and C. Kop.  A static higher-order dependency pair framework.  In Proceedings of ESOP 2019, 2019.
[Kop12]  C. Kop.  Higher Order Termination.  PhD Thesis, 2012.