We consider the system sort.

  Alphabet:

    0 : [] --> nat 
    ascending!6220sort : [list] --> list 
    cons : [nat * list] --> list 
    descending!6220sort : [list] --> list 
    insert : [nat * list * nat -> nat -> nat * nat -> nat -> nat] --> list 
    max : [nat * nat] --> nat 
    min : [nat * nat] --> nat 
    nil : [] --> list 
    s : [nat] --> nat 
    sort : [list * nat -> nat -> nat * nat -> nat -> nat] --> list 

  Rules:

    max(0, x) => x 
    max(x, 0) => x 
    max(s(x), s(y)) => s(max(x, y)) 
    min(0, x) => 0 
    min(x, 0) => 0 
    min(s(x), s(y)) => s(min(x, y)) 
    insert(x, nil, f, g) => cons(x, nil) 
    insert(x, cons(y, z), f, g) => cons(f x y, insert(g x y, z, f, g)) 
    sort(nil, f, g) => nil 
    sort(cons(x, y), f, g) => insert(x, sort(y, f, g), f, g) 
    ascending!6220sort(x) => sort(x, /\y./\z.min(y, z), /\u./\v.max(u, v)) 
    descending!6220sort(x) => sort(x, /\y./\z.max(y, z), /\u./\v.min(u, v)) 

This AFS is converted to an AFSM simply by replacing all free variables by meta-variables (with arity 0).

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

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

  max(0, X) >? X 
  max(X, 0) >? X 
  max(s(X), s(Y)) >? s(max(X, Y)) 
  min(0, X) >? 0 
  min(X, 0) >? 0 
  min(s(X), s(Y)) >? s(min(X, Y)) 
  insert(X, nil, F, G) >? cons(X, nil) 
  insert(X, cons(Y, Z), F, G) >? cons(F X Y, insert(G X Y, Z, F, G)) 
  sort(nil, F, G) >? nil 
  sort(cons(X, Y), F, G) >? insert(X, sort(Y, F, G), F, G) 
  ascending!6220sort(X) >? sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u)) 
  descending!6220sort(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:

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

We choose Lex = {insert} and Mul = {@_{o -> o -> o}, @_{o -> o}, ascending!6220sort, cons, descending!6220sort, max, min, s, sort}, and the following precedence: ascending!6220sort > descending!6220sort > max > min > s > sort > insert > @_{o -> o -> o} > @_{o -> o} > cons

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

  max(_|_, X) > X 
  max(X, _|_) >= X 
  max(s(X), s(Y)) >= s(max(X, Y)) 
  min(_|_, X) >= _|_ 
  min(X, _|_) >= _|_ 
  min(s(X), s(Y)) >= s(min(X, Y)) 
  insert(X, _|_, F, G) >= cons(X, _|_) 
  insert(X, cons(Y, Z), F, G) >= cons(@_{o -> o}(@_{o -> o -> o}(F, X), Y), insert(@_{o -> o}(@_{o -> o -> o}(G, X), Y), Z, F, G)) 
  sort(_|_, F, G) >= _|_ 
  sort(cons(X, Y), F, G) >= insert(X, sort(Y, F, G), F, G) 
  ascending!6220sort(X) >= sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u)) 
  descending!6220sort(X) >= sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u)) 

