We consider the system AotoYamada_05__009.

  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(true, false) => false 
    and(false, true) => false 
    and(false, false) => false 
    or(true, true) => true 
    or(true, false) => true 
    or(false, 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(true, false) >? false 
  and(false, true) >? false 
  and(false, false) >? false 
  or(true, true) >? true 
  or(true, false) >? true 
  or(false, 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]] = _|_ 
  [[true]] = _|_ 

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

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

  and(_|_, _|_) >= _|_ 
  and(_|_, _|_) >= _|_ 
  and(_|_, _|_) > _|_ 
  and(_|_, _|_) > _|_ 
  or(_|_, _|_) > _|_ 
  or(_|_, _|_) > _|_ 
  or(_|_, _|_) > _|_ 
  or(_|_, _|_) >= _|_ 
  forall(F, nil) >= _|_ 
  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(_|_, _|_) >= _|_  by (Bot) 

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

  3] and(_|_, _|_) > _|_  because [4], by definition 
  4] and*(_|_, _|_) >= _|_  by (Bot) 

  5] and(_|_, _|_) > _|_  because [6], by definition 
  6] and*(_|_, _|_) >= _|_  by (Bot) 

  7] or(_|_, _|_) > _|_  because [8], by definition 
  8] or*(_|_, _|_) >= _|_  by (Bot) 

  9] or(_|_, _|_) > _|_  because [10], by definition 
  10] or*(_|_, _|_) >= _|_  by (Bot) 

  11] or(_|_, _|_) > _|_  because [12], by definition 
  12] or*(_|_, _|_) >= _|_  by (Bot) 

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

  14] forall(F, nil) >= _|_  by (Bot) 

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

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

  30] forsome(F, cons(X, Y)) > or(@_{o -> o}(F, X), forsome(F, Y))  because [31], by definition 
  31] forsome*(F, cons(X, Y)) >= or(@_{o -> o}(F, X), forsome(F, Y))  because forsome > or, [32] and [39], by (Copy) 
  32] forsome*(F, cons(X, Y)) >= @_{o -> o}(F, X)  because forsome > @_{o -> o}, [33] and [35], by (Copy) 
  33] forsome*(F, cons(X, Y)) >= F  because [34], by (Select) 
  34] F >= F  by (Meta) 
  35] forsome*(F, cons(X, Y)) >= X  because [36], by (Select) 
  36] cons(X, Y) >= X  because [37], by (Star) 
  37] cons*(X, Y) >= X  because [38], by (Select) 
  38] X >= X  by (Meta) 
  39] forsome*(F, cons(X, Y)) >= forsome(F, Y)  because forsome in Mul, [40] and [41], by (Stat) 
  40] F >= F  by (Meta) 
  41] cons(X, Y) > Y  because [42], by definition 
  42] cons*(X, Y) >= Y  because [43], by (Select) 
  43] Y >= Y  by (Meta) 

We can thus remove the following rules:

  and(false, true) => false 
  and(false, false) => false 
  or(true, true) => true 
  or(true, false) => true 
  or(false, true) => 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(true, false) >? false 
  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:

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

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

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

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

With these choices, we have:

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

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

  3] or(_|_, _|_) > _|_  because [4], by definition 
  4] or*(_|_, _|_) >= _|_  by (Bot) 

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

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

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

We can thus remove the following rules:

  or(false, 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(true, true) >? true 
  and(true, 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:

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

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

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

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

With these choices, we have:

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

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

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

  4] forall(F, cons(X, Y)) > and(@_{o -> o}(F, X), forall(F, Y))  because [5], by definition 
  5] forall*(F, cons(X, Y)) >= and(@_{o -> o}(F, X), forall(F, Y))  because forall > and, [6] and [13], by (Copy) 
  6] forall*(F, cons(X, Y)) >= @_{o -> o}(F, X)  because forall > @_{o -> o}, [7] and [9], by (Copy) 
  7] forall*(F, cons(X, Y)) >= F  because [8], by (Select) 
  8] F >= F  by (Meta) 
  9] forall*(F, cons(X, Y)) >= X  because [10], by (Select) 
  10] cons(X, Y) >= X  because [11], by (Star) 
  11] cons*(X, Y) >= X  because [12], by (Select) 
  12] X >= X  by (Meta) 
  13] forall*(F, cons(X, Y)) >= forall(F, Y)  because forall in Mul, [14] and [15], by (Stat) 
  14] F >= F  by (Meta) 
  15] cons(X, Y) > Y  because [16], by definition 
  16] cons*(X, Y) >= Y  because [17], by (Select) 
  17] Y >= Y  by (Meta) 

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

We can thus remove the following rules:

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

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

Argument functions:

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

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

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

  and(_|_, _|_) > _|_ 
  and(_|_, _|_) >= _|_ 
  forall(F, nil) >= _|_ 

With these choices, we have:

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

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

  4] forall(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(true, false) >? false 
  forall(F, nil) >? true 

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

Argument functions:

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

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

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

  and(_|_, _|_) > _|_ 
  forall(F, nil) >= _|_ 

With these choices, we have:

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

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

We can thus remove the following rules:

  and(true, 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]):

  forall(F, nil) >? true 

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

Argument functions:

  [[true]] = _|_ 

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

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

  forall(F, nil) > _|_ 

With these choices, we have:

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

We can thus remove the following rules:

  forall(F, nil) => true 

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.