Term Rewriting System R:
[x]
f(a, h(x)) -> f(g(x), h(x))
h(g(x)) -> h(a)
h(h(x)) -> x
g(h(x)) -> g(x)

Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

F(a, h(x)) -> F(g(x), h(x))
F(a, h(x)) -> G(x)
H(g(x)) -> H(a)
G(h(x)) -> G(x)

Furthermore, R contains two SCCs.


   R
DPs
       →DP Problem 1
Size-Change Principle
       →DP Problem 2
Neg POLO


Dependency Pair:

G(h(x)) -> G(x)


Rules:


f(a, h(x)) -> f(g(x), h(x))
h(g(x)) -> h(a)
h(h(x)) -> x
g(h(x)) -> g(x)





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

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

DP: empty set
Oriented Rules: none

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

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

We obtain no new DP problems.


   R
DPs
       →DP Problem 1
SCP
       →DP Problem 2
Negative Polynomial Order


Dependency Pair:

F(a, h(x)) -> F(g(x), h(x))


Rules:


f(a, h(x)) -> f(g(x), h(x))
h(g(x)) -> h(a)
h(h(x)) -> x
g(h(x)) -> g(x)





The following Dependency Pair can be strictly oriented using the given order.

F(a, h(x)) -> F(g(x), h(x))


Moreover, the following usable rules (regarding the implicit AFS) are oriented.

g(h(x)) -> g(x)


Used ordering:
Polynomial Order with Interpretation:

POL( F(x1, x2) ) = x1

POL( a ) = 1

POL( g(x1) ) = 0


This results in one new DP problem.


   R
DPs
       →DP Problem 1
SCP
       →DP Problem 2
Neg POLO
           →DP Problem 3
Dependency Graph


Dependency Pair:


Rules:


f(a, h(x)) -> f(g(x), h(x))
h(g(x)) -> h(a)
h(h(x)) -> x
g(h(x)) -> g(x)





Using the Dependency Graph resulted in no new DP problems.

Termination of R successfully shown.
Duration:
0:06 minutes