We consider the system onearg.

  Alphabet:

    0 : [] --> nat 
    add : [nat] --> nat -> nat 
    eq : [nat] --> nat -> bool 
    err : [] --> nat 
    false : [] --> bool 
    id : [] --> nat -> nat 
    nul : [] --> nat -> bool 
    pred : [nat] --> nat 
    s : [nat] --> nat 
    true : [] --> bool 

  Rules:

    nul 0 => true 
    nul s(x) => false 
    nul err => false 
    pred(0) => err 
    pred(s(x)) => x 
    id x => x 
    eq(0) => nul 
    eq(s(x)) => /\y.eq(x) pred(y) 
    add(0) => id 
    add(s(x)) => /\y.add(x) s(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]):

  nul 0 >? true 
  nul s(X) >? false 
  nul err >? false 
  pred(0) >? err 
  pred(s(X)) >? X 
  id X >? X 
  eq(0) >? nul 
  eq(s(X)) >? /\x.eq(X) pred(x) 
  add(0) >? id 
  add(s(X)) >? /\x.add(X) s(x) 

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

Argument functions:

  [[false]] = _|_ 
  [[id]] = _|_ 
  [[nul]] = _|_ 
  [[true]] = _|_ 

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

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

  @_{o -> o}(_|_, 0) >= _|_ 
  @_{o -> o}(_|_, s(X)) > _|_ 
  @_{o -> o}(_|_, err) >= _|_ 
  pred(0) >= err 
  pred(s(X)) > X 
  @_{o -> o}(_|_, X) >= X 
  eq(0) >= _|_ 
  eq(s(X)) >= /\x.@_{o -> o}(eq(X), pred(x)) 
  add(0) >= _|_ 
  add(s(X)) >= /\x.@_{o -> o}(add(X), s(x)) 

With these choices, we have:

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

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

  4] @_{o -> o}(_|_, err) >= _|_  by (Bot) 

  5] pred(0) >= err  because [6], by (Star) 
  6] pred*(0) >= err  because pred > err, by (Copy) 

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

  12] @_{o -> o}(_|_, X) >= X  because [13], by (Star) 
  13] @_{o -> o}*(_|_, X) >= X  because [14], by (Select) 
  14] X >= X  by (Meta) 

  15] eq(0) >= _|_  by (Bot) 

  16] eq(s(X)) >= /\x.@_{o -> o}(eq(X), pred(x))  because [17], by (Star) 
  17] eq*(s(X)) >= /\y.@_{o -> o}(eq(X), pred(y))  because [18], by (F-Abs) 
  18] eq*(s(X), x) >= @_{o -> o}(eq(X), pred(x))  because eq > @_{o -> o}, [19] and [23], by (Copy) 
  19] eq*(s(X), x) >= eq(X)  because eq in Mul and [20], by (Stat) 
  20] s(X) > X  because [21], by definition 
  21] s*(X) >= X  because [22], by (Select) 
  22] X >= X  by (Meta) 
  23] eq*(s(X), x) >= pred(x)  because eq > pred and [24], by (Copy) 
  24] eq*(s(X), x) >= x  because [25], by (Select) 
  25] x >= x  by (Var) 

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

  27] add(s(X)) >= /\x.@_{o -> o}(add(X), s(x))  because [28], by (Star) 
  28] add*(s(X)) >= /\y.@_{o -> o}(add(X), s(y))  because [29], by (F-Abs) 
  29] add*(s(X), x) >= @_{o -> o}(add(X), s(x))  because add > @_{o -> o}, [30] and [34], by (Copy) 
  30] add*(s(X), x) >= add(X)  because add in Mul and [31], by (Stat) 
  31] s(X) > X  because [32], by definition 
  32] s*(X) >= X  because [33], by (Select) 
  33] X >= X  by (Meta) 
  34] add*(s(X), x) >= s(x)  because add > s and [35], by (Copy) 
  35] add*(s(X), x) >= x  because [36], by (Select) 
  36] x >= x  by (Var) 

We can thus remove the following rules:

  nul s(X) => false 
  pred(s(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]):

  nul 0 >? true 
  nul err >? false 
  pred(0) >? err 
  id X >? X 
  eq(0) >? nul 
  eq(s(X)) >? /\x.eq(X) pred(x) 
  add(0) >? id 
  add(s(X)) >? /\x.add(X) s(x) 

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

