(0) Obligation:
Relative term rewrite system:
The relative TRS consists of the following R rules:
t(f(x), g(y), f(z)) → t(z, g(x), g(y))
t(g(x), g(y), f(z)) → t(f(y), f(z), x)
The relative TRS consists of the following S rules:
g(g(x)) → f(f(x))
f(f(x)) → g(g(x))
g(f(x)) → f(g(x))
f(g(x)) → g(f(x))
(1) RelTRStoQDPProof (SOUND transformation)
The relative termination problem is root-restricted. We can therefore treat it as a dependency pair problem.
(2) Obligation:
Q DP problem:
The TRS P consists of the following rules:
t(f(x), g(y), f(z)) → t(z, g(x), g(y))
t(g(x), g(y), f(z)) → t(f(y), f(z), x)
The TRS R consists of the following rules:
g(g(x)) → f(f(x))
f(f(x)) → g(g(x))
g(f(x)) → f(g(x))
f(g(x)) → g(f(x))
Q is empty.
We have to consider all (P,Q,R)-chains.
(3) MRRProof (EQUIVALENT transformation)
By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:
t(f(x), g(y), f(z)) → t(z, g(x), g(y))
t(g(x), g(y), f(z)) → t(f(y), f(z), x)
Used ordering: Polynomial interpretation [POLO]:
POL(f(x1)) = 1 + 2·x1
POL(g(x1)) = 1 + 2·x1
POL(t(x1, x2, x3)) = x1 + x2 + x3
(4) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
g(g(x)) → f(f(x))
f(f(x)) → g(g(x))
g(f(x)) → f(g(x))
f(g(x)) → g(f(x))
Q is empty.
We have to consider all (P,Q,R)-chains.
(5) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(6) YES