Term Rewriting System R:
[x, y, z]
f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))

Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

F(x, g(y)) -> F(h(x), i(x, y))
F(x, g(y)) -> I(x, y)
I(x, j(y, z)) -> J(g(y), i(x, z))
I(x, j(y, z)) -> I(x, z)
I(h(x), j(j(y, z), 0)) -> J(i(h(x), j(y, z)), i(x, j(y, z)))
I(h(x), j(j(y, z), 0)) -> I(h(x), j(y, z))
I(h(x), j(j(y, z), 0)) -> I(x, j(y, z))
J(g(x), g(y)) -> J(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:

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


Rules:


f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))





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

I(h(x), j(j(y, z), 0)) -> I(x, j(y, z))
I(h(x), j(j(y, z), 0)) -> I(h(x), j(y, z))
I(x, j(y, z)) -> I(x, z)


Rules:


f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))





We have the following set of usable rules:

j(g(x), g(y)) -> g(j(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(I(x1, x2))=  1 + x1 + x2  
  POL(0)=  0  
  POL(g(x1))=  x1  
  POL(h(x1))=  1 + x1  
  POL(j(x1, x2))=  x1 + x2  

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

I(h(x), j(j(y, z), 0)) -> I(x, j(y, z))
I(h(x), j(j(y, z), 0)) -> I(h(x), j(y, z))

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:

I(x, j(y, z)) -> I(x, z)


Rule:


j(g(x), g(y)) -> g(j(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(I(x1, x2))=  x1 + x2  
  POL(j(x1, x2))=  x1 + x2  

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

I(x, j(y, z)) -> I(x, z)

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:

F(x, g(y)) -> F(h(x), i(x, y))


Rules:


f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))





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

F(x, g(y)) -> F(h(x), i(x, y))
one new Dependency Pair is created:

F(h(x''''), g(y')) -> F(h(h(x'''')), i(h(x''''), y'))

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:

F(h(x''''), g(y')) -> F(h(h(x'''')), i(h(x''''), y'))


Rules:


f(x, g(y)) -> f(h(x), i(x, y))
i(x, j(0, 0)) -> g(0)
i(x, j(y, z)) -> j(g(y), i(x, z))
i(h(x), j(j(y, z), 0)) -> j(i(h(x), j(y, z)), i(x, j(y, z)))
j(g(x), g(y)) -> g(j(x, y))




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