We consider the system AotoYamada_05__016.

  Alphabet:

    0 : [] --> a 
    cons : [a * c] --> c 
    false : [] --> b 
    filter : [a -> b] --> c -> c 
    filtersub : [b * a -> b * c] --> c 
    neq : [a] --> a -> b 
    nil : [] --> c 
    nonzero : [] --> c -> c 
    s : [a] --> a 
    true : [] --> b 

  Rules:

    neq(0) 0 => false 
    neq(0) s(x) => true 
    neq(s(x)) 0 => true 
    neq(s(x)) s(y) => neq(x) y 
    filter(f) nil => nil 
    filter(f) cons(x, y) => filtersub(f x, f, cons(x, y)) 
    filtersub(true, f, cons(x, y)) => cons(x, filter(f) y) 
    filtersub(false, f, cons(x, y)) => filter(f) y 
    nonzero => filter(neq(0)) 

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

  neq(0) 0 >? false 
  neq(0) s(X) >? true 
  neq(s(X)) 0 >? true 
  neq(s(X)) s(Y) >? neq(X) Y 
  filter(F) nil >? nil 
  filter(F) cons(X, Y) >? filtersub(F X, F, cons(X, Y)) 
  filtersub(true, F, cons(X, Y)) >? cons(X, filter(F) Y) 
  filtersub(false, F, cons(X, Y)) >? filter(F) Y 
  nonzero >? filter(neq(0)) 

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

Argument functions:

  [[0]] = _|_ 
  [[@_{o -> o}(x_1, x_2)]] = @_{o -> o}(x_2, x_1) 
  [[cons(x_1, x_2)]] = cons(x_2, x_1) 
  [[false]] = _|_ 
  [[filtersub(x_1, x_2, x_3)]] = filtersub(x_3, x_2, x_1) 
  [[nil]] = _|_ 

We choose Lex = {@_{o -> o}, cons, filter, filtersub, true} and Mul = {neq, nonzero, s}, and the following precedence: nonzero > @_{o -> o} = filtersub > filter > neq > s > cons = true

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

  @_{o -> o}(neq(_|_), _|_) >= _|_ 
  @_{o -> o}(neq(_|_), s(X)) > true 
  @_{o -> o}(neq(s(X)), _|_) > true 
  @_{o -> o}(neq(s(X)), s(Y)) >= @_{o -> o}(neq(X), Y) 
  @_{o -> o}(filter(F), _|_) > _|_ 
  @_{o -> o}(filter(F), cons(X, Y)) >= filtersub(@_{o -> o}(F, X), F, cons(X, Y)) 
  filtersub(true, F, cons(X, Y)) >= cons(X, @_{o -> o}(filter(F), Y)) 
  filtersub(_|_, F, cons(X, Y)) > @_{o -> o}(filter(F), Y) 
  nonzero > filter(neq(_|_)) 

