We consider the system kop12thesis_ex2.11.

  Alphabet:

    cons : [nat * list] --> list 
    emap : [nat -> nat * list] --> list 
    nil : [] --> list 
    twice : [nat -> nat] --> nat -> nat 

  Rules:

    emap(f, nil) => nil 
    emap(f, cons(x, y)) => cons(f x, emap(/\z.twice(f) z, y)) 
    twice(f) x => f (f x) 

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

We use the dependency pair framework as described in [Kop12, Ch. 6/7], with dynamic dependency pairs.

After applying [Kop12, Thm. 7.22] to denote collapsing dependency pairs in an extended form, we thus obtain the following dependency pair problem (P_0, R_0, minimal, formative):

  Dependency Pairs P_0:

    0] emap#(F, cons(X, Y)) =#> F(X)   
    1] emap#(F, cons(X, Y)) =#> emap#(/\x.twice(F, x), Y)   
    2] emap#(F, cons(X, Y)) =#> twice#(F, x)   
    3] twice#(F, X) =#> F(F X)   
    4] twice#(F, X) =#> F(X)   

  Rules R_0:

    emap(F, nil) => nil 
    emap(F, cons(X, Y)) => cons(F X, emap(/\x.twice(F, x), Y)) 
    twice(F, X) => F (F X) 

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 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, 2, 3, 4 
    * 1 : 0, 1, 2 
    * 2 :  
    * 3 : 0, 1, 2, 3, 4 
    * 4 : 0, 1, 2, 3, 4 

This graph has the following strongly connected components:

  P_1:

    emap#(F, cons(X, Y)) =#> F(X)   
    emap#(F, cons(X, Y)) =#> emap#(/\x.twice(F, x), Y)   
    twice#(F, X) =#> F(F X)   
    twice#(F, X) =#> F(X)   

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

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

The formative rules of (P_1, R_0) are R_1 ::=

  emap(F, cons(X, Y)) => cons(F X, emap(/\x.twice(F, x), Y)) 

By [Kop12, Thm. 7.17], we may replace the dependency pair problem (P_1, R_0, minimal, formative) by (P_1, R_1, minimal, formative).

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

