Term Rewriting System R:
[X, Z, Y]
h(X, Z) -> f(X, s(X), Z)
f(X, Y, g(X, Y)) -> h(0, g(X, Y))
g(0, Y) -> 0
g(X, s(Y)) -> g(X, Y)

Termination of R to be shown. 



   R
     ↳Removing Redundant Rules



Removing the following rules from R which fullfill a polynomial ordering:

g(0, Y) -> 0

where the Polynomial interpretation:
  POL(0)=  0  
  POL(g(x1, x2))=  1 + x1 + x2  
  POL(h(x1, x2))=  2·x1 + x2  
  POL(s(x1))=  x1  
  POL(f(x1, x2, x3))=  x1 + x2 + x3  
was used.

Not all Rules of R can be deleted, so we still have to regard a part of R. 


   R
     ↳RRRPolo
       →TRS2
         ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

F(X, Y, g(X, Y)) -> H(0, g(X, Y))
G(X, s(Y)) -> G(X, Y)
H(X, Z) -> F(X, s(X), Z)

Furthermore, R contains two SCCs. 


   R
     ↳RRRPolo
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳Size-Change Principle
           →DP Problem 2
             ↳NonTerm


Dependency Pair:

G(X, s(Y)) -> G(X, Y)


Rules:


f(X, Y, g(X, Y)) -> h(0, g(X, Y))
g(X, s(Y)) -> g(X, Y)
h(X, Z) -> f(X, s(X), Z)





We number the DPs as follows:
  1. G(X, s(Y)) -> G(X, Y)
and get the following Size-Change Graph(s):
{1} , {1}
1=1
2>2

which lead(s) to this/these maximal multigraph(s):
{1} , {1}
1=1
2>2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
s(x1) -> s(x1)

We obtain no new DP problems. 


   R
     ↳RRRPolo
       →TRS2
         ↳DPs
           →DP Problem 1
             ↳SCP
           →DP Problem 2
             ↳Non Termination


Dependency Pairs:

H(X, Z) -> F(X, s(X), Z)
F(X, Y, g(X, Y)) -> H(0, g(X, Y))


Rules:


f(X, Y, g(X, Y)) -> h(0, g(X, Y))
g(X, s(Y)) -> g(X, Y)
h(X, Z) -> f(X, s(X), Z)





Found an infinite P-chain over R:
P =

H(X, Z) -> F(X, s(X), Z)
F(X, Y, g(X, Y)) -> H(0, g(X, Y))

R =

f(X, Y, g(X, Y)) -> h(0, g(X, Y))
g(X, s(Y)) -> g(X, Y)
h(X, Z) -> f(X, s(X), Z)

s = F(0, s(0), g(0, s(0)))
evaluates to t =F(0, s(0), g(0, s(0)))

Thus, s starts an infinite chain.

Non-Termination of R could be shown.
Duration:
0:00 minutes