Argument functions:

  [[err]] = _|_ 
  [[false]] = _|_ 
  [[id]] = _|_ 
  [[nul]] = _|_ 
  [[true]] = _|_ 

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

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

  @_{o -> o}(_|_, 0) > _|_ 
  @_{o -> o}(_|_, _|_) >= _|_ 
  pred(0) >= _|_ 
  @_{o -> o}(_|_, X) > X 
  eq(0) >= _|_ 
  eq(s(X)) > /\x.@_{o -> o}(eq(X), pred(x)) 
  add(0) > _|_ 
  add(s(X)) > /\x.@_{o -> o}(add(X), s(x)) 

With these choices, we have:

  1] @_{o -> o}(_|_, 0) > _|_  because [2], by definition 
  2] @_{o -> o}*(_|_, 0) >= _|_  by (Bot) 

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

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

  5] @_{o -> o}(_|_, X) > X  because [6], by definition 
  6] @_{o -> o}*(_|_, X) >= X  because [7], by (Select) 
  7] X >= X  by (Meta) 

  8] eq(0) >= _|_  by (Bot) 

  9] eq(s(X)) > /\x.@_{o -> o}(eq(X), pred(x))  because [10], by definition 
  10] eq*(s(X)) >= /\y.@_{o -> o}(eq(X), pred(y))  because [11], by (F-Abs) 
  11] eq*(s(X), x) >= @_{o -> o}(eq(X), pred(x))  because eq > @_{o -> o}, [12] and [16], by (Copy) 
  12] eq*(s(X), x) >= eq(X)  because eq in Mul and [13], by (Stat) 
  13] s(X) > X  because [14], by definition 
  14] s*(X) >= X  because [15], by (Select) 
  15] X >= X  by (Meta) 
  16] eq*(s(X), x) >= pred(x)  because eq > pred and [17], by (Copy) 
  17] eq*(s(X), x) >= x  because [18], by (Select) 
  18] x >= x  by (Var) 

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

  21] add(s(X)) > /\x.@_{o -> o}(add(X), s(x))  because [22], by definition 
  22] add*(s(X)) >= /\y.@_{o -> o}(add(X), s(y))  because [23], by (F-Abs) 
  23] add*(s(X), x) >= @_{o -> o}(add(X), s(x))  because add > @_{o -> o}, [24] and [28], by (Copy) 
  24] add*(s(X), x) >= add(X)  because add in Mul and [25], by (Stat) 
  25] s(X) > X  because [26], by definition 
  26] s*(X) >= X  because [27], by (Select) 
  27] X >= X  by (Meta) 
  28] add*(s(X), x) >= s(x)  because add > s and [29], by (Copy) 
  29] add*(s(X), x) >= x  because [30], by (Select) 
  30] x >= x  by (Var) 

We can thus remove the following rules:

  nul 0 => true 
  id X => X 
  eq(s(X)) => /\x.eq(X) pred(x) 
  add(0) => id 
  add(s(X)) => /\x.add(X) s(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]):

  nul err >? false 
  pred(0) >? err 
  eq(0) >? nul 

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

Argument functions:

  [[err]] = _|_ 
  [[false]] = _|_ 
  [[nul]] = _|_ 

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

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

  @_{o -> o}(_|_, _|_) > _|_ 
  pred(0) >= _|_ 
  eq(0) >= _|_ 

With these choices, we have:

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

  3] pred(0) >= _|_  by (Bot) 

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

We can thus remove the following rules:

  nul err => false 

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

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

  pred(0) >? err 
  eq(0) >? nul 

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

Argument functions:

  [[err]] = _|_ 
  [[nul]] = _|_ 

We choose Lex = {} and Mul = {0, eq, pred}, and the following precedence: 0 > eq > pred

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

  pred(0) > _|_ 
  eq(0) >= _|_ 

With these choices, we have:

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

  3] eq(0) >= _|_  by (Bot) 

We can thus remove the following rules:

  pred(0) => err 

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

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

  eq(0) >? nul 

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

Argument functions:

  [[nul]] = _|_ 

We choose Lex = {} and Mul = {0, eq}, and the following precedence: 0 > eq

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

  eq(0) > _|_ 

With these choices, we have:

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

We can thus remove the following rules:

  eq(0) => nul 

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.