Term Rewriting System R:

   [x, y]
   minus(minus(x)) -> x
   minus(+(x, y)) -> *(minus(minus(minus(x))), minus(minus(minus(y))))
   minus(*(x, y)) -> +(minus(minus(minus(x))), minus(minus(minus(y))))
   f(minus(x)) -> minus(minus(minus(f(x))))

Termination of R to be shown.


R contains the following Dependency Pairs: 


   MINUS(+(x, y)) -> MINUS(minus(minus(x)))
   MINUS(+(x, y)) -> MINUS(minus(x))
   MINUS(+(x, y)) -> MINUS(x)
   MINUS(+(x, y)) -> MINUS(minus(minus(y)))
   MINUS(+(x, y)) -> MINUS(minus(y))
   MINUS(+(x, y)) -> MINUS(y)
   MINUS(*(x, y)) -> MINUS(minus(minus(x)))
   MINUS(*(x, y)) -> MINUS(minus(x))
   MINUS(*(x, y)) -> MINUS(x)
   MINUS(*(x, y)) -> MINUS(minus(minus(y)))
   MINUS(*(x, y)) -> MINUS(minus(y))
   MINUS(*(x, y)) -> MINUS(y)
   F(minus(x)) -> MINUS(minus(minus(f(x))))
   F(minus(x)) -> MINUS(minus(f(x)))
   F(minus(x)) -> MINUS(f(x))
   F(minus(x)) -> F(x)

Furthermore, R contains two SCCs.


SCC1:

MINUS(*(x, y)) -> MINUS(y)
MINUS(*(x, y)) -> MINUS(minus(y))
MINUS(*(x, y)) -> MINUS(minus(minus(y)))
MINUS(*(x, y)) -> MINUS(x)
MINUS(*(x, y)) -> MINUS(minus(x))
MINUS(*(x, y)) -> MINUS(minus(minus(x)))
MINUS(+(x, y)) -> MINUS(y)
MINUS(+(x, y)) -> MINUS(minus(y))
MINUS(+(x, y)) -> MINUS(minus(minus(y)))
MINUS(+(x, y)) -> MINUS(x)
MINUS(+(x, y)) -> MINUS(minus(x))
MINUS(+(x, y)) -> MINUS(minus(minus(x)))

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)) = x_1 + x_2
POL(minus(x_1)) = x_1
POL(MINUS(x_1)) = 1 + x_1
POL(+(x_1, x_2)) = x_1 + x_2

No Dependency Pairs can be deleted.

The following rules of R can be deleted: 

   f(minus(x)) -> minus(minus(minus(f(x))))


 This transformation is resulting in one new subcycle:


SCC1.MRR1:

MINUS(*(x, y)) -> MINUS(minus(y))
MINUS(*(x, y)) -> MINUS(minus(minus(y)))
MINUS(*(x, y)) -> MINUS(x)
MINUS(*(x, y)) -> MINUS(minus(x))
MINUS(*(x, y)) -> MINUS(minus(minus(x)))
MINUS(+(x, y)) -> MINUS(y)
MINUS(+(x, y)) -> MINUS(minus(y))
MINUS(+(x, y)) -> MINUS(minus(minus(y)))
MINUS(+(x, y)) -> MINUS(x)
MINUS(+(x, y)) -> MINUS(minus(x))
MINUS(+(x, y)) -> MINUS(minus(minus(x)))
MINUS(*(x, y)) -> MINUS(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(minus(x_1)) = x_1
POL(MINUS(x_1)) = x_1
POL(+(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   MINUS(*(x, y)) -> MINUS(minus(y))
   MINUS(*(x, y)) -> MINUS(minus(minus(y)))
   MINUS(*(x, y)) -> MINUS(x)
   MINUS(*(x, y)) -> MINUS(minus(x))
   MINUS(*(x, y)) -> MINUS(minus(minus(x)))
   MINUS(+(x, y)) -> MINUS(y)
   MINUS(+(x, y)) -> MINUS(minus(y))
   MINUS(+(x, y)) -> MINUS(minus(minus(y)))
   MINUS(+(x, y)) -> MINUS(x)
   MINUS(+(x, y)) -> MINUS(minus(x))
   MINUS(+(x, y)) -> MINUS(minus(minus(x)))
   MINUS(*(x, y)) -> MINUS(y)



 This transformation is resulting in no new subcycles.


SCC2:

F(minus(x)) -> F(x)

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(minus(x_1)) = 1 + x_1
POL(F(x_1)) = 1 + x_1

The following Dependency Pairs can be deleted:

   F(minus(x)) -> F(x)



 This transformation is resulting in no new subcycles.




Termination of R successfully shown.


Duration: 2.501 seconds.