We consider the dependency pair problem (P_1, R_1, 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:

  emap#(F, cons(X, Y)) >? F(X) 
  emap#(F, cons(X, Y)) >? emap#(/\x.twice-(F, x), Y) 
  twice#(F, X) >? F(F X) 
  twice#(F, X) >? F(X) 
  emap(F, cons(X, Y)) >= cons(F X, emap(/\x.twice-(F, x), Y)) 
  twice-(F, X) >= twice(F, X) 
  twice-(F, X) >= twice#(F, X) 

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

  pi( twice#(F, X) ) = #argfun-twice##(F (F X), F X) 

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:

  [[emap(x_1, x_2)]] = emap(x_2, x_1) 
  [[emap#(x_1, x_2)]] = emap#(x_2, x_1) 
  [[twice(x_1, x_2)]] = _|_ 

We choose Lex = {emap, emap#} and Mul = {#argfun-twice##, @_{o -> o}, cons, twice-, twice#}, and the following precedence: emap > emap# > twice- > #argfun-twice## > twice# > @_{o -> o} > cons

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

  emap#(F, cons(X, Y)) >= @_{o -> o}(F, X) 
  emap#(F, cons(X, Y)) > emap#(/\x.twice-(F, x), Y) 
  #argfun-twice##(@_{o -> o}(F, @_{o -> o}(F, X)), @_{o -> o}(F, X)) >= @_{o -> o}(F, @_{o -> o}(F, X)) 
  #argfun-twice##(@_{o -> o}(F, @_{o -> o}(F, X)), @_{o -> o}(F, X)) >= @_{o -> o}(F, X) 
  emap(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), emap(/\x.twice-(F, x), Y)) 
  twice-(F, X) >= _|_ 
  twice-(F, X) >= #argfun-twice##(@_{o -> o}(F, @_{o -> o}(F, X)), @_{o -> o}(F, X)) 

With these choices, we have:

  1] emap#(F, cons(X, Y)) >= @_{o -> o}(F, X)  because [2], by (Star) 
  2] emap#*(F, cons(X, Y)) >= @_{o -> o}(F, X)  because emap# > @_{o -> o}, [3] and [5], by (Copy) 
  3] emap#*(F, cons(X, Y)) >= F  because [4], by (Select) 
  4] F >= F  by (Meta) 
  5] emap#*(F, cons(X, Y)) >= X  because [6], by (Select) 
  6] cons(X, Y) >= X  because [7], by (Star) 
  7] cons*(X, Y) >= X  because [8], by (Select) 
  8] X >= X  by (Meta) 

  9] emap#(F, cons(X, Y)) > emap#(/\x.twice-(F, x), Y)  because [10], by definition 
  10] emap#*(F, cons(X, Y)) >= emap#(/\x.twice-(F, x), Y)  because [11], [14] and [19], by (Stat) 
  11] cons(X, Y) > Y  because [12], by definition 
  12] cons*(X, Y) >= Y  because [13], by (Select) 
  13] Y >= Y  by (Meta) 
  14] emap#*(F, cons(X, Y)) >= /\y.twice-(F, y)  because [15], by (F-Abs) 
  15] emap#*(F, cons(X, Y), x) >= twice-(F, x)  because emap# > twice-, [16] and [17], by (Copy) 
  16] emap#*(F, cons(X, Y), x) >= F  because [4], by (Select) 
  17] emap#*(F, cons(X, Y), x) >= x  because [18], by (Select) 
  18] x >= x  by (Var) 
  19] emap#*(F, cons(X, Y)) >= Y  because [20], by (Select) 
  20] cons(X, Y) >= Y  because [12], by (Star) 

  21] #argfun-twice##(@_{o -> o}(F, @_{o -> o}(F, X)), @_{o -> o}(F, X)) >= @_{o -> o}(F, @_{o -> o}(F, X))  because [22], by (Star) 
  22] #argfun-twice##*(@_{o -> o}(F, @_{o -> o}(F, X)), @_{o -> o}(F, X)) >= @_{o -> o}(F, @_{o -> o}(F, X))  because [23], by (Select) 
  23] @_{o -> o}(F, @_{o -> o}(F, X)) >= @_{o -> o}(F, @_{o -> o}(F, X))  because @_{o -> o} in Mul, [24] and [25], by (Fun) 
  24] F >= F  by (Meta) 
  25] @_{o -> o}(F, X) >= @_{o -> o}(F, X)  because @_{o -> o} in Mul, [24] and [26], by (Fun) 
  26] X >= X  by (Meta) 

  27] #argfun-twice##(@_{o -> o}(F, @_{o -> o}(F, X)), @_{o -> o}(F, X)) >= @_{o -> o}(F, X)  because [28], by (Star) 
  28] #argfun-twice##*(@_{o -> o}(F, @_{o -> o}(F, X)), @_{o -> o}(F, X)) >= @_{o -> o}(F, X)  because [25], by (Select) 

  29] emap(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), emap(/\x.twice-(F, x), Y))  because [30], by (Star) 
  30] emap*(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), emap(/\x.twice-(F, x), Y))  because emap > cons, [31] and [34], by (Copy) 
  31] emap*(F, cons(X, Y)) >= @_{o -> o}(F, X)  because emap > @_{o -> o}, [32] and [33], by (Copy) 
  32] emap*(F, cons(X, Y)) >= F  because [4], by (Select) 
  33] emap*(F, cons(X, Y)) >= X  because [6], by (Select) 
  34] emap*(F, cons(X, Y)) >= emap(/\x.twice-(F, x), Y)  because [11], [35] and [40], by (Stat) 
  35] emap*(F, cons(X, Y)) >= /\y.twice-(F, y)  because [36], by (F-Abs) 
  36] emap*(F, cons(X, Y), x) >= twice-(F, x)  because emap > twice-, [37] and [38], by (Copy) 
  37] emap*(F, cons(X, Y), x) >= F  because [4], by (Select) 
  38] emap*(F, cons(X, Y), x) >= x  because [39], by (Select) 
  39] x >= x  by (Var) 
  40] emap*(F, cons(X, Y)) >= Y  because [20], by (Select) 

  41] twice-(F, X) >= _|_  by (Bot) 

  42] twice-(F, X) >= #argfun-twice##(@_{o -> o}(F, @_{o -> o}(F, X)), @_{o -> o}(F, X))  because [43], by (Star) 
  43] twice-*(F, X) >= #argfun-twice##(@_{o -> o}(F, @_{o -> o}(F, X)), @_{o -> o}(F, X))  because twice- > #argfun-twice##, [44] and [47], by (Copy) 
  44] twice-*(F, X) >= @_{o -> o}(F, @_{o -> o}(F, X))  because twice- > @_{o -> o}, [45] and [47], by (Copy) 
  45] twice-*(F, X) >= F  because [46], by (Select) 
  46] F >= F  by (Meta) 
  47] twice-*(F, X) >= @_{o -> o}(F, X)  because twice- > @_{o -> o}, [45] and [48], by (Copy) 
  48] twice-*(F, X) >= X  because [49], by (Select) 
  49] X >= X  by (Meta) 

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

  emap#(F, cons(X, Y)) =#> F(X)   
  twice#(F, X) =#> F(F X)   
  twice#(F, X) =#> F(X)   

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

