Term Rewriting System R:

   [x, y]
   fac(0) -> 1
   fac(s(x)) -> *(s(x), fac(x))
   fac(0) -> s(0)
   floop(0, y) -> y
   floop(s(x), y) -> floop(x, *(s(x), y))
   *(x, 0) -> 0
   *(x, s(y)) -> +(*(x, y), x)
   +(x, 0) -> x
   +(x, s(y)) -> s(+(x, y))
   1 -> s(0)

Termination of R to be shown.


R contains the following Dependency Pairs: 


   FAC(s(x)) -> *'(s(x), fac(x))
   FAC(s(x)) -> FAC(x)
   FAC(0) -> 1'
   *'(x, s(y)) -> +'(*(x, y), x)
   *'(x, s(y)) -> *'(x, y)
   +'(x, s(y)) -> +'(x, y)
   FLOOP(s(x), y) -> FLOOP(x, *(s(x), y))
   FLOOP(s(x), y) -> *'(s(x), y)

Furthermore, R contains four SCCs.


SCC1:

+'(x, s(y)) -> +'(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(s(x_1)) = 1 + x_1
POL(+'(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   +'(x, s(y)) -> +'(x, y)



 This transformation is resulting in no new subcycles.


SCC2:

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

The following Dependency Pairs can be deleted:

   *'(x, s(y)) -> *'(x, y)



 This transformation is resulting in no new subcycles.


SCC3:

FAC(s(x)) -> FAC(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(s(x_1)) = 1 + x_1
POL(FAC(x_1)) = 1 + x_1

The following Dependency Pairs can be deleted:

   FAC(s(x)) -> FAC(x)



 This transformation is resulting in no new subcycles.


SCC4:

FLOOP(s(x), y) -> FLOOP(x, *(s(x), y))

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

No rules need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
POL(*(x_1, x_2)) = 0
POL(s(x_1)) = 1 + x_1
POL(FLOOP(x_1, x_2)) = x_1
POL(+(x_1, x_2)) = 0
POL(0) = 0

 resulting in no subcycles.




Termination of R successfully shown.


Duration: 0.635 seconds.