We consider the system Applicative_first_order_05__02.

  Alphabet:

    !facdot : [a * a] --> a 
    1 : [] --> a 
    cons : [c * d] --> d 
    false : [] --> b 
    filter : [c -> b * d] --> d 
    filter2 : [b * c -> b * c * d] --> d 
    i : [a] --> a 
    map : [c -> c * d] --> d 
    nil : [] --> d 
    true : [] --> b 

  Rules:

    !facdot(1, x) => x 
    !facdot(x, 1) => x 
    !facdot(i(x), x) => 1 
    !facdot(x, i(x)) => 1 
    !facdot(i(x), !facdot(x, y)) => y 
    !facdot(x, !facdot(i(x), y)) => y 
    i(1) => 1 
    i(i(x)) => x 
    map(f, nil) => nil 
    map(f, cons(x, y)) => cons(f x, map(f, y)) 
    filter(f, nil) => nil 
    filter(f, cons(x, y)) => filter2(f x, f, x, y) 
    filter2(true, f, x, y) => cons(x, filter(f, y)) 
    filter2(false, f, x, y) => filter(f, y) 

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

  !facdot(1, X) >? X 
  !facdot(X, 1) >? X 
  !facdot(i(X), X) >? 1 
  !facdot(X, i(X)) >? 1 
  !facdot(i(X), !facdot(X, Y)) >? Y 
  !facdot(X, !facdot(i(X), Y)) >? Y 
  i(1) >? 1 
  i(i(X)) >? X 
  map(F, nil) >? nil 
  map(F, cons(X, Y)) >? cons(F X, map(F, Y)) 
  filter(F, nil) >? nil 
  filter(F, cons(X, Y)) >? filter2(F X, F, X, Y) 
  filter2(true, F, X, Y) >? cons(X, filter(F, Y)) 
  filter2(false, F, X, Y) >? filter(F, Y) 

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

Argument functions:

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

We choose Lex = {filter, filter2} and Mul = {!facdot, 1, @_{o -> o}, cons, false, i, map, true}, and the following precedence: i > 1 > true > !facdot > filter = filter2 > false > map > @_{o -> o} > cons

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

  !facdot(1, X) >= X 
  !facdot(X, 1) > X 
  !facdot(i(X), X) >= 1 
  !facdot(X, i(X)) >= 1 
  !facdot(i(X), !facdot(X, Y)) > Y 
  !facdot(X, !facdot(i(X), Y)) > Y 
  i(1) >= 1 
  i(i(X)) >= X 
  map(F, _|_) >= _|_ 
  map(F, cons(X, Y)) > cons(@_{o -> o}(F, X), map(F, Y)) 
  filter(F, _|_) >= _|_ 
  filter(F, cons(X, Y)) > filter2(@_{o -> o}(F, X), F, X, Y) 
  filter2(true, F, X, Y) > cons(X, filter(F, Y)) 
  filter2(false, F, X, Y) >= filter(F, Y) 

