We consider the system Applicative_05__TakeDropWhile.

  Alphabet:

    cons : [a * c] --> c 
    dropWhile : [a -> b * c] --> c 
    if : [b * c * c] --> c 
    nil : [] --> c 
    takeWhile : [a -> b * c] --> c 
    true : [] --> b 

  Rules:

    if(true, x, y) => x 
    if(true, x, y) => y 
    takeWhile(f, nil) => nil 
    takeWhile(f, cons(x, y)) => if(f x, cons(x, takeWhile(f, y)), nil) 
    dropWhile(f, nil) => nil 
    dropWhile(f, cons(x, y)) => if(f x, dropWhile(f, y), cons(x, 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]):

  if(true, X, Y) >? X 
  if(true, X, Y) >? Y 
  takeWhile(F, nil) >? nil 
  takeWhile(F, cons(X, Y)) >? if(F X, cons(X, takeWhile(F, Y)), nil) 
  dropWhile(F, nil) >? nil 
  dropWhile(F, cons(X, Y)) >? if(F X, dropWhile(F, Y), cons(X, Y)) 

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

Argument functions:

  [[nil]] = _|_ 

We choose Lex = {} and Mul = {@_{o -> o}, cons, dropWhile, if, takeWhile, true}, and the following precedence: true > takeWhile > dropWhile > @_{o -> o} > cons > if

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

  if(true, X, Y) >= X 
  if(true, X, Y) > Y 
  takeWhile(F, _|_) >= _|_ 
  takeWhile(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, takeWhile(F, Y)), _|_) 
  dropWhile(F, _|_) > _|_ 
  dropWhile(F, cons(X, Y)) > if(@_{o -> o}(F, X), dropWhile(F, Y), cons(X, Y)) 

With these choices, we have:

  1] if(true, X, Y) >= X  because [2], by (Star) 
  2] if*(true, X, Y) >= X  because [3], by (Select) 
  3] X >= X  by (Meta) 

  4] if(true, X, Y) > Y  because [5], by definition 
  5] if*(true, X, Y) >= Y  because [6], by (Select) 
  6] Y >= Y  by (Meta) 

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

  8] takeWhile(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, takeWhile(F, Y)), _|_)  because [9], by (Star) 
  9] takeWhile*(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, takeWhile(F, Y)), _|_)  because takeWhile > if, [10], [17] and [23], by (Copy) 
  10] takeWhile*(F, cons(X, Y)) >= @_{o -> o}(F, X)  because takeWhile > @_{o -> o}, [11] and [13], by (Copy) 
  11] takeWhile*(F, cons(X, Y)) >= F  because [12], by (Select) 
  12] F >= F  by (Meta) 
  13] takeWhile*(F, cons(X, Y)) >= X  because [14], by (Select) 
  14] cons(X, Y) >= X  because [15], by (Star) 
  15] cons*(X, Y) >= X  because [16], by (Select) 
  16] X >= X  by (Meta) 
  17] takeWhile*(F, cons(X, Y)) >= cons(X, takeWhile(F, Y))  because takeWhile > cons, [13] and [18], by (Copy) 
  18] takeWhile*(F, cons(X, Y)) >= takeWhile(F, Y)  because takeWhile in Mul, [19] and [20], by (Stat) 
  19] F >= F  by (Meta) 
  20] cons(X, Y) > Y  because [21], by definition 
  21] cons*(X, Y) >= Y  because [22], by (Select) 
  22] Y >= Y  by (Meta) 
  23] takeWhile*(F, cons(X, Y)) >= _|_  by (Bot) 

  24] dropWhile(F, _|_) > _|_  because [25], by definition 
  25] dropWhile*(F, _|_) >= _|_  by (Bot) 

  26] dropWhile(F, cons(X, Y)) > if(@_{o -> o}(F, X), dropWhile(F, Y), cons(X, Y))  because [27], by definition 
  27] dropWhile*(F, cons(X, Y)) >= if(@_{o -> o}(F, X), dropWhile(F, Y), cons(X, Y))  because dropWhile > if, [28], [35] and [40], by (Copy) 
  28] dropWhile*(F, cons(X, Y)) >= @_{o -> o}(F, X)  because dropWhile > @_{o -> o}, [29] and [31], by (Copy) 
  29] dropWhile*(F, cons(X, Y)) >= F  because [30], by (Select) 
  30] F >= F  by (Meta) 
  31] dropWhile*(F, cons(X, Y)) >= X  because [32], by (Select) 
  32] cons(X, Y) >= X  because [33], by (Star) 
  33] cons*(X, Y) >= X  because [34], by (Select) 
  34] X >= X  by (Meta) 
  35] dropWhile*(F, cons(X, Y)) >= dropWhile(F, Y)  because dropWhile in Mul, [36] and [37], by (Stat) 
  36] F >= F  by (Meta) 
  37] cons(X, Y) > Y  because [38], by definition 
  38] cons*(X, Y) >= Y  because [39], by (Select) 
  39] Y >= Y  by (Meta) 
  40] dropWhile*(F, cons(X, Y)) >= cons(X, Y)  because [41], by (Select) 
  41] cons(X, Y) >= cons(X, Y)  because cons in Mul, [42] and [43], by (Fun) 
  42] X >= X  by (Meta) 
  43] Y >= Y  by (Meta) 

