We consider the system AotoYamada_05__012.

  Alphabet:

    and : [c * c] --> c 
    cons : [a * b] --> b 
    false : [] --> c 
    forall : [a -> c * b] --> c 
    forsome : [a -> c * b] --> c 
    nil : [] --> b 
    or : [c * c] --> c 
    true : [] --> c 

  Rules:

    and(true, true) => true 
    and(x, false) => false 
    and(false, x) => false 
    or(true, x) => true 
    or(x, true) => true 
    or(false, false) => false 
    forall(f, nil) => true 
    forall(f, cons(x, y)) => and(f x, forall(f, y)) 
    forsome(f, nil) => false 
    forsome(f, cons(x, y)) => or(f x, forsome(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]):

  and(true, true) >? true 
  and(X, false) >? false 
  and(false, X) >? false 
  or(true, X) >? true 
  or(X, true) >? true 
  or(false, false) >? false 
  forall(F, nil) >? true 
  forall(F, cons(X, Y)) >? and(F X, forall(F, Y)) 
  forsome(F, nil) >? false 
  forsome(F, cons(X, Y)) >? or(F X, forsome(F, Y)) 

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

Argument functions:

  [[false]] = _|_ 

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

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

  and(true, true) >= true 
  and(X, _|_) >= _|_ 
  and(_|_, X) >= _|_ 
  or(true, X) > true 
  or(X, true) >= true 
  or(_|_, _|_) >= _|_ 
  forall(F, nil) >= true 
  forall(F, cons(X, Y)) >= and(@_{o -> o}(F, X), forall(F, Y)) 
  forsome(F, nil) >= _|_ 
  forsome(F, cons(X, Y)) > or(@_{o -> o}(F, X), forsome(F, Y)) 

With these choices, we have:

  1] and(true, true) >= true  because [2], by (Star) 
  2] and*(true, true) >= true  because and > true, by (Copy) 

  3] and(X, _|_) >= _|_  by (Bot) 

  4] and(_|_, X) >= _|_  by (Bot) 

  5] or(true, X) > true  because [6], by definition 
  6] or*(true, X) >= true  because or > true, by (Copy) 

  7] or(X, true) >= true  because [8], by (Star) 
  8] or*(X, true) >= true  because or > true, by (Copy) 

  9] or(_|_, _|_) >= _|_  by (Bot) 

  10] forall(F, nil) >= true  because [11], by (Star) 
  11] forall*(F, nil) >= true  because forall > true, by (Copy) 

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

  23] forsome(F, nil) >= _|_  by (Bot) 

  24] forsome(F, cons(X, Y)) > or(@_{o -> o}(F, X), forsome(F, Y))  because [25], by definition 
  25] forsome*(F, cons(X, Y)) >= or(@_{o -> o}(F, X), forsome(F, Y))  because forsome > or, [26] and [33], by (Copy) 
  26] forsome*(F, cons(X, Y)) >= @_{o -> o}(F, X)  because forsome > @_{o -> o}, [27] and [29], by (Copy) 
  27] forsome*(F, cons(X, Y)) >= F  because [28], by (Select) 
  28] F >= F  by (Meta) 
  29] forsome*(F, cons(X, Y)) >= X  because [30], by (Select) 
  30] cons(X, Y) >= X  because [31], by (Star) 
  31] cons*(X, Y) >= X  because [32], by (Select) 
  32] X >= X  by (Meta) 
  33] forsome*(F, cons(X, Y)) >= forsome(F, Y)  because forsome in Mul, [34] and [35], by (Stat) 
  34] F >= F  by (Meta) 
  35] cons(X, Y) > Y  because [36], by definition 
  36] cons*(X, Y) >= Y  because [37], by (Select) 
  37] Y >= Y  by (Meta) 

We can thus remove the following rules:

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

  and(true, true) >? true 
  and(X, false) >? false 
  and(false, X) >? false 
  or(X, true) >? true 
  or(false, false) >? false 
  forall(F, nil) >? true 
  forall(F, cons(X, Y)) >? and(F X, forall(F, Y)) 
  forsome(F, nil) >? false 

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

Argument functions:

  [[true]] = _|_ 

We choose Lex = {} and Mul = {@_{o -> o}, and, cons, false, forall, forsome, nil, or}, and the following precedence: false = nil > forsome > forall > @_{o -> o} > cons > or > and

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

  and(_|_, _|_) >= _|_ 
  and(X, false) >= false 
  and(false, X) >= false 
  or(X, _|_) >= _|_ 
  or(false, false) > false 
  forall(F, nil) > _|_ 
  forall(F, cons(X, Y)) > and(@_{o -> o}(F, X), forall(F, Y)) 
  forsome(F, nil) >= false 

