Term Rewriting System R:
[z, x, y]
h(z, e(x)) -> h(c(z), d(z, x))
d(z, g(0, 0)) -> e(0)
d(z, g(x, y)) -> g(e(x), d(z, y))
d(c(z), g(g(x, y), 0)) -> g(d(c(z), g(x, y)), d(z, g(x, y)))
g(e(x), e(y)) -> e(g(x, y))

Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

H(z, e(x)) -> H(c(z), d(z, x))
H(z, e(x)) -> D(z, x)
D(z, g(x, y)) -> G(e(x), d(z, y))
D(z, g(x, y)) -> D(z, y)
D(c(z), g(g(x, y), 0)) -> G(d(c(z), g(x, y)), d(z, g(x, y)))
D(c(z), g(g(x, y), 0)) -> D(c(z), g(x, y))
D(c(z), g(g(x, y), 0)) -> D(z, g(x, y))
G(e(x), e(y)) -> G(x, y)

Furthermore, R contains three SCCs. 


   R
     ↳DPs
       →DP Problem 1
         ↳Size-Change Principle
       →DP Problem 2
         ↳MRR
       →DP Problem 3
         ↳Inst


Dependency Pair:

G(e(x), e(y)) -> G(x, y)


Rules:


h(z, e(x)) -> h(c(z), d(z, x))
d(z, g(0, 0)) -> e(0)
d(z, g(x, y)) -> g(e(x), d(z, y))
d(c(z), g(g(x, y), 0)) -> g(d(c(z), g(x, y)), d(z, g(x, y)))
g(e(x), e(y)) -> e(g(x, y))





We number the DPs as follows:
  1. G(e(x), e(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:
e(x1) -> e(x1)

We obtain no new DP problems. 


   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳Modular Removal of Rules
       →DP Problem 3
         ↳Inst


Dependency Pairs:

D(c(z), g(g(x, y), 0)) -> D(z, g(x, y))
D(c(z), g(g(x, y), 0)) -> D(c(z), g(x, y))
D(z, g(x, y)) -> D(z, y)


Rules:


h(z, e(x)) -> h(c(z), d(z, x))
d(z, g(0, 0)) -> e(0)
d(z, g(x, y)) -> g(e(x), d(z, y))
d(c(z), g(g(x, y), 0)) -> g(d(c(z), g(x, y)), d(z, g(x, y)))
g(e(x), e(y)) -> e(g(x, y))





We have the following set of usable rules:

g(e(x), e(y)) -> e(g(x, y))
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(c(x1))=  1 + x1  
  POL(0)=  0  
  POL(g(x1, x2))=  x1 + x2  
  POL(e(x1))=  x1  
  POL(D(x1, x2))=  1 + x1 + x2  

We have the following set D of usable symbols: {c, g, e, D}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:

D(c(z), g(g(x, y), 0)) -> D(z, g(x, y))
D(c(z), g(g(x, y), 0)) -> D(c(z), g(x, y))

4 non usable rules have been deleted.

The result of this processor delivers one new DP problem.



   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳MRR
           →DP Problem 4
             ↳Modular Removal of Rules
       →DP Problem 3
         ↳Inst


Dependency Pair:

D(z, g(x, y)) -> D(z, y)


Rule:


g(e(x), e(y)) -> e(g(x, y))





We have the following set of usable rules: none
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(g(x1, x2))=  x1 + x2  
  POL(D(x1, x2))=  x1 + x2  

We have the following set D of usable symbols: {D}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:

D(z, g(x, y)) -> D(z, y)

No Rules can be deleted.

After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved. 



   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳MRR
       →DP Problem 3
         ↳Instantiation Transformation


Dependency Pair:

H(z, e(x)) -> H(c(z), d(z, x))


Rules:


h(z, e(x)) -> h(c(z), d(z, x))
d(z, g(0, 0)) -> e(0)
d(z, g(x, y)) -> g(e(x), d(z, y))
d(c(z), g(g(x, y), 0)) -> g(d(c(z), g(x, y)), d(z, g(x, y)))
g(e(x), e(y)) -> e(g(x, y))





On this DP problem, an Instantiation SCC transformation can be performed.
As a result of transforming the rule

H(z, e(x)) -> H(c(z), d(z, x))
one new Dependency Pair is created:

H(c(z''), e(x')) -> H(c(c(z'')), d(c(z''), x'))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳MRR
       →DP Problem 3
         ↳Inst
           →DP Problem 5
             ↳Remaining Obligation(s)




The following remains to be proven:
Dependency Pair:

H(c(z''), e(x')) -> H(c(c(z'')), d(c(z''), x'))


Rules:


h(z, e(x)) -> h(c(z), d(z, x))
d(z, g(0, 0)) -> e(0)
d(z, g(x, y)) -> g(e(x), d(z, y))
d(c(z), g(g(x, y), 0)) -> g(d(c(z), g(x, y)), d(z, g(x, y)))
g(e(x), e(y)) -> e(g(x, y))




The Proof could not be continued due to a Timeout.
Termination of R could not be shown.
Duration:
1:00 minutes