We consider the system AotoYamada_05__Ex1SimplyTyped.

  Alphabet:

    0 : [] --> a 
    add : [a] --> a -> a 
    cons : [b * c] --> c 
    id : [] --> a -> a 
    map : [b -> b * c] --> c 
    nil : [] --> c 
    s : [a] --> a 

  Rules:

    id x => x 
    add(0) => id 
    add(s(x)) y => s(add(x) y) 
    map(f, nil) => nil 
    map(f, cons(x, y)) => cons(f x, map(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]):

  id X >? X 
  add(0) >? id 
  add(s(X)) Y >? s(add(X) Y) 
  map(F, nil) >? nil 
  map(F, cons(X, Y)) >? cons(F X, map(F, Y)) 

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

Argument functions:

  [[id]] = _|_ 
  [[nil]] = _|_ 
  [[s(x_1)]] = x_1 

We choose Lex = {} and Mul = {0, @_{o -> o}, add, cons, map}, and the following precedence: map > add > @_{o -> o} > 0 > cons

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

  @_{o -> o}(_|_, X) >= X 
  add(0) >= _|_ 
  @_{o -> o}(add(X), Y) >= @_{o -> o}(add(X), Y) 
  map(F, _|_) >= _|_ 
  map(F, cons(X, Y)) > cons(@_{o -> o}(F, X), map(F, Y)) 

With these choices, we have:

  1] @_{o -> o}(_|_, X) >= X  because [2], by (Star) 
  2] @_{o -> o}*(_|_, X) >= X  because [3], by (Select) 
  3] X >= X  by (Meta) 

  4] add(0) >= _|_  by (Bot) 

  5] @_{o -> o}(add(X), Y) >= @_{o -> o}(add(X), Y)  because @_{o -> o} in Mul, [6] and [8], by (Fun) 
  6] add(X) >= add(X)  because add in Mul and [7], by (Fun) 
  7] X >= X  by (Meta) 
  8] Y >= Y  by (Meta) 

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

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

We can thus remove the following rules:

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

  id X >? X 
  add(0) >? id 
  add(s(X)) Y >? s(add(X) Y) 
  map(F, nil) >? nil 

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

Argument functions:

  [[id]] = _|_ 
  [[nil]] = _|_ 
  [[s(x_1)]] = x_1 

We choose Lex = {} and Mul = {0, @_{o -> o}, add, map}, and the following precedence: add > map > 0 > @_{o -> o}

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

  @_{o -> o}(_|_, X) >= X 
  add(0) >= _|_ 
  @_{o -> o}(add(X), Y) >= @_{o -> o}(add(X), Y) 
  map(F, _|_) > _|_ 

With these choices, we have:

  1] @_{o -> o}(_|_, X) >= X  because [2], by (Star) 
  2] @_{o -> o}*(_|_, X) >= X  because [3], by (Select) 
  3] X >= X  by (Meta) 

  4] add(0) >= _|_  by (Bot) 

  5] @_{o -> o}(add(X), Y) >= @_{o -> o}(add(X), Y)  because @_{o -> o} in Mul, [6] and [8], by (Fun) 
  6] add(X) >= add(X)  because add in Mul and [7], by (Fun) 
  7] X >= X  by (Meta) 
  8] Y >= Y  by (Meta) 

  9] map(F, _|_) > _|_  because [10], by definition 
  10] map*(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]):

  id X >? X 
  add(0) >? id 
  add(s(X)) Y >? s(add(X) Y) 

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

Argument functions:

  [[id]] = _|_ 
  [[s(x_1)]] = x_1 

We choose Lex = {} and Mul = {0, @_{o -> o}, add}, and the following precedence: add > @_{o -> o} > 0

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

  @_{o -> o}(_|_, X) > X 
  add(0) >= _|_ 
  @_{o -> o}(add(X), Y) >= @_{o -> o}(add(X), Y) 

With these choices, we have:

  1] @_{o -> o}(_|_, X) > X  because [2], by definition 
  2] @_{o -> o}*(_|_, X) >= X  because [3], by (Select) 
  3] X >= X  by (Meta) 

  4] add(0) >= _|_  by (Bot) 

  5] @_{o -> o}(add(X), Y) >= @_{o -> o}(add(X), Y)  because @_{o -> o} in Mul, [6] and [8], by (Fun) 
  6] add(X) >= add(X)  because add in Mul and [7], by (Fun) 
  7] X >= X  by (Meta) 
  8] Y >= Y  by (Meta) 

We can thus remove the following rules:

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

  add(0) >? id 
  add(s(X)) Y >? s(add(X) Y) 

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

Argument functions:

  [[id]] = _|_ 
  [[s(x_1)]] = x_1 

We choose Lex = {} and Mul = {0, @_{o -> o}, add}, and the following precedence: add > @_{o -> o} > 0

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

  add(0) > _|_ 
  @_{o -> o}(add(X), Y) >= @_{o -> o}(add(X), Y) 

With these choices, we have:

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

  3] @_{o -> o}(add(X), Y) >= @_{o -> o}(add(X), Y)  because @_{o -> o} in Mul, [4] and [6], by (Fun) 
  4] add(X) >= add(X)  because add in Mul and [5], by (Fun) 
  5] X >= X  by (Meta) 
  6] Y >= Y  by (Meta) 

We can thus remove the following rules:

  add(0) => id 

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

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

  add(s(X), Y) >? s(add(X, Y)) 

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

We choose Lex = {} and Mul = {add, s}, and the following precedence: add > s

With these choices, we have:

  1] add(s(X), Y) > s(add(X, Y))  because [2], by definition 
  2] add*(s(X), Y) >= s(add(X, Y))  because add > s and [3], by (Copy) 
  3] add*(s(X), Y) >= add(X, Y)  because add in Mul, [4] and [7], by (Stat) 
  4] s(X) > X  because [5], by definition 
  5] s*(X) >= X  because [6], by (Select) 
  6] X >= X  by (Meta) 
  7] Y >= Y  by (Meta) 

We can thus remove the following rules:

  add(s(X), Y) => s(add(X, Y)) 

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.