Term Rewriting System R:

   [x, y, z]
   f(x, nil) -> g(nil, x)
   f(x, g(y, z)) -> g(f(x, y), z)
   ++(x, nil) -> x
   ++(x, g(y, z)) -> g(++(x, y), z)
   null(nil) -> true
   null(g(x, y)) -> false
   mem(nil, y) -> false
   mem(g(x, y), z) -> or(=(y, z), mem(x, z))
   mem(x, max(x)) -> not(null(x))
   max(g(g(nil, x), y)) -> max'(x, y)
   max(g(g(g(x, y), z), u)) -> max'(max(g(g(x, y), z)), u)

Termination of R to be shown.


R contains the following Dependency Pairs: 


   MEM(g(x, y), z) -> MEM(x, z)
   MEM(x, max(x)) -> NULL(x)
   ++'(x, g(y, z)) -> ++'(x, y)
   MAX(g(g(g(x, y), z), u)) -> MAX(g(g(x, y), z))
   F(x, g(y, z)) -> F(x, y)

Furthermore, R contains four SCCs.


SCC1:

MEM(g(x, y), z) -> MEM(x, z)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(g(x_1, x_2)) = 1 + x_1 + x_2
POL(MEM(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   MEM(g(x, y), z) -> MEM(x, z)



 This transformation is resulting in no new subcycles.


SCC2:

++'(x, g(y, z)) -> ++'(x, y)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(++'(x_1, x_2)) = 1 + x_1 + x_2
POL(g(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   ++'(x, g(y, z)) -> ++'(x, y)



 This transformation is resulting in no new subcycles.


SCC3:

MAX(g(g(g(x, y), z), u)) -> MAX(g(g(x, y), z))

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(g(x_1, x_2)) = 1 + x_1 + x_2
POL(MAX(x_1)) = 1 + x_1
POL(u) = 1

The following Dependency Pairs can be deleted:

   MAX(g(g(g(x, y), z), u)) -> MAX(g(g(x, y), z))



 This transformation is resulting in no new subcycles.


SCC4:

F(x, g(y, z)) -> F(x, y)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(g(x_1, x_2)) = 1 + x_1 + x_2
POL(F(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   F(x, g(y, z)) -> F(x, y)



 This transformation is resulting in no new subcycles.




Termination of R successfully shown.


Duration: 0.759 seconds.