With these choices, we have:

  1] max(_|_, X) > X  because [2], by definition 
  2] max*(_|_, X) >= X  because [3], by (Select) 
  3] X >= X  by (Meta) 

  4] max(X, _|_) >= X  because [5], by (Star) 
  5] max*(X, _|_) >= X  because [6], by (Select) 
  6] X >= X  by (Meta) 

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

  16] min(_|_, X) >= _|_  by (Bot) 

  17] min(X, _|_) >= _|_  by (Bot) 

  18] min(s(X), s(Y)) >= s(min(X, Y))  because [19], by (Star) 
  19] min*(s(X), s(Y)) >= s(min(X, Y))  because min > s and [20], by (Copy) 
  20] min*(s(X), s(Y)) >= min(X, Y)  because min in Mul, [21] and [24], by (Stat) 
  21] s(X) >= X  because [22], by (Star) 
  22] s*(X) >= X  because [23], by (Select) 
  23] X >= X  by (Meta) 
  24] s(Y) > Y  because [25], by definition 
  25] s*(Y) >= Y  because [26], by (Select) 
  26] Y >= Y  by (Meta) 

  27] insert(X, _|_, F, G) >= cons(X, _|_)  because [28], by (Star) 
  28] insert*(X, _|_, F, G) >= cons(X, _|_)  because insert > cons, [29] and [31], by (Copy) 
  29] insert*(X, _|_, F, G) >= X  because [30], by (Select) 
  30] X >= X  by (Meta) 
  31] insert*(X, _|_, F, G) >= _|_  by (Bot) 

  32] insert(X, cons(Y, Z), F, G) >= cons(@_{o -> o}(@_{o -> o -> o}(F, X), Y), insert(@_{o -> o}(@_{o -> o -> o}(G, X), Y), Z, F, G))  because [33], by (Star) 
  33] insert*(X, cons(Y, Z), F, G) >= cons(@_{o -> o}(@_{o -> o -> o}(F, X), Y), insert(@_{o -> o}(@_{o -> o -> o}(G, X), Y), Z, F, G))  because insert > cons, [34] and [44], by (Copy) 
  34] insert*(X, cons(Y, Z), F, G) >= @_{o -> o}(@_{o -> o -> o}(F, X), Y)  because insert > @_{o -> o}, [35] and [40], by (Copy) 
  35] insert*(X, cons(Y, Z), F, G) >= @_{o -> o -> o}(F, X)  because insert > @_{o -> o -> o}, [36] and [38], by (Copy) 
  36] insert*(X, cons(Y, Z), F, G) >= F  because [37], by (Select) 
  37] F >= F  by (Meta) 
  38] insert*(X, cons(Y, Z), F, G) >= X  because [39], by (Select) 
  39] X >= X  by (Meta) 
  40] insert*(X, cons(Y, Z), F, G) >= Y  because [41], by (Select) 
  41] cons(Y, Z) >= Y  because [42], by (Star) 
  42] cons*(Y, Z) >= Y  because [43], by (Select) 
  43] Y >= Y  by (Meta) 
  44] insert*(X, cons(Y, Z), F, G) >= insert(@_{o -> o}(@_{o -> o -> o}(G, X), Y), Z, F, G)  because [45], [48], [52], [36] and [50], by (Stat) 
  45] cons(Y, Z) > Z  because [46], by definition 
  46] cons*(Y, Z) >= Z  because [47], by (Select) 
  47] Z >= Z  by (Meta) 
  48] insert*(X, cons(Y, Z), F, G) >= @_{o -> o}(@_{o -> o -> o}(G, X), Y)  because insert > @_{o -> o}, [49] and [40], by (Copy) 
  49] insert*(X, cons(Y, Z), F, G) >= @_{o -> o -> o}(G, X)  because insert > @_{o -> o -> o}, [50] and [38], by (Copy) 
  50] insert*(X, cons(Y, Z), F, G) >= G  because [51], by (Select) 
  51] G >= G  by (Meta) 
  52] insert*(X, cons(Y, Z), F, G) >= Z  because [53], by (Select) 
  53] cons(Y, Z) >= Z  because [46], by (Star) 

  54] sort(_|_, F, G) >= _|_  by (Bot) 

  55] sort(cons(X, Y), F, G) >= insert(X, sort(Y, F, G), F, G)  because [56], by (Star) 
  56] sort*(cons(X, Y), F, G) >= insert(X, sort(Y, F, G), F, G)  because sort > insert, [57], [61], [67] and [68], by (Copy) 
  57] sort*(cons(X, Y), F, G) >= X  because [58], by (Select) 
  58] cons(X, Y) >= X  because [59], by (Star) 
  59] cons*(X, Y) >= X  because [60], by (Select) 
  60] X >= X  by (Meta) 
  61] sort*(cons(X, Y), F, G) >= sort(Y, F, G)  because sort in Mul, [62], [65] and [66], by (Stat) 
  62] cons(X, Y) > Y  because [63], by definition 
  63] cons*(X, Y) >= Y  because [64], by (Select) 
  64] Y >= Y  by (Meta) 
  65] F >= F  by (Meta) 
  66] G >= G  by (Meta) 
  67] sort*(cons(X, Y), F, G) >= F  because [65], by (Select) 
  68] sort*(cons(X, Y), F, G) >= G  because [66], by (Select) 

  69] ascending!6220sort(X) >= sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u))  because [70], by (Star) 
  70] ascending!6220sort*(X) >= sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u))  because ascending!6220sort > sort, [71], [73] and [80], by (Copy) 
  71] ascending!6220sort*(X) >= X  because [72], by (Select) 
  72] X >= X  by (Meta) 
  73] ascending!6220sort*(X) >= /\y./\z.min(y, z)  because [74], by (F-Abs) 
  74] ascending!6220sort*(X, x) >= /\z.min(x, z)  because [75], by (F-Abs) 
  75] ascending!6220sort*(X, x, y) >= min(x, y)  because ascending!6220sort > min, [76] and [78], by (Copy) 
  76] ascending!6220sort*(X, x, y) >= x  because [77], by (Select) 
  77] x >= x  by (Var) 
  78] ascending!6220sort*(X, x, y) >= y  because [79], by (Select) 
  79] y >= y  by (Var) 
  80] ascending!6220sort*(X) >= /\u./\v.max(u, v)  because [81], by (F-Abs) 
  81] ascending!6220sort*(X, z) >= /\v.max(z, v)  because [82], by (F-Abs) 
  82] ascending!6220sort*(X, z, u) >= max(z, u)  because ascending!6220sort > max, [83] and [85], by (Copy) 
  83] ascending!6220sort*(X, z, u) >= z  because [84], by (Select) 
  84] z >= z  by (Var) 
  85] ascending!6220sort*(X, z, u) >= u  because [86], by (Select) 
  86] u >= u  by (Var) 

  87] descending!6220sort(X) >= sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u))  because [88], by (Star) 
  88] descending!6220sort*(X) >= sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u))  because descending!6220sort > sort, [89], [91] and [98], by (Copy) 
  89] descending!6220sort*(X) >= X  because [90], by (Select) 
  90] X >= X  by (Meta) 
  91] descending!6220sort*(X) >= /\y./\z.max(y, z)  because [92], by (F-Abs) 
  92] descending!6220sort*(X, x) >= /\z.max(x, z)  because [93], by (F-Abs) 
  93] descending!6220sort*(X, x, y) >= max(x, y)  because descending!6220sort > max, [94] and [96], by (Copy) 
  94] descending!6220sort*(X, x, y) >= x  because [95], by (Select) 
  95] x >= x  by (Var) 
  96] descending!6220sort*(X, x, y) >= y  because [97], by (Select) 
  97] y >= y  by (Var) 
  98] descending!6220sort*(X) >= /\u./\v.min(u, v)  because [99], by (F-Abs) 
  99] descending!6220sort*(X, z) >= /\v.min(z, v)  because [100], by (F-Abs) 
  100] descending!6220sort*(X, z, u) >= min(z, u)  because descending!6220sort > min, [101] and [103], by (Copy) 
  101] descending!6220sort*(X, z, u) >= z  because [102], by (Select) 
  102] z >= z  by (Var) 
  103] descending!6220sort*(X, z, u) >= u  because [104], by (Select) 
  104] u >= u  by (Var) 

