Term Rewriting System R:

   [X, Y]
   *(X, +(Y, 1)) -> +(*(X, +(Y, *(1, 0))), X)
   *(X, 1) -> X
   *(X, 0) -> X
   *(X, 0) -> 0

Innermost Termination of R to be shown.


R contains the following Dependency Pairs: 


   *'(X, +(Y, 1)) -> *'(X, +(Y, *(1, 0)))
   *'(X, +(Y, 1)) -> *'(1, 0)

Furthermore, R contains one SCC.


SCC1:

*'(X, +(Y, 1)) -> *'(X, +(Y, *(1, 0)))

Found an infinite P-chain over R:
P = *'(X, +(Y, 1)) -> *'(X, +(Y, *(1, 0)))
R = [*(X, +(Y, 1)) -> +(*(X, +(Y, *(1, 0))), X), *(X, 1) -> X, *(X, 0) -> 0, *(X, 0) -> X]
s = *'(X', +(Y', 1)) evaluates to t = *'(X', +(Y', 1))
Thus, s starts an infinite reduction.


Innermost Non-Termination of R could be shown.

Duration: 0.528 seconds.