Term Rewriting System R:

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

Termination of R to be shown.


R contains the following Dependency Pairs: 


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

Furthermore, R contains two SCCs.


SCC1:

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

Found an infinite P-chain over R:
P = *'(x, +(y, f(z))) -> *'(g(x, z), +(y, y))
R = [*(x, +(y, f(z))) -> *(g(x, z), +(y, y)), *(+(x, y), z) -> +(*(x, z), *(y, z)), *(*(x, y), z) -> *(x, *(y, z))]
s = *'(x'', +(f(z'''), f(z''))) evaluates to t = *'(g(g(x'', z''), z'''), +(f(z'''), f(z''')))
Thus, s starts an infinite reduction as s matches t.


Non-Termination of R could be shown.

Duration: 0.540 seconds.