We consider the dependency pair problem (P_2, R_1, 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:

  emap#(F, cons(X, Y)) >? F(X) 
  twice#(F, X) >? F(F X) 
  twice#(F, X) >? F(X) 
  emap(F, cons(X, Y)) >= cons(F X, emap(/\x.twice-(F, x), Y)) 
  twice-(F, X) >= twice(F, X) 
  twice-(F, X) >= twice#(F, X) 

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

  pi( twice#(F, X) ) = #argfun-twice##(F (F X), F X) 

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:

  [[cons(x_1, x_2)]] = x_1 
  [[twice(x_1, x_2)]] = twice(x_1) 

We choose Lex = {} and Mul = {#argfun-twice##, @_{o -> o}, emap, emap#, twice, twice-, twice#}, and the following precedence: emap > emap# > twice- > #argfun-twice## > twice > @_{o -> o} > twice#

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

  emap#(F, X) >= @_{o -> o}(F, X) 
  #argfun-twice##(@_{o -> o}(F, @_{o -> o}(F, X)), @_{o -> o}(F, X)) >= @_{o -> o}(F, @_{o -> o}(F, X)) 
  #argfun-twice##(@_{o -> o}(F, @_{o -> o}(F, X)), @_{o -> o}(F, X)) > @_{o -> o}(F, X) 
  emap(F, X) >= @_{o -> o}(F, X) 
  twice-(F, X) >= twice(F) 
  twice-(F, X) >= #argfun-twice##(@_{o -> o}(F, @_{o -> o}(F, X)), @_{o -> o}(F, X)) 

With these choices, we have:

  1] emap#(F, X) >= @_{o -> o}(F, X)  because [2], by (Star) 
  2] emap#*(F, X) >= @_{o -> o}(F, X)  because emap# > @_{o -> o}, [3] and [5], by (Copy) 
  3] emap#*(F, X) >= F  because [4], by (Select) 
  4] F >= F  by (Meta) 
  5] emap#*(F, X) >= X  because [6], by (Select) 
  6] X >= X  by (Meta) 

  7] #argfun-twice##(@_{o -> o}(F, @_{o -> o}(F, X)), @_{o -> o}(F, X)) >= @_{o -> o}(F, @_{o -> o}(F, X))  because [8], by (Star) 
  8] #argfun-twice##*(@_{o -> o}(F, @_{o -> o}(F, X)), @_{o -> o}(F, X)) >= @_{o -> o}(F, @_{o -> o}(F, X))  because [9], by (Select) 
  9] @_{o -> o}(F, @_{o -> o}(F, X)) >= @_{o -> o}(F, @_{o -> o}(F, X))  because @_{o -> o} in Mul, [10] and [11], by (Fun) 
  10] F >= F  by (Meta) 
  11] @_{o -> o}(F, X) >= @_{o -> o}(F, X)  because @_{o -> o} in Mul, [10] and [12], by (Fun) 
  12] X >= X  by (Meta) 

  13] #argfun-twice##(@_{o -> o}(F, @_{o -> o}(F, X)), @_{o -> o}(F, X)) > @_{o -> o}(F, X)  because [14], by definition 
  14] #argfun-twice##*(@_{o -> o}(F, @_{o -> o}(F, X)), @_{o -> o}(F, X)) >= @_{o -> o}(F, X)  because [11], by (Select) 

  15] emap(F, X) >= @_{o -> o}(F, X)  because [16], by (Star) 
  16] emap*(F, X) >= @_{o -> o}(F, X)  because emap > @_{o -> o}, [17] and [18], by (Copy) 
  17] emap*(F, X) >= F  because [4], by (Select) 
  18] emap*(F, X) >= X  because [6], by (Select) 

  19] twice-(F, X) >= twice(F)  because [20], by (Star) 
  20] twice-*(F, X) >= twice(F)  because twice- > twice and [21], by (Copy) 
  21] twice-*(F, X) >= F  because [22], by (Select) 
  22] F >= F  by (Meta) 

  23] twice-(F, X) >= #argfun-twice##(@_{o -> o}(F, @_{o -> o}(F, X)), @_{o -> o}(F, X))  because [24], by (Star) 
  24] twice-*(F, X) >= #argfun-twice##(@_{o -> o}(F, @_{o -> o}(F, X)), @_{o -> o}(F, X))  because twice- > #argfun-twice##, [25] and [26], by (Copy) 
  25] twice-*(F, X) >= @_{o -> o}(F, @_{o -> o}(F, X))  because twice- > @_{o -> o}, [21] and [26], by (Copy) 
  26] twice-*(F, X) >= @_{o -> o}(F, X)  because twice- > @_{o -> o}, [21] and [27], by (Copy) 
  27] twice-*(F, X) >= X  because [28], by (Select) 
  28] X >= X  by (Meta) 

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

  emap#(F, cons(X, Y)) =#> F(X)   
  twice#(F, X) =#> F(F X)   