With these choices, we have:

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

  4] !facdot(X, 1) > X  because [5], by definition 
  5] !facdot*(X, 1) >= X  because [6], by (Select) 
  6] X >= X  by (Meta) 

  7] !facdot(i(X), X) >= 1  because [8], by (Star) 
  8] !facdot*(i(X), X) >= 1  because [9], by (Select) 
  9] i(X) >= 1  because [10], by (Star) 
  10] i*(X) >= 1  because i > 1, by (Copy) 

  11] !facdot(X, i(X)) >= 1  because [12], by (Star) 
  12] !facdot*(X, i(X)) >= 1  because [13], by (Select) 
  13] i(X) >= 1  because [14], by (Star) 
  14] i*(X) >= 1  because i > 1, by (Copy) 

  15] !facdot(i(X), !facdot(X, Y)) > Y  because [16], by definition 
  16] !facdot*(i(X), !facdot(X, Y)) >= Y  because [17], by (Select) 
  17] !facdot(X, Y) >= Y  because [18], by (Star) 
  18] !facdot*(X, Y) >= Y  because [19], by (Select) 
  19] Y >= Y  by (Meta) 

  20] !facdot(X, !facdot(i(X), Y)) > Y  because [21], by definition 
  21] !facdot*(X, !facdot(i(X), Y)) >= Y  because [22], by (Select) 
  22] !facdot(i(X), Y) >= Y  because [23], by (Star) 
  23] !facdot*(i(X), Y) >= Y  because [24], by (Select) 
  24] Y >= Y  by (Meta) 

  25] i(1) >= 1  because [26], by (Star) 
  26] i*(1) >= 1  because i > 1, by (Copy) 

  27] i(i(X)) >= X  because [28], by (Star) 
  28] i*(i(X)) >= X  because [29], by (Select) 
  29] i(X) >= X  because [30], by (Star) 
  30] i*(X) >= X  because [31], by (Select) 
  31] X >= X  by (Meta) 

  32] map(F, _|_) >= _|_  by (Bot) 

  33] map(F, cons(X, Y)) > cons(@_{o -> o}(F, X), map(F, Y))  because [34], by definition 
  34] map*(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y))  because map > cons, [35] and [42], by (Copy) 
  35] map*(F, cons(X, Y)) >= @_{o -> o}(F, X)  because map > @_{o -> o}, [36] and [38], by (Copy) 
  36] map*(F, cons(X, Y)) >= F  because [37], by (Select) 
  37] F >= F  by (Meta) 
  38] map*(F, cons(X, Y)) >= X  because [39], by (Select) 
  39] cons(X, Y) >= X  because [40], by (Star) 
  40] cons*(X, Y) >= X  because [41], by (Select) 
  41] X >= X  by (Meta) 
  42] map*(F, cons(X, Y)) >= map(F, Y)  because map in Mul, [43] and [44], by (Stat) 
  43] F >= F  by (Meta) 
  44] cons(X, Y) > Y  because [45], by definition 
  45] cons*(X, Y) >= Y  because [46], by (Select) 
  46] Y >= Y  by (Meta) 

  47] filter(F, _|_) >= _|_  by (Bot) 

  48] filter(F, cons(X, Y)) > filter2(@_{o -> o}(F, X), F, X, Y)  because [49], by definition 
  49] filter*(F, cons(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y)  because filter = filter2, [50], [51], [54], [55], [56] and [60], by (Stat) 
  50] F >= F  by (Meta) 
  51] cons(X, Y) > Y  because [52], by definition 
  52] cons*(X, Y) >= Y  because [53], by (Select) 
  53] Y >= Y  by (Meta) 
  54] filter*(F, cons(X, Y)) >= @_{o -> o}(F, X)  because filter > @_{o -> o}, [55] and [56], by (Copy) 
  55] filter*(F, cons(X, Y)) >= F  because [50], by (Select) 
  56] filter*(F, cons(X, Y)) >= X  because [57], by (Select) 
  57] cons(X, Y) >= X  because [58], by (Star) 
  58] cons*(X, Y) >= X  because [59], by (Select) 
  59] X >= X  by (Meta) 
  60] filter*(F, cons(X, Y)) >= Y  because [61], by (Select) 
  61] cons(X, Y) >= Y  because [52], by (Star) 

  62] filter2(true, F, X, Y) > cons(X, filter(F, Y))  because [63], by definition 
  63] filter2*(true, F, X, Y) >= cons(X, filter(F, Y))  because filter2 > cons, [64] and [66], by (Copy) 
  64] filter2*(true, F, X, Y) >= X  because [65], by (Select) 
  65] X >= X  by (Meta) 
  66] filter2*(true, F, X, Y) >= filter(F, Y)  because filter2 = filter, [67], [68], [69] and [70], by (Stat) 
  67] F >= F  by (Meta) 
  68] Y >= Y  by (Meta) 
  69] filter2*(true, F, X, Y) >= F  because [67], by (Select) 
  70] filter2*(true, F, X, Y) >= Y  because [68], by (Select) 

  71] filter2(false, F, X, Y) >= filter(F, Y)  because [72], by (Star) 
  72] filter2*(false, F, X, Y) >= filter(F, Y)  because filter2 = filter, [73], [74], [75] and [76], by (Stat) 
  73] F >= F  by (Meta) 
  74] Y >= Y  by (Meta) 
  75] filter2*(false, F, X, Y) >= F  because [73], by (Select) 
  76] filter2*(false, F, X, Y) >= Y  because [74], by (Select) 

We can thus remove the following rules:

  !facdot(X, 1) => X 
  !facdot(i(X), !facdot(X, Y)) => Y 
  !facdot(X, !facdot(i(X), Y)) => Y 
  map(F, cons(X, Y)) => cons(F X, map(F, Y)) 
  filter(F, cons(X, Y)) => filter2(F X, F, X, Y) 
  filter2(true, F, X, Y) => cons(X, filter(F, Y)) 

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

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

  !facdot(1, X) >? X 
  !facdot(i(X), X) >? 1 
  !facdot(X, i(X)) >? 1 
  i(1) >? 1 
  i(i(X)) >? X 
  map(F, nil) >? nil 
  filter(F, nil) >? nil 
  filter2(false, F, X, Y) >? filter(F, Y) 

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