We can thus remove the following rules:

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

  max(X, 0) >? X 
  max(s(X), s(Y)) >? s(max(X, Y)) 
  min(0, X) >? 0 
  min(X, 0) >? 0 
  min(s(X), s(Y)) >? s(min(X, Y)) 
  insert(X, nil, F, G) >? cons(X, nil) 
  insert(X, cons(Y, Z), F, G) >? cons(F X Y, insert(G X Y, Z, F, G)) 
  sort(nil, F, G) >? nil 
  sort(cons(X, Y), F, G) >? insert(X, sort(Y, F, G), F, G) 
  ascending!6220sort(X) >? sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u)) 
  descending!6220sort(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:

  [[0]] = _|_ 
  [[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 = {@_{o -> o -> o}, @_{o -> o}, ascending!6220sort, cons, descending!6220sort, max, min, s, sort}, and the following precedence: ascending!6220sort > descending!6220sort > max > min > s > sort > insert > @_{o -> o -> o} > @_{o -> o} > cons

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

  max(X, _|_) > X 
  max(s(X), s(Y)) > s(max(X, Y)) 
  min(_|_, X) >= _|_ 
  min(X, _|_) >= _|_ 
  min(s(X), s(Y)) >= s(min(X, Y)) 
  insert(X, _|_, F, G) >= cons(X, _|_) 
  insert(X, cons(Y, Z), F, G) >= cons(@_{o -> o}(@_{o -> o -> o}(F, X), Y), insert(@_{o -> o}(@_{o -> o -> o}(G, X), Y), Z, F, G)) 
  sort(_|_, F, G) >= _|_ 
  sort(cons(X, Y), F, G) > insert(X, sort(Y, F, G), F, G) 
  ascending!6220sort(X) >= sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u)) 
  descending!6220sort(X) >= sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u)) 