With these choices, we have:

  1] @_{o -> o}(neq(_|_), _|_) >= _|_  by (Bot) 

  2] @_{o -> o}(neq(_|_), s(X)) > true  because [3], by definition 
  3] @_{o -> o}*(neq(_|_), s(X)) >= true  because [4], by (Select) 
  4] neq(_|_) @_{o -> o}*(neq(_|_), s(X)) >= true  because [5] 
  5] neq*(_|_, @_{o -> o}*(neq(_|_), s(X))) >= true  because neq > true, by (Copy) 

  6] @_{o -> o}(neq(s(X)), _|_) > true  because [7], by definition 
  7] @_{o -> o}*(neq(s(X)), _|_) >= true  because [8], by (Select) 
  8] neq(s(X)) @_{o -> o}*(neq(s(X)), _|_) >= true  because [9] 
  9] neq*(s(X), @_{o -> o}*(neq(s(X)), _|_)) >= true  because [10], by (Select) 
  10] @_{o -> o}*(neq(s(X)), _|_) >= true  because @_{o -> o} > true, by (Copy) 

  11] @_{o -> o}(neq(s(X)), s(Y)) >= @_{o -> o}(neq(X), Y)  because [12] and [16], by (Fun) 
  12] neq(s(X)) >= neq(X)  because neq in Mul and [13], by (Fun) 
  13] s(X) >= X  because [14], by (Star) 
  14] s*(X) >= X  because [15], by (Select) 
  15] X >= X  by (Meta) 
  16] s(Y) >= Y  because [17], by (Star) 
  17] s*(Y) >= Y  because [18], by (Select) 
  18] Y >= Y  by (Meta) 

  19] @_{o -> o}(filter(F), _|_) > _|_  because [20], by definition 
  20] @_{o -> o}*(filter(F), _|_) >= _|_  by (Bot) 

  21] @_{o -> o}(filter(F), cons(X, Y)) >= filtersub(@_{o -> o}(F, X), F, cons(X, Y))  because [22], by (Star) 
  22] @_{o -> o}*(filter(F), cons(X, Y)) >= filtersub(@_{o -> o}(F, X), F, cons(X, Y))  because @_{o -> o} = filtersub, [23], [26], [29], [32] and [37], by (Stat) 
  23] filter(F) > F  because [24], by definition 
  24] filter*(F) >= F  because [25], by (Select) 
  25] F >= F  by (Meta) 
  26] cons(X, Y) >= cons(X, Y)  because [27] and [28], by (Fun) 
  27] X >= X  by (Meta) 
  28] Y >= Y  by (Meta) 
  29] @_{o -> o}*(filter(F), cons(X, Y)) >= @_{o -> o}(F, X)  because [30], [32], [34], [36] and [30], by (Stat) 
  30] cons(X, Y) > X  because [31], by definition 
  31] cons*(X, Y) >= X  because [27], by (Select) 
  32] @_{o -> o}*(filter(F), cons(X, Y)) >= F  because [33], by (Select) 
  33] filter(F) >= F  because [24], by (Star) 
  34] @_{o -> o}*(filter(F), cons(X, Y)) >= X  because [35], by (Select) 
  35] cons(X, Y) >= X  because [31], by (Star) 
  36] filter(F) >= F  because [24], by (Star) 
  37] @_{o -> o}*(filter(F), cons(X, Y)) >= cons(X, Y)  because [26], by (Select) 

  38] filtersub(true, F, cons(X, Y)) >= cons(X, @_{o -> o}(filter(F), Y))  because [39], by (Star) 
  39] filtersub*(true, F, cons(X, Y)) >= cons(X, @_{o -> o}(filter(F), Y))  because filtersub > cons, [40] and [44], by (Copy) 
  40] filtersub*(true, F, cons(X, Y)) >= X  because [41], by (Select) 
  41] cons(X, Y) >= X  because [42], by (Star) 
  42] cons*(X, Y) >= X  because [43], by (Select) 
  43] X >= X  by (Meta) 
  44] filtersub*(true, F, cons(X, Y)) >= @_{o -> o}(filter(F), Y)  because filtersub = @_{o -> o}, [45], [48], [51] and [53], by (Stat) 
  45] cons(X, Y) > Y  because [46], by definition 
  46] cons*(X, Y) >= Y  because [47], by (Select) 
  47] Y >= Y  by (Meta) 
  48] filtersub*(true, F, cons(X, Y)) >= filter(F)  because filtersub > filter and [49], by (Copy) 
  49] filtersub*(true, F, cons(X, Y)) >= F  because [50], by (Select) 
  50] F >= F  by (Meta) 
  51] filtersub*(true, F, cons(X, Y)) >= Y  because [52], by (Select) 
  52] cons(X, Y) >= Y  because [46], by (Star) 
  53] cons(X, Y) >= Y  because [46], by (Star) 

  54] filtersub(_|_, F, cons(X, Y)) > @_{o -> o}(filter(F), Y)  because [55], by definition 
  55] filtersub*(_|_, F, cons(X, Y)) >= @_{o -> o}(filter(F), Y)  because filtersub = @_{o -> o}, [56], [59], [62] and [64], by (Stat) 
  56] cons(X, Y) > Y  because [57], by definition 
  57] cons*(X, Y) >= Y  because [58], by (Select) 
  58] Y >= Y  by (Meta) 
  59] filtersub*(_|_, F, cons(X, Y)) >= filter(F)  because filtersub > filter and [60], by (Copy) 
  60] filtersub*(_|_, F, cons(X, Y)) >= F  because [61], by (Select) 
  61] F >= F  by (Meta) 
  62] filtersub*(_|_, F, cons(X, Y)) >= Y  because [63], by (Select) 
  63] cons(X, Y) >= Y  because [57], by (Star) 
  64] cons(X, Y) >= Y  because [57], by (Star) 

  65] nonzero > filter(neq(_|_))  because [66], by definition 
  66] nonzero* >= filter(neq(_|_))  because nonzero > filter and [67], by (Copy) 
  67] nonzero* >= neq(_|_)  because nonzero > neq and [68], by (Copy) 
  68] nonzero* >= _|_  by (Bot) 