We can thus remove the following rules:

  if(true, X, Y) => Y 
  dropWhile(F, nil) => nil 
  dropWhile(F, cons(X, Y)) => if(F X, dropWhile(F, Y), cons(X, 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]):

  if(true, X, Y) >? X 
  takeWhile(F, nil) >? nil 
  takeWhile(F, cons(X, Y)) >? if(F X, cons(X, takeWhile(F, Y)), nil) 

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

We choose Lex = {} and Mul = {@_{o -> o}, cons, if, nil, takeWhile, true}, and the following precedence: takeWhile > @_{o -> o} > nil > cons > if > true

With these choices, we have:

  1] if(true, X, Y) >= X  because [2], by (Star) 
  2] if*(true, X, Y) >= X  because [3], by (Select) 
  3] X >= X  by (Meta) 

  4] takeWhile(F, nil) > nil  because [5], by definition 
  5] takeWhile*(F, nil) >= nil  because takeWhile > nil, by (Copy) 

  6] takeWhile(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, takeWhile(F, Y)), nil)  because [7], by (Star) 
  7] takeWhile*(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, takeWhile(F, Y)), nil)  because takeWhile > if, [8], [15] and [21], by (Copy) 
  8] takeWhile*(F, cons(X, Y)) >= @_{o -> o}(F, X)  because takeWhile > @_{o -> o}, [9] and [11], by (Copy) 
  9] takeWhile*(F, cons(X, Y)) >= F  because [10], by (Select) 
  10] F >= F  by (Meta) 
  11] takeWhile*(F, cons(X, Y)) >= X  because [12], by (Select) 
  12] cons(X, Y) >= X  because [13], by (Star) 
  13] cons*(X, Y) >= X  because [14], by (Select) 
  14] X >= X  by (Meta) 
  15] takeWhile*(F, cons(X, Y)) >= cons(X, takeWhile(F, Y))  because takeWhile > cons, [11] and [16], by (Copy) 
  16] takeWhile*(F, cons(X, Y)) >= takeWhile(F, Y)  because takeWhile in Mul, [17] and [18], by (Stat) 
  17] F >= F  by (Meta) 
  18] cons(X, Y) > Y  because [19], by definition 
  19] cons*(X, Y) >= Y  because [20], by (Select) 
  20] Y >= Y  by (Meta) 
  21] takeWhile*(F, cons(X, Y)) >= nil  because takeWhile > nil, by (Copy) 

We can thus remove the following rules:

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

  if(true, X, Y) >? X 
  takeWhile(F, cons(X, Y)) >? if(F X, cons(X, takeWhile(F, Y)), nil) 

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

Argument functions:

  [[nil]] = _|_ 

