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_3, x_4, x_2, 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 > sort > max > insert > cons > min > s > @_{o -> o} > @_{o -> o -> o}

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 (Star) 
  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 definition 
  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, _|_) > _|_  because [18], by definition 
  18] min*(X, _|_) >= _|_  by (Bot) 

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

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

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

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

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

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

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

We can thus remove the following rules:

  max(s(X), s(Y)) => s(max(X, Y)) 
  min(X, 0) => 0 
  min(s(X), s(Y)) => s(min(X, Y)) 
  insert(X, nil, F, G) => cons(X, nil) 
  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]):

  max(0, X) >? X 
  max(X, 0) >? X 
  min(0, X) >? 0 
  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:

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

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

  max(0, X) >= X 
  max(X, 0) > X 
  min(0, X) > 0 
  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] max(0, X) >= X  because [2], by (Star) 
  2] max*(0, X) >= X  because [3], by (Select) 
  3] X >= X  by (Meta) 

  4] max(X, 0) > X  because [5], by definition 
  5] max*(X, 0) >= X  because [6], by (Select) 
  6] X >= X  by (Meta) 

  7] min(0, X) > 0  because [8], by definition 
  8] min*(0, X) >= 0  because min > 0, by (Copy) 

  9] 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 [10], by definition 
  10] 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, [11] and [21], by (Copy) 
  11] insert*(X, cons(Y, Z), F, G) >= @_{o -> o}(@_{o -> o -> o}(F, X), Y)  because insert > @_{o -> o}, [12] and [17], by (Copy) 
  12] insert*(X, cons(Y, Z), F, G) >= @_{o -> o -> o}(F, X)  because insert > @_{o -> o -> o}, [13] and [15], by (Copy) 
  13] insert*(X, cons(Y, Z), F, G) >= F  because [14], by (Select) 
  14] F >= F  by (Meta) 
  15] insert*(X, cons(Y, Z), F, G) >= X  because [16], by (Select) 
  16] X >= X  by (Meta) 
  17] insert*(X, cons(Y, Z), F, G) >= Y  because [18], by (Select) 
  18] cons(Y, Z) >= Y  because [19], by (Star) 
  19] cons*(Y, Z) >= Y  because [20], by (Select) 
  20] Y >= Y  by (Meta) 
  21] insert*(X, cons(Y, Z), F, G) >= insert(@_{o -> o}(@_{o -> o -> o}(G, X), Y), Z, F, G)  because [22], [25], [29], [13] and [27], by (Stat) 
  22] cons(Y, Z) > Z  because [23], by definition 
  23] cons*(Y, Z) >= Z  because [24], by (Select) 
  24] Z >= Z  by (Meta) 
  25] insert*(X, cons(Y, Z), F, G) >= @_{o -> o}(@_{o -> o -> o}(G, X), Y)  because insert > @_{o -> o}, [26] and [17], by (Copy) 
  26] insert*(X, cons(Y, Z), F, G) >= @_{o -> o -> o}(G, X)  because insert > @_{o -> o -> o}, [27] and [15], by (Copy) 
  27] insert*(X, cons(Y, Z), F, G) >= G  because [28], by (Select) 
  28] G >= G  by (Meta) 
  29] insert*(X, cons(Y, Z), F, G) >= Z  because [30], by (Select) 
  30] cons(Y, Z) >= Z  because [23], by (Star) 

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

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

  50] descending!6220sort(X) > sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u))  because [51], by definition 
  51] descending!6220sort*(X) >= sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u))  because descending!6220sort > sort, [52], [54] and [61], by (Copy) 
  52] descending!6220sort*(X) >= X  because [53], by (Select) 
  53] X >= X  by (Meta) 
  54] descending!6220sort*(X) >= /\y./\z.max(y, z)  because [55], by (F-Abs) 
  55] descending!6220sort*(X, x) >= /\z.max(x, z)  because [56], by (F-Abs) 
  56] descending!6220sort*(X, x, y) >= max(x, y)  because descending!6220sort > max, [57] and [59], by (Copy) 
  57] descending!6220sort*(X, x, y) >= x  because [58], by (Select) 
  58] x >= x  by (Var) 
  59] descending!6220sort*(X, x, y) >= y  because [60], by (Select) 
  60] y >= y  by (Var) 
  61] descending!6220sort*(X) >= /\u./\v.min(u, v)  because [62], by (F-Abs) 
  62] descending!6220sort*(X, z) >= /\v.min(z, v)  because [63], by (F-Abs) 
  63] descending!6220sort*(X, z, u) >= min(z, u)  because descending!6220sort > min, [64] and [66], by (Copy) 
  64] descending!6220sort*(X, z, u) >= z  because [65], by (Select) 
  65] z >= z  by (Var) 
  66] descending!6220sort*(X, z, u) >= u  because [67], by (Select) 
  67] u >= u  by (Var) 

We can thus remove the following rules:

  max(X, 0) => X 
  min(0, X) => 0 
  insert(X, cons(Y, Z), F, G) => cons(F X Y, insert(G X Y, Z, F, G)) 
  descending!6220sort(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]):

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

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

Argument functions:

  [[nil]] = _|_ 

We choose Lex = {} and Mul = {0, ascending!6220sort, max, min, sort}, and the following precedence: ascending!6220sort > 0 > min > sort > max

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

  max(0, X) >= X 
  sort(_|_, F, G) > _|_ 
  ascending!6220sort(X) >= sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u)) 