Thus, the original system is terminating if (P_3, R_1, minimal, formative) is finite.

We consider the dependency pair problem (P_3, R_1, 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:

  emap#(F, cons(X, Y)) >? F(X) 
  twice#(F, X) >? F(F X) 
  emap(F, cons(X, Y)) >= cons(F X, emap(/\x.twice-(F, x), Y)) 
  twice-(F, X) >= twice(F, X) 
  twice-(F, X) >= twice#(F, X) 

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

  pi( twice#(F, X) ) = #argfun-twice##(F (F X)) 

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:

  [[emap(x_1, x_2)]] = emap(x_2, x_1) 
  [[twice(x_1, x_2)]] = twice(x_1) 

We choose Lex = {emap} and Mul = {#argfun-twice##, @_{o -> o}, cons, emap#, twice, twice-, twice#}, and the following precedence: twice# > emap > twice- > #argfun-twice## > emap# > @_{o -> o} > cons > twice

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

  emap#(F, cons(X, Y)) > @_{o -> o}(F, X) 
  #argfun-twice##(@_{o -> o}(F, @_{o -> o}(F, X))) > @_{o -> o}(F, @_{o -> o}(F, X)) 
  emap(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), emap(/\x.twice-(F, x), Y)) 
  twice-(F, X) >= twice(F) 
  twice-(F, X) >= #argfun-twice##(@_{o -> o}(F, @_{o -> o}(F, X))) 

With these choices, we have:

  1] emap#(F, cons(X, Y)) > @_{o -> o}(F, X)  because [2], by definition 
  2] emap#*(F, cons(X, Y)) >= @_{o -> o}(F, X)  because emap# > @_{o -> o}, [3] and [5], by (Copy) 
  3] emap#*(F, cons(X, Y)) >= F  because [4], by (Select) 
  4] F >= F  by (Meta) 
  5] emap#*(F, cons(X, Y)) >= X  because [6], by (Select) 
  6] cons(X, Y) >= X  because [7], by (Star) 
  7] cons*(X, Y) >= X  because [8], by (Select) 
  8] X >= X  by (Meta) 

  9] #argfun-twice##(@_{o -> o}(F, @_{o -> o}(F, X))) > @_{o -> o}(F, @_{o -> o}(F, X))  because [10], by definition 
  10] #argfun-twice##*(@_{o -> o}(F, @_{o -> o}(F, X))) >= @_{o -> o}(F, @_{o -> o}(F, X))  because [11], by (Select) 
  11] @_{o -> o}(F, @_{o -> o}(F, X)) >= @_{o -> o}(F, @_{o -> o}(F, X))  because @_{o -> o} in Mul, [12] and [13], by (Fun) 
  12] F >= F  by (Meta) 
  13] @_{o -> o}(F, X) >= @_{o -> o}(F, X)  because @_{o -> o} in Mul, [12] and [14], by (Fun) 
  14] X >= X  by (Meta) 

  15] emap(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), emap(/\x.twice-(F, x), Y))  because [16], by (Star) 
  16] emap*(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), emap(/\x.twice-(F, x), Y))  because emap > cons, [17] and [20], by (Copy) 
  17] emap*(F, cons(X, Y)) >= @_{o -> o}(F, X)  because emap > @_{o -> o}, [18] and [19], by (Copy) 
  18] emap*(F, cons(X, Y)) >= F  because [4], by (Select) 
  19] emap*(F, cons(X, Y)) >= X  because [6], by (Select) 
  20] emap*(F, cons(X, Y)) >= emap(/\x.twice-(F, x), Y)  because [21], [24] and [29], by (Stat) 
  21] cons(X, Y) > Y  because [22], by definition 
  22] cons*(X, Y) >= Y  because [23], by (Select) 
  23] Y >= Y  by (Meta) 
  24] emap*(F, cons(X, Y)) >= /\y.twice-(F, y)  because [25], by (F-Abs) 
  25] emap*(F, cons(X, Y), x) >= twice-(F, x)  because emap > twice-, [26] and [27], by (Copy) 
  26] emap*(F, cons(X, Y), x) >= F  because [4], by (Select) 
  27] emap*(F, cons(X, Y), x) >= x  because [28], by (Select) 
  28] x >= x  by (Var) 
  29] emap*(F, cons(X, Y)) >= Y  because [30], by (Select) 
  30] cons(X, Y) >= Y  because [22], by (Star) 

  31] twice-(F, X) >= twice(F)  because [32], by (Star) 
  32] twice-*(F, X) >= twice(F)  because twice- > twice and [33], by (Copy) 
  33] twice-*(F, X) >= F  because [34], by (Select) 
  34] F >= F  by (Meta) 

  35] twice-(F, X) >= #argfun-twice##(@_{o -> o}(F, @_{o -> o}(F, X)))  because [36], by (Star) 
  36] twice-*(F, X) >= #argfun-twice##(@_{o -> o}(F, @_{o -> o}(F, X)))  because twice- > #argfun-twice## and [37], by (Copy) 
  37] twice-*(F, X) >= @_{o -> o}(F, @_{o -> o}(F, X))  because twice- > @_{o -> o}, [33] and [38], by (Copy) 
  38] twice-*(F, X) >= @_{o -> o}(F, X)  because twice- > @_{o -> o}, [33] and [39], by (Copy) 
  39] twice-*(F, X) >= X  because [40], by (Select) 
  40] X >= X  by (Meta) 

By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_3, R_1) by ({}, R_1).  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 +++

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