With these choices, we have:

  1] max(X, _|_) > X  because [2], by definition 
  2] max*(X, _|_) >= X  because [3], by (Select) 
  3] X >= X  by (Meta) 

  4] max(s(X), s(Y)) > s(max(X, Y))  because [5], by definition 
  5] max*(s(X), s(Y)) >= s(max(X, Y))  because max > s and [6], by (Copy) 
  6] max*(s(X), s(Y)) >= max(X, Y)  because max in Mul, [7] and [10], by (Stat) 
  7] s(X) >= X  because [8], by (Star) 
  8] s*(X) >= X  because [9], by (Select) 
  9] X >= X  by (Meta) 
  10] s(Y) > Y  because [11], by definition 
  11] s*(Y) >= Y  because [12], by (Select) 
  12] Y >= Y  by (Meta) 

  13] min(_|_, X) >= _|_  by (Bot) 

  14] min(X, _|_) >= _|_  by (Bot) 

  15] min(s(X), s(Y)) >= s(min(X, Y))  because [16], by (Star) 
  16] min*(s(X), s(Y)) >= s(min(X, Y))  because min > s and [17], by (Copy) 
  17] min*(s(X), s(Y)) >= min(X, Y)  because min in Mul, [18] and [21], by (Stat) 
  18] s(X) >= X  because [19], by (Star) 
  19] s*(X) >= X  because [20], by (Select) 
  20] X >= X  by (Meta) 
  21] s(Y) > Y  because [22], by definition 
  22] s*(Y) >= Y  because [23], by (Select) 
  23] Y >= Y  by (Meta) 

  24] insert(X, _|_, F, G) >= cons(X, _|_)  because [25], by (Star) 
  25] insert*(X, _|_, F, G) >= cons(X, _|_)  because insert > cons, [26] and [28], by (Copy) 
  26] insert*(X, _|_, F, G) >= X  because [27], by (Select) 
  27] X >= X  by (Meta) 
  28] insert*(X, _|_, F, G) >= _|_  by (Bot) 

  29] insert(X, cons(Y, Z), F, G) >= cons(@_{o -> o}(@_{o -> o -> o}(F, X), Y), insert(@_{o -> o}(@_{o -> o -> o}(G, X), Y), Z, F, G))  because [30], by (Star) 
  30] insert*(X, cons(Y, Z), F, G) >= cons(@_{o -> o}(@_{o -> o -> o}(F, X), Y), insert(@_{o -> o}(@_{o -> o -> o}(G, X), Y), Z, F, G))  because insert > cons, [31] and [41], by (Copy) 
  31] insert*(X, cons(Y, Z), F, G) >= @_{o -> o}(@_{o -> o -> o}(F, X), Y)  because insert > @_{o -> o}, [32] and [37], by (Copy) 
  32] insert*(X, cons(Y, Z), F, G) >= @_{o -> o -> o}(F, X)  because insert > @_{o -> o -> o}, [33] and [35], by (Copy) 
  33] insert*(X, cons(Y, Z), F, G) >= F  because [34], by (Select) 
  34] F >= F  by (Meta) 
  35] insert*(X, cons(Y, Z), F, G) >= X  because [36], by (Select) 
  36] X >= X  by (Meta) 
  37] insert*(X, cons(Y, Z), F, G) >= Y  because [38], by (Select) 
  38] cons(Y, Z) >= Y  because [39], by (Star) 
  39] cons*(Y, Z) >= Y  because [40], by (Select) 
  40] Y >= Y  by (Meta) 
  41] insert*(X, cons(Y, Z), F, G) >= insert(@_{o -> o}(@_{o -> o -> o}(G, X), Y), Z, F, G)  because [42], [45], [49], [33] and [47], by (Stat) 
  42] cons(Y, Z) > Z  because [43], by definition 
  43] cons*(Y, Z) >= Z  because [44], by (Select) 
  44] Z >= Z  by (Meta) 
  45] insert*(X, cons(Y, Z), F, G) >= @_{o -> o}(@_{o -> o -> o}(G, X), Y)  because insert > @_{o -> o}, [46] and [37], by (Copy) 
  46] insert*(X, cons(Y, Z), F, G) >= @_{o -> o -> o}(G, X)  because insert > @_{o -> o -> o}, [47] and [35], by (Copy) 
  47] insert*(X, cons(Y, Z), F, G) >= G  because [48], by (Select) 
  48] G >= G  by (Meta) 
  49] insert*(X, cons(Y, Z), F, G) >= Z  because [50], by (Select) 
  50] cons(Y, Z) >= Z  because [43], by (Star) 

  51] sort(_|_, F, G) >= _|_  by (Bot) 

  52] sort(cons(X, Y), F, G) > insert(X, sort(Y, F, G), F, G)  because [53], by definition 
  53] sort*(cons(X, Y), F, G) >= insert(X, sort(Y, F, G), F, G)  because sort > insert, [54], [58], [64] and [65], by (Copy) 
  54] sort*(cons(X, Y), F, G) >= X  because [55], by (Select) 
  55] cons(X, Y) >= X  because [56], by (Star) 
  56] cons*(X, Y) >= X  because [57], by (Select) 
  57] X >= X  by (Meta) 
  58] sort*(cons(X, Y), F, G) >= sort(Y, F, G)  because sort in Mul, [59], [62] and [63], by (Stat) 
  59] cons(X, Y) > Y  because [60], by definition 
  60] cons*(X, Y) >= Y  because [61], by (Select) 
  61] Y >= Y  by (Meta) 
  62] F >= F  by (Meta) 
  63] G >= G  by (Meta) 
  64] sort*(cons(X, Y), F, G) >= F  because [62], by (Select) 
  65] sort*(cons(X, Y), F, G) >= G  because [63], by (Select) 

  66] ascending!6220sort(X) >= sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u))  because [67], by (Star) 
  67] ascending!6220sort*(X) >= sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u))  because ascending!6220sort > sort, [68], [70] and [77], by (Copy) 
  68] ascending!6220sort*(X) >= X  because [69], by (Select) 
  69] X >= X  by (Meta) 
  70] ascending!6220sort*(X) >= /\y./\z.min(y, z)  because [71], by (F-Abs) 
  71] ascending!6220sort*(X, x) >= /\z.min(x, z)  because [72], by (F-Abs) 
  72] ascending!6220sort*(X, x, y) >= min(x, y)  because ascending!6220sort > min, [73] and [75], by (Copy) 
  73] ascending!6220sort*(X, x, y) >= x  because [74], by (Select) 
  74] x >= x  by (Var) 
  75] ascending!6220sort*(X, x, y) >= y  because [76], by (Select) 
  76] y >= y  by (Var) 
  77] ascending!6220sort*(X) >= /\u./\v.max(u, v)  because [78], by (F-Abs) 
  78] ascending!6220sort*(X, z) >= /\v.max(z, v)  because [79], by (F-Abs) 
  79] ascending!6220sort*(X, z, u) >= max(z, u)  because ascending!6220sort > max, [80] and [82], by (Copy) 
  80] ascending!6220sort*(X, z, u) >= z  because [81], by (Select) 
  81] z >= z  by (Var) 
  82] ascending!6220sort*(X, z, u) >= u  because [83], by (Select) 
  83] u >= u  by (Var) 

  84] descending!6220sort(X) >= sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u))  because [85], by (Star) 
  85] descending!6220sort*(X) >= sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u))  because descending!6220sort > sort, [86], [88] and [95], by (Copy) 
  86] descending!6220sort*(X) >= X  because [87], by (Select) 
  87] X >= X  by (Meta) 
  88] descending!6220sort*(X) >= /\y./\z.max(y, z)  because [89], by (F-Abs) 
  89] descending!6220sort*(X, x) >= /\z.max(x, z)  because [90], by (F-Abs) 
  90] descending!6220sort*(X, x, y) >= max(x, y)  because descending!6220sort > max, [91] and [93], by (Copy) 
  91] descending!6220sort*(X, x, y) >= x  because [92], by (Select) 
  92] x >= x  by (Var) 
  93] descending!6220sort*(X, x, y) >= y  because [94], by (Select) 
  94] y >= y  by (Var) 
  95] descending!6220sort*(X) >= /\u./\v.min(u, v)  because [96], by (F-Abs) 
  96] descending!6220sort*(X, z) >= /\v.min(z, v)  because [97], by (F-Abs) 
  97] descending!6220sort*(X, z, u) >= min(z, u)  because descending!6220sort > min, [98] and [100], by (Copy) 
  98] descending!6220sort*(X, z, u) >= z  because [99], by (Select) 
  99] z >= z  by (Var) 
  100] descending!6220sort*(X, z, u) >= u  because [101], by (Select) 
  101] u >= u  by (Var) 