With these choices, we have:

  1] max(0, X) >= X  because [2], by (Star) 
  2] max*(0, X) >= X  because [3], by (Select) 
  3] X >= X  by (Meta) 

  4] sort(_|_, F, G) > _|_  because [5], by definition 
  5] sort*(_|_, F, G) >= _|_  by (Bot) 

  6] ascending!6220sort(X) >= sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u))  because [7], by (Star) 
  7] ascending!6220sort*(X) >= sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u))  because ascending!6220sort > sort, [8], [10] and [17], by (Copy) 
  8] ascending!6220sort*(X) >= X  because [9], by (Select) 
  9] X >= X  by (Meta) 
  10] ascending!6220sort*(X) >= /\y./\z.min(y, z)  because [11], by (F-Abs) 
  11] ascending!6220sort*(X, x) >= /\z.min(x, z)  because [12], by (F-Abs) 
  12] ascending!6220sort*(X, x, y) >= min(x, y)  because ascending!6220sort > min, [13] and [15], by (Copy) 
  13] ascending!6220sort*(X, x, y) >= x  because [14], by (Select) 
  14] x >= x  by (Var) 
  15] ascending!6220sort*(X, x, y) >= y  because [16], by (Select) 
  16] y >= y  by (Var) 
  17] ascending!6220sort*(X) >= /\u./\v.max(u, v)  because [18], by (F-Abs) 
  18] ascending!6220sort*(X, z) >= /\v.max(z, v)  because [19], by (F-Abs) 
  19] ascending!6220sort*(X, z, u) >= max(z, u)  because ascending!6220sort > max, [20] and [22], by (Copy) 
  20] ascending!6220sort*(X, z, u) >= z  because [21], by (Select) 
  21] z >= z  by (Var) 
  22] ascending!6220sort*(X, z, u) >= u  because [23], by (Select) 
  23] u >= u  by (Var) 

We can thus remove the following rules:

  sort(nil, F, G) => 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]):

  max(0, X) >? X 
  ascending!6220sort(X) >? sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u)) 

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

We choose Lex = {} and Mul = {0, ascending!6220sort, max, min, sort}, and the following precedence: ascending!6220sort > 0 > max > min > sort

With these choices, we have:

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

  4] ascending!6220sort(X) >= sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u))  because [5], by (Star) 
  5] ascending!6220sort*(X) >= sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u))  because ascending!6220sort > sort, [6], [8] and [15], by (Copy) 
  6] ascending!6220sort*(X) >= X  because [7], by (Select) 
  7] X >= X  by (Meta) 
  8] ascending!6220sort*(X) >= /\y./\z.min(y, z)  because [9], by (F-Abs) 
  9] ascending!6220sort*(X, x) >= /\z.min(x, z)  because [10], by (F-Abs) 
  10] ascending!6220sort*(X, x, y) >= min(x, y)  because ascending!6220sort > min, [11] and [13], by (Copy) 
  11] ascending!6220sort*(X, x, y) >= x  because [12], by (Select) 
  12] x >= x  by (Var) 
  13] ascending!6220sort*(X, x, y) >= y  because [14], by (Select) 
  14] y >= y  by (Var) 
  15] ascending!6220sort*(X) >= /\u./\v.max(u, v)  because [16], by (F-Abs) 
  16] ascending!6220sort*(X, z) >= /\v.max(z, v)  because [17], by (F-Abs) 
  17] ascending!6220sort*(X, z, u) >= max(z, u)  because ascending!6220sort > max, [18] and [20], by (Copy) 
  18] ascending!6220sort*(X, z, u) >= z  because [19], by (Select) 
  19] z >= z  by (Var) 
  20] ascending!6220sort*(X, z, u) >= u  because [21], by (Select) 
  21] 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]):

  ascending!6220sort(X) >? sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u)) 

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

We choose Lex = {} and Mul = {ascending!6220sort, max, min, sort}, and the following precedence: ascending!6220sort > min > max > sort

With these choices, we have:

  1] ascending!6220sort(X) > sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u))  because [2], by definition 
  2] ascending!6220sort*(X) >= sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u))  because ascending!6220sort > sort, [3], [5] and [12], by (Copy) 
  3] ascending!6220sort*(X) >= X  because [4], by (Select) 
  4] X >= X  by (Meta) 
  5] ascending!6220sort*(X) >= /\y./\z.min(y, z)  because [6], by (F-Abs) 
  6] ascending!6220sort*(X, x) >= /\z.min(x, z)  because [7], by (F-Abs) 
  7] ascending!6220sort*(X, x, y) >= min(x, y)  because ascending!6220sort > min, [8] and [10], by (Copy) 
  8] ascending!6220sort*(X, x, y) >= x  because [9], by (Select) 
  9] x >= x  by (Var) 
  10] ascending!6220sort*(X, x, y) >= y  because [11], by (Select) 
  11] y >= y  by (Var) 
  12] ascending!6220sort*(X) >= /\u./\v.max(u, v)  because [13], by (F-Abs) 
  13] ascending!6220sort*(X, z) >= /\v.max(z, v)  because [14], by (F-Abs) 
  14] ascending!6220sort*(X, z, u) >= max(z, u)  because ascending!6220sort > max, [15] and [17], by (Copy) 
  15] ascending!6220sort*(X, z, u) >= z  because [16], by (Select) 
  16] z >= z  by (Var) 
  17] ascending!6220sort*(X, z, u) >= u  because [18], by (Select) 
  18] u >= u  by (Var) 

We can thus remove the following rules:

  ascending!6220sort(X) => sort(X, /\x./\y.min(x, y), /\z./\u.max(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.