With these choices, we have:

  1] and(_|_, _|_) >= _|_  by (Bot) 

  2] and(X, false) >= false  because [3], by (Star) 
  3] and*(X, false) >= false  because [4], by (Select) 
  4] false >= false  by (Fun) 

  5] and(false, X) >= false  because [6], by (Star) 
  6] and*(false, X) >= false  because [4], by (Select) 

  7] or(X, _|_) >= _|_  by (Bot) 

  8] or(false, false) > false  because [9], by definition 
  9] or*(false, false) >= false  because [4], by (Select) 

  10] forall(F, nil) > _|_  because [11], by definition 
  11] forall*(F, nil) >= _|_  by (Bot) 

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

  26] forsome(F, nil) >= false  because [27], by (Star) 
  27] forsome*(F, nil) >= false  because [28], by (Select) 
  28] nil >= false  because nil = false, by (Fun) 

We can thus remove the following rules:

  or(false, false) => false 
  forall(F, nil) => true 
  forall(F, cons(X, Y)) => and(F X, forall(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]):

  and(true, true) >? true 
  and(X, false) >? false 
  and(false, X) >? false 
  or(X, true) >? true 
  forsome(F, nil) >? false 

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

Argument functions:

  [[false]] = _|_ 
  [[true]] = _|_ 

We choose Lex = {} and Mul = {and, forsome, nil, or}, and the following precedence: and > forsome > nil > or

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

  and(_|_, _|_) > _|_ 
  and(X, _|_) >= _|_ 
  and(_|_, X) >= _|_ 
  or(X, _|_) >= _|_ 
  forsome(F, nil) >= _|_ 

With these choices, we have:

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

  3] and(X, _|_) >= _|_  by (Bot) 

  4] and(_|_, X) >= _|_  by (Bot) 

  5] or(X, _|_) >= _|_  by (Bot) 

  6] forsome(F, nil) >= _|_  by (Bot) 

We can thus remove the following rules:

  and(true, true) => true 

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

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

  and(X, false) >? false 
  and(false, X) >? false 
  or(X, true) >? true 
  forsome(F, nil) >? false 

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

Argument functions:

  [[false]] = _|_ 
  [[true]] = _|_ 

We choose Lex = {} and Mul = {and, forsome, nil, or}, and the following precedence: forsome > and > or > nil

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

  and(X, _|_) > _|_ 
  and(_|_, X) >= _|_ 
  or(X, _|_) >= _|_ 
  forsome(F, nil) >= _|_ 

With these choices, we have:

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

  3] and(_|_, X) >= _|_  by (Bot) 

  4] or(X, _|_) >= _|_  by (Bot) 

  5] forsome(F, nil) >= _|_  by (Bot) 

We can thus remove the following rules:

  and(X, false) => 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]):

  and(false, X) >? false 
  or(X, true) >? true 
  forsome(F, nil) >? false 

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

Argument functions:

  [[false]] = _|_ 
  [[true]] = _|_ 

We choose Lex = {} and Mul = {and, forsome, nil, or}, and the following precedence: and > forsome > nil > or

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

  and(_|_, X) > _|_ 
  or(X, _|_) >= _|_ 
  forsome(F, nil) >= _|_ 

With these choices, we have:

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

  3] or(X, _|_) >= _|_  by (Bot) 

  4] forsome(F, nil) >= _|_  by (Bot) 

We can thus remove the following rules:

  and(false, X) => 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]):

  or(X, true) >? true 
  forsome(F, nil) >? false 

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

Argument functions:

  [[false]] = _|_ 
  [[true]] = _|_ 

We choose Lex = {} and Mul = {forsome, nil, or}, and the following precedence: forsome > nil > or

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

  or(X, _|_) > _|_ 
  forsome(F, nil) >= _|_ 

With these choices, we have:

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

  3] forsome(F, nil) >= _|_  by (Bot) 

We can thus remove the following rules:

  or(X, true) => true 

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

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

  forsome(F, nil) >? false 

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

Argument functions:

  [[false]] = _|_ 

We choose Lex = {} and Mul = {forsome, nil}, and the following precedence: forsome > nil

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

  forsome(F, nil) > _|_ 

With these choices, we have:

  1] forsome(F, nil) > _|_  because [2], by definition 
  2] forsome*(F, nil) >= _|_  by (Bot) 

We can thus remove the following rules:

  forsome(F, nil) => false 

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.