We can thus remove the following rules:

  max(X, 0) => X 
  max(s(X), s(Y)) => s(max(X, Y)) 
  sort(cons(X, Y), F, G) => insert(X, sort(Y, F, G), F, G) 

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

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

  min(0, X) >? 0 
  min(X, 0) >? 0 
  min(s(X), s(Y)) >? s(min(X, Y)) 
  insert(X, nil, F, G) >? cons(X, nil) 
  insert(X, cons(Y, Z), F, G) >? cons(F X Y, insert(G X Y, Z, F, G)) 
  sort(nil, F, G) >? nil 
  ascending!6220sort(X) >? sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u)) 
  descending!6220sort(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:

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

We choose Lex = {insert} and Mul = {@_{o -> o -> o}, @_{o -> o}, ascending!6220sort, cons, descending!6220sort, max, min, s, sort}, and the following precedence: ascending!6220sort > descending!6220sort > insert > @_{o -> o -> o} > @_{o -> o} > cons > max > min > s > sort

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

  min(_|_, X) >= _|_ 
  min(X, _|_) >= _|_ 
  min(s(X), s(Y)) >= s(min(X, Y)) 
  insert(X, _|_, F, G) >= cons(X, _|_) 
  insert(X, cons(Y, Z), F, G) > cons(@_{o -> o}(@_{o -> o -> o}(F, X), Y), insert(@_{o -> o}(@_{o -> o -> o}(G, X), Y), Z, F, G)) 
  sort(_|_, F, G) >= _|_ 
  ascending!6220sort(X) >= sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u)) 
  descending!6220sort(X) >= sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u)) 