Argument functions:

  [[1]] = _|_ 
  [[nil]] = _|_ 

We choose Lex = {} and Mul = {!facdot, false, filter, filter2, i, map}, and the following precedence: false > i > !facdot > map > filter2 > filter

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

  !facdot(_|_, X) > X 
  !facdot(i(X), X) >= _|_ 
  !facdot(X, i(X)) >= _|_ 
  i(_|_) >= _|_ 
  i(i(X)) >= X 
  map(F, _|_) >= _|_ 
  filter(F, _|_) >= _|_ 
  filter2(false, F, X, Y) >= filter(F, Y) 

With these choices, we have:

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

  4] !facdot(i(X), X) >= _|_  by (Bot) 

  5] !facdot(X, i(X)) >= _|_  by (Bot) 

  6] i(_|_) >= _|_  by (Bot) 

  7] i(i(X)) >= X  because [8], by (Star) 
  8] i*(i(X)) >= X  because [9], by (Select) 
  9] i(X) >= X  because [10], by (Star) 
  10] i*(X) >= X  because [11], by (Select) 
  11] X >= X  by (Meta) 

  12] map(F, _|_) >= _|_  by (Bot) 

  13] filter(F, _|_) >= _|_  by (Bot) 

  14] filter2(false, F, X, Y) >= filter(F, Y)  because [15], by (Star) 
  15] filter2*(false, F, X, Y) >= filter(F, Y)  because filter2 > filter, [16] and [18], by (Copy) 
  16] filter2*(false, F, X, Y) >= F  because [17], by (Select) 
  17] F >= F  by (Meta) 
  18] filter2*(false, F, X, Y) >= Y  because [19], by (Select) 
  19] Y >= Y  by (Meta) 

We can thus remove the following rules:

  !facdot(1, 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]):

  !facdot(i(X), X) >? 1 
  !facdot(X, i(X)) >? 1 
  i(1) >? 1 
  i(i(X)) >? X 
  map(F, nil) >? nil 
  filter(F, nil) >? nil 
  filter2(false, F, X, Y) >? filter(F, Y) 

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

Argument functions:

  [[1]] = _|_ 
  [[nil]] = _|_ 

We choose Lex = {} and Mul = {!facdot, false, filter, filter2, i, map}, and the following precedence: filter2 > filter > !facdot > map > false > i

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

  !facdot(i(X), X) > _|_ 
  !facdot(X, i(X)) > _|_ 
  i(_|_) >= _|_ 
  i(i(X)) >= X 
  map(F, _|_) >= _|_ 
  filter(F, _|_) >= _|_ 
  filter2(false, F, X, Y) >= filter(F, Y) 

With these choices, we have:

  1] !facdot(i(X), X) > _|_  because [2], by definition 
  2] !facdot*(i(X), X) >= _|_  by (Bot) 

  3] !facdot(X, i(X)) > _|_  because [4], by definition 
  4] !facdot*(X, i(X)) >= _|_  by (Bot) 

  5] i(_|_) >= _|_  by (Bot) 

  6] i(i(X)) >= X  because [7], by (Star) 
  7] i*(i(X)) >= X  because [8], by (Select) 
  8] i(X) >= X  because [9], by (Star) 
  9] i*(X) >= X  because [10], by (Select) 
  10] X >= X  by (Meta) 

  11] map(F, _|_) >= _|_  by (Bot) 

  12] filter(F, _|_) >= _|_  by (Bot) 

  13] filter2(false, F, X, Y) >= filter(F, Y)  because [14], by (Star) 
  14] filter2*(false, F, X, Y) >= filter(F, Y)  because filter2 > filter, [15] and [17], by (Copy) 
  15] filter2*(false, F, X, Y) >= F  because [16], by (Select) 
  16] F >= F  by (Meta) 
  17] filter2*(false, F, X, Y) >= Y  because [18], by (Select) 
  18] Y >= Y  by (Meta) 

We can thus remove the following rules:

  !facdot(i(X), X) => 1 
  !facdot(X, i(X)) => 1 

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

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

  i(1) >? 1 
  i(i(X)) >? X 
  map(F, nil) >? nil 
  filter(F, nil) >? nil 
  filter2(false, F, X, Y) >? filter(F, Y) 

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

Argument functions:

  [[1]] = _|_ 
  [[nil]] = _|_ 

We choose Lex = {} and Mul = {false, filter, filter2, i, map}, and the following precedence: i > false > map > filter2 > filter

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

  i(_|_) >= _|_ 
  i(i(X)) >= X 
  map(F, _|_) >= _|_ 
  filter(F, _|_) >= _|_ 
  filter2(false, F, X, Y) > filter(F, Y) 