We choose Lex = {} and Mul = {@_{o -> o}, cons, if, takeWhile, true}, and the following precedence: true > takeWhile > cons > @_{o -> o} = if

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

  if(true, X, Y) > X 
  takeWhile(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, takeWhile(F, Y)), _|_) 

With these choices, we have:

  1] if(true, X, Y) > X  because [2], by definition 
  2] if*(true, X, Y) >= X  because [3], by (Select) 
  3] X >= X  by (Meta) 

  4] takeWhile(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, takeWhile(F, Y)), _|_)  because [5], by (Star) 
  5] takeWhile*(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, takeWhile(F, Y)), _|_)  because takeWhile > if, [6], [13] and [19], by (Copy) 
  6] takeWhile*(F, cons(X, Y)) >= @_{o -> o}(F, X)  because takeWhile > @_{o -> o}, [7] and [9], by (Copy) 
  7] takeWhile*(F, cons(X, Y)) >= F  because [8], by (Select) 
  8] F >= F  by (Meta) 
  9] takeWhile*(F, cons(X, Y)) >= X  because [10], by (Select) 
  10] cons(X, Y) >= X  because [11], by (Star) 
  11] cons*(X, Y) >= X  because [12], by (Select) 
  12] X >= X  by (Meta) 
  13] takeWhile*(F, cons(X, Y)) >= cons(X, takeWhile(F, Y))  because takeWhile > cons, [9] and [14], by (Copy) 
  14] takeWhile*(F, cons(X, Y)) >= takeWhile(F, Y)  because takeWhile in Mul, [15] and [16], by (Stat) 
  15] F >= F  by (Meta) 
  16] cons(X, Y) > Y  because [17], by definition 
  17] cons*(X, Y) >= Y  because [18], by (Select) 
  18] Y >= Y  by (Meta) 
  19] takeWhile*(F, cons(X, Y)) >= _|_  by (Bot) 

We can thus remove the following rules:

  if(true, X, Y) => 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]):

  takeWhile(F, cons(X, Y)) >? if(F X, cons(X, takeWhile(F, Y)), nil) 

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

Argument functions:

  [[nil]] = _|_ 

We choose Lex = {} and Mul = {@_{o -> o}, cons, if, takeWhile}, and the following precedence: takeWhile > cons > @_{o -> o} > if

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

  takeWhile(F, cons(X, Y)) > if(@_{o -> o}(F, X), cons(X, takeWhile(F, Y)), _|_) 

With these choices, we have:

  1] takeWhile(F, cons(X, Y)) > if(@_{o -> o}(F, X), cons(X, takeWhile(F, Y)), _|_)  because [2], by definition 
  2] takeWhile*(F, cons(X, Y)) >= if(@_{o -> o}(F, X), cons(X, takeWhile(F, Y)), _|_)  because takeWhile > if, [3], [10] and [16], by (Copy) 
  3] takeWhile*(F, cons(X, Y)) >= @_{o -> o}(F, X)  because takeWhile > @_{o -> o}, [4] and [6], by (Copy) 
  4] takeWhile*(F, cons(X, Y)) >= F  because [5], by (Select) 
  5] F >= F  by (Meta) 
  6] takeWhile*(F, cons(X, Y)) >= X  because [7], by (Select) 
  7] cons(X, Y) >= X  because [8], by (Star) 
  8] cons*(X, Y) >= X  because [9], by (Select) 
  9] X >= X  by (Meta) 
  10] takeWhile*(F, cons(X, Y)) >= cons(X, takeWhile(F, Y))  because takeWhile > cons, [6] and [11], by (Copy) 
  11] takeWhile*(F, cons(X, Y)) >= takeWhile(F, Y)  because takeWhile in Mul, [12] and [13], by (Stat) 
  12] F >= F  by (Meta) 
  13] cons(X, Y) > Y  because [14], by definition 
  14] cons*(X, Y) >= Y  because [15], by (Select) 
  15] Y >= Y  by (Meta) 
  16] takeWhile*(F, cons(X, Y)) >= _|_  by (Bot) 

We can thus remove the following rules:

  takeWhile(F, cons(X, Y)) => if(F X, cons(X, takeWhile(F, Y)), nil) 

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.