With these choices, we have:

  1] min(_|_, X) >= _|_  by (Bot) 

  2] min(X, _|_) >= _|_  by (Bot) 

  3] min(s(X), s(Y)) >= s(min(X, Y))  because [4], by (Star) 
  4] min*(s(X), s(Y)) >= s(min(X, Y))  because min > s and [5], by (Copy) 
  5] min*(s(X), s(Y)) >= min(X, Y)  because min in Mul, [6] and [9], by (Stat) 
  6] s(X) >= X  because [7], by (Star) 
  7] s*(X) >= X  because [8], by (Select) 
  8] X >= X  by (Meta) 
  9] s(Y) > Y  because [10], by definition 
  10] s*(Y) >= Y  because [11], by (Select) 
  11] Y >= Y  by (Meta) 

  12] insert(X, _|_, F, G) >= cons(X, _|_)  because [13], by (Star) 
  13] insert*(X, _|_, F, G) >= cons(X, _|_)  because insert > cons, [14] and [16], by (Copy) 
  14] insert*(X, _|_, F, G) >= X  because [15], by (Select) 
  15] X >= X  by (Meta) 
  16] insert*(X, _|_, F, G) >= _|_  by (Bot) 

  17] insert(X, cons(Y, Z), F, G) > cons(@_{o -> o}(@_{o -> o -> o}(F, X), Y), insert(@_{o -> o}(@_{o -> o -> o}(G, X), Y), Z, F, G))  because [18], by definition 
  18] insert*(X, cons(Y, Z), F, G) >= cons(@_{o -> o}(@_{o -> o -> o}(F, X), Y), insert(@_{o -> o}(@_{o -> o -> o}(G, X), Y), Z, F, G))  because insert > cons, [19] and [29], by (Copy) 
  19] insert*(X, cons(Y, Z), F, G) >= @_{o -> o}(@_{o -> o -> o}(F, X), Y)  because insert > @_{o -> o}, [20] and [25], by (Copy) 
  20] insert*(X, cons(Y, Z), F, G) >= @_{o -> o -> o}(F, X)  because insert > @_{o -> o -> o}, [21] and [23], by (Copy) 
  21] insert*(X, cons(Y, Z), F, G) >= F  because [22], by (Select) 
  22] F >= F  by (Meta) 
  23] insert*(X, cons(Y, Z), F, G) >= X  because [24], by (Select) 
  24] X >= X  by (Meta) 
  25] insert*(X, cons(Y, Z), F, G) >= Y  because [26], by (Select) 
  26] cons(Y, Z) >= Y  because [27], by (Star) 
  27] cons*(Y, Z) >= Y  because [28], by (Select) 
  28] Y >= Y  by (Meta) 
  29] insert*(X, cons(Y, Z), F, G) >= insert(@_{o -> o}(@_{o -> o -> o}(G, X), Y), Z, F, G)  because [30], [33], [37], [21] and [35], by (Stat) 
  30] cons(Y, Z) > Z  because [31], by definition 
  31] cons*(Y, Z) >= Z  because [32], by (Select) 
  32] Z >= Z  by (Meta) 
  33] insert*(X, cons(Y, Z), F, G) >= @_{o -> o}(@_{o -> o -> o}(G, X), Y)  because insert > @_{o -> o}, [34] and [25], by (Copy) 
  34] insert*(X, cons(Y, Z), F, G) >= @_{o -> o -> o}(G, X)  because insert > @_{o -> o -> o}, [35] and [23], by (Copy) 
  35] insert*(X, cons(Y, Z), F, G) >= G  because [36], by (Select) 
  36] G >= G  by (Meta) 
  37] insert*(X, cons(Y, Z), F, G) >= Z  because [38], by (Select) 
  38] cons(Y, Z) >= Z  because [31], by (Star) 

  39] sort(_|_, F, G) >= _|_  by (Bot) 

  40] ascending!6220sort(X) >= sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u))  because [41], by (Star) 
  41] ascending!6220sort*(X) >= sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u))  because ascending!6220sort > sort, [42], [44] and [51], by (Copy) 
  42] ascending!6220sort*(X) >= X  because [43], by (Select) 
  43] X >= X  by (Meta) 
  44] ascending!6220sort*(X) >= /\y./\z.min(y, z)  because [45], by (F-Abs) 
  45] ascending!6220sort*(X, x) >= /\z.min(x, z)  because [46], by (F-Abs) 
  46] ascending!6220sort*(X, x, y) >= min(x, y)  because ascending!6220sort > min, [47] and [49], by (Copy) 
  47] ascending!6220sort*(X, x, y) >= x  because [48], by (Select) 
  48] x >= x  by (Var) 
  49] ascending!6220sort*(X, x, y) >= y  because [50], by (Select) 
  50] y >= y  by (Var) 
  51] ascending!6220sort*(X) >= /\u./\v.max(u, v)  because [52], by (F-Abs) 
  52] ascending!6220sort*(X, z) >= /\v.max(z, v)  because [53], by (F-Abs) 
  53] ascending!6220sort*(X, z, u) >= max(z, u)  because ascending!6220sort > max, [54] and [56], by (Copy) 
  54] ascending!6220sort*(X, z, u) >= z  because [55], by (Select) 
  55] z >= z  by (Var) 
  56] ascending!6220sort*(X, z, u) >= u  because [57], by (Select) 
  57] u >= u  by (Var) 

  58] descending!6220sort(X) >= sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u))  because [59], by (Star) 
  59] descending!6220sort*(X) >= sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u))  because descending!6220sort > sort, [60], [62] and [69], by (Copy) 
  60] descending!6220sort*(X) >= X  because [61], by (Select) 
  61] X >= X  by (Meta) 
  62] descending!6220sort*(X) >= /\y./\z.max(y, z)  because [63], by (F-Abs) 
  63] descending!6220sort*(X, x) >= /\z.max(x, z)  because [64], by (F-Abs) 
  64] descending!6220sort*(X, x, y) >= max(x, y)  because descending!6220sort > max, [65] and [67], by (Copy) 
  65] descending!6220sort*(X, x, y) >= x  because [66], by (Select) 
  66] x >= x  by (Var) 
  67] descending!6220sort*(X, x, y) >= y  because [68], by (Select) 
  68] y >= y  by (Var) 
  69] descending!6220sort*(X) >= /\u./\v.min(u, v)  because [70], by (F-Abs) 
  70] descending!6220sort*(X, z) >= /\v.min(z, v)  because [71], by (F-Abs) 
  71] descending!6220sort*(X, z, u) >= min(z, u)  because descending!6220sort > min, [72] and [74], by (Copy) 
  72] descending!6220sort*(X, z, u) >= z  because [73], by (Select) 
  73] z >= z  by (Var) 
  74] descending!6220sort*(X, z, u) >= u  because [75], by (Select) 
  75] u >= u  by (Var) 