With these choices, we have:

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

  2] i(i(X)) >= X  because [3], by (Star) 
  3] i*(i(X)) >= X  because [4], by (Select) 
  4] i(X) >= X  because [5], by (Star) 
  5] i*(X) >= X  because [6], by (Select) 
  6] X >= X  by (Meta) 

  7] map(F, _|_) >= _|_  by (Bot) 

  8] filter(F, _|_) >= _|_  by (Bot) 

  9] filter2(false, F, X, Y) > filter(F, Y)  because [10], by definition 
  10] filter2*(false, F, X, Y) >= filter(F, Y)  because filter2 > filter, [11] and [13], by (Copy) 
  11] filter2*(false, F, X, Y) >= F  because [12], by (Select) 
  12] F >= F  by (Meta) 
  13] filter2*(false, F, X, Y) >= Y  because [14], by (Select) 
  14] Y >= Y  by (Meta) 

We can thus remove the following rules:

  filter2(false, F, X, Y) => filter(F, Y) 

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

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

  i(1) >? 1 
  i(i(X)) >? X 
  map(F, nil) >? nil 
  filter(F, nil) >? nil 

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

Argument functions:

  [[1]] = _|_ 
  [[nil]] = _|_ 

We choose Lex = {} and Mul = {filter, i, map}, and the following precedence: i > map > filter

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

  i(_|_) > _|_ 
  i(i(X)) >= X 
  map(F, _|_) >= _|_ 
  filter(F, _|_) >= _|_ 

With these choices, we have:

  1] i(_|_) > _|_  because [2], by definition 
  2] i*(_|_) >= _|_  by (Bot) 

  3] i(i(X)) >= X  because [4], by (Star) 
  4] i*(i(X)) >= X  because [5], by (Select) 
  5] i(X) >= X  because [6], by (Star) 
  6] i*(X) >= X  because [7], by (Select) 
  7] X >= X  by (Meta) 

  8] map(F, _|_) >= _|_  by (Bot) 

  9] filter(F, _|_) >= _|_  by (Bot) 

We can thus remove the following rules:

  i(1) => 1 

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

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

  i(i(X)) >? X 
  map(F, nil) >? nil 
  filter(F, nil) >? nil 

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

Argument functions:

  [[nil]] = _|_ 

We choose Lex = {} and Mul = {filter, i, map}, and the following precedence: i > map > filter

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

  i(i(X)) >= X 
  map(F, _|_) > _|_ 
  filter(F, _|_) >= _|_ 

With these choices, we have:

  1] i(i(X)) >= X  because [2], by (Star) 
  2] i*(i(X)) >= X  because [3], by (Select) 
  3] i(X) >= X  because [4], by (Star) 
  4] i*(X) >= X  because [5], by (Select) 
  5] X >= X  by (Meta) 

  6] map(F, _|_) > _|_  because [7], by definition 
  7] map*(F, _|_) >= _|_  by (Bot) 

  8] filter(F, _|_) >= _|_  by (Bot) 

We can thus remove the following rules:

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

  i(i(X)) >? X 
  filter(F, nil) >? nil 

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

Argument functions:

  [[nil]] = _|_ 

We choose Lex = {} and Mul = {filter, i}, and the following precedence: i > filter

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

  i(i(X)) >= X 
  filter(F, _|_) > _|_ 

With these choices, we have:

  1] i(i(X)) >= X  because [2], by (Star) 
  2] i*(i(X)) >= X  because [3], by (Select) 
  3] i(X) >= X  because [4], by (Star) 
  4] i*(X) >= X  because [5], by (Select) 
  5] X >= X  by (Meta) 

  6] filter(F, _|_) > _|_  because [7], by definition 
  7] filter*(F, _|_) >= _|_  by (Bot) 

We can thus remove the following rules:

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

  i(i(X)) >? X 

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

We choose Lex = {} and Mul = {i}, and the following precedence: i

With these choices, we have:

  1] i(i(X)) > X  because [2], by definition 
  2] i*(i(X)) >= X  because [3], by (Select) 
  3] i(X) >= X  because [4], by (Star) 
  4] i*(X) >= X  because [5], by (Select) 
  5] X >= X  by (Meta) 

We can thus remove the following rules:

  i(i(X)) => X 

All rules were succesfully removed.  Thus, termination of the original system has been reduced to termination of the beta-rule, which is well-known to hold.


+++ Citations +++

[Kop12]  C. Kop.  Higher Order Termination.  PhD Thesis, 2012.