We can thus remove the following rules:

  neq(0) s(X) => true 
  neq(s(X)) 0 => true 
  filter(F) nil => nil 
  filtersub(false, F, cons(X, Y)) => filter(F) Y 
  nonzero => filter(neq(0)) 

We use the dependency pair framework as described in [Kop12, Ch. 6/7], with static dependency pairs (see [KusIsoSakBla09] and the adaptation for AFSMs and accessible arguments in [FuhKop19]).

We thus obtain the following dependency pair problem (P_0, R_0, computable, formative):

  Dependency Pairs P_0:

    0] neq#(s(X), s(Y)) =#> neq#(X, Y)   
    1] filter#(F, cons(X, Y)) =#> filtersub#(F X, F, cons(X, Y))   
    2] filtersub#(true, F, cons(X, Y)) =#> filter#(F, Y)   

  Rules R_0:

    neq(0, 0) => false 
    neq(s(X), s(Y)) => neq(X, Y) 
    filter(F, cons(X, Y)) => filtersub(F X, F, cons(X, Y)) 
    filtersub(true, F, cons(X, Y)) => cons(X, filter(F, Y)) 

Thus, the original system is terminating if (P_0, R_0, computable, formative) is finite.

We consider the dependency pair problem (P_0, R_0, computable, 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 
    * 2 : 1 

This graph has the following strongly connected components:

  P_1:

    neq#(s(X), s(Y)) =#> neq#(X, Y)   

  P_2:

    filter#(F, cons(X, Y)) =#> filtersub#(F X, F, cons(X, Y))   
    filtersub#(true, F, cons(X, Y)) =#> filter#(F, Y)   

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) and (P_2, R_0, m, f).

Thus, the original system is terminating if each of (P_1, R_0, computable, formative) and (P_2, R_0, computable, formative) is finite.

We consider the dependency pair problem (P_2, R_0, computable, formative).

We apply the subterm criterion with the following projection function:

  nu(filter#) = 2 
  nu(filtersub#) = 3 

Thus, we can orient the dependency pairs as follows:

  nu(filter#(F, cons(X, Y))) = cons(X, Y) = cons(X, Y) = nu(filtersub#(F X, F, cons(X, Y))) 
  nu(filtersub#(true, F, cons(X, Y))) = cons(X, Y) |> Y = nu(filter#(F, Y)) 

By [FuhKop19, Thm. 61], we may replace a dependency pair problem (P_2, R_0, computable, f) by (P_3, R_0, computable, f), where P_3 contains:

  filter#(F, cons(X, Y)) =#> filtersub#(F X, F, cons(X, Y))   

Thus, the original system is terminating if each of (P_1, R_0, computable, formative) and (P_3, R_0, computable, formative) is finite.

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

This graph has no strongly connected components.  By [Kop12, Thm. 7.31], this implies finiteness of the dependency pair problem.

Thus, the original system is terminating if (P_1, R_0, computable, formative) is finite.

We consider the dependency pair problem (P_1, R_0, computable, formative).

We apply the subterm criterion with the following projection function:

  nu(neq#) = 1 

Thus, we can orient the dependency pairs as follows:

  nu(neq#(s(X), s(Y))) = s(X) |> X = nu(neq#(X, Y)) 

By [FuhKop19, Thm. 61], we may replace a dependency pair problem (P_1, R_0, computable, f) by ({}, R_0, computable, f).  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 +++

[FuhKop19]  C. Fuhs, and C. Kop.  A static higher-order dependency pair framework.  In Proceedings of ESOP 2019, 2019.
[Kop12]  C. Kop.  Higher Order Termination.  PhD Thesis, 2012.
[KusIsoSakBla09]  K. Kusakari, Y. Isogai, M. Sakai, and F. Blanqui.  Static Dependency Pair Method Based On Strong Computability for Higher-Order Rewrite Systems.  In volume 92(10) of IEICE Transactions on Information and Systems.  2007--2015, 2009.