We can thus remove the following rules:

  insert(X, cons(Y, Z), F, G) => cons(F X Y, insert(G X Y, Z, F, G)) 

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

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

  min(0, X) >? 0 
  min(X, 0) >? 0 
  min(s(X), s(Y)) >? s(min(X, Y)) 
  insert(X, nil, F, G) >? cons(X, nil) 
  sort(nil, F, G) >? nil 
  ascending!6220sort(X) >? sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u)) 
  descending!6220sort(X) >? sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u)) 

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

The following interpretation satisfies the requirements:

  0 = 1 
  ascending!6220sort = \y0.3 + 3y0 
  cons = \y0y1.y0 + y1 
  descending!6220sort = \y0.3 + 3y0 
  insert = \y0y1G2G3.3 + 3y0 + 3y1 + G3(0,0) + 2G2(0,0) 
  max = \y0y1.y0 + y1 
  min = \y0y1.2y0 + 2y1 
  nil = 0 
  s = \y0.2 + y0 
  sort = \y0G1G2.2 + 2y0 + G2(0,0) + 2G1(0,0) 

Using this interpretation, the requirements translate to:

  [[min(0, _x0)]] = 2 + 2x0 > 1 = [[0]] 
  [[min(_x0, 0)]] = 2 + 2x0 > 1 = [[0]] 
  [[min(s(_x0), s(_x1))]] = 8 + 2x0 + 2x1 > 2 + 2x0 + 2x1 = [[s(min(_x0, _x1))]] 
  [[insert(_x0, nil, _F1, _F2)]] = 3 + 3x0 + F2(0,0) + 2F1(0,0) > x0 = [[cons(_x0, nil)]] 
  [[sort(nil, _F0, _F1)]] = 2 + F1(0,0) + 2F0(0,0) > 0 = [[nil]] 
  [[ascending!6220sort(_x0)]] = 3 + 3x0 > 2 + 2x0 = [[sort(_x0, /\x./\y.min(x, y), /\z./\u.max(z, u))]] 
  [[descending!6220sort(_x0)]] = 3 + 3x0 > 2 + 2x0 = [[sort(_x0, /\x./\y.max(x, y), /\z./\u.min(z, u))]] 

We can thus remove the following rules:

  min(0, X) => 0 
  min(X, 0) => 0 
  min(s(X), s(Y)) => s(min(X, Y)) 
  insert(X, nil, F, G) => cons(X, nil) 
  sort(nil, F, G) => nil 
  ascending!6220sort(X) => sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u)) 
  descending!6220sort(X) => sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u)) 

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.