(0) Obligation:
Relative term rewrite system:
The relative TRS consists of the following R rules:
f(f(x)) → x
The relative TRS consists of the following S rules:
f(x) → g(f(g(f(x))))
(1) RelTRS Reverse (EQUIVALENT transformation)
We have reversed the following relative TRS [REVERSE]:
The set of rules R is
f(f(x)) → x
The set of rules S is
f(x) → g(f(g(f(x))))
We have obtained the following relative TRS:
The set of rules R is
f(f(x)) → x
The set of rules S is
f(x) → f(g(f(g(x))))
(2) Obligation:
Relative term rewrite system:
The relative TRS consists of the following R rules:
f(f(x)) → x
The relative TRS consists of the following S rules:
f(x) → f(g(f(g(x))))
(3) FlatCCProof (EQUIVALENT transformation)
We used flat context closure [ROOTLAB]
(4) Obligation:
Relative term rewrite system:
The relative TRS consists of the following R rules:
f(f(f(x))) → f(x)
g(f(f(x))) → g(x)
The relative TRS consists of the following S rules:
f(x) → f(g(f(g(x))))
(5) RootLabelingProof (EQUIVALENT transformation)
We used plain root labeling [ROOTLAB] with the following heuristic:
LabelAll: All function symbols get labeled
(6) Obligation:
Relative term rewrite system:
The relative TRS consists of the following R rules:
f_{f_1}(f_{f_1}(f_{f_1}(x))) → f_{f_1}(x)
f_{f_1}(f_{f_1}(f_{g_1}(x))) → f_{g_1}(x)
g_{f_1}(f_{f_1}(f_{f_1}(x))) → g_{f_1}(x)
g_{f_1}(f_{f_1}(f_{g_1}(x))) → g_{g_1}(x)
The relative TRS consists of the following S rules:
f_{f_1}(x) → f_{g_1}(g_{f_1}(f_{g_1}(g_{f_1}(x))))
f_{g_1}(x) → f_{g_1}(g_{f_1}(f_{g_1}(g_{g_1}(x))))
(7) RelTRSRRRProof (EQUIVALENT transformation)
We used the following monotonic ordering for rule removal:
Polynomial interpretation [POLO]:
POL(f_{f_1}(x1)) = 1 + x1
POL(f_{g_1}(x1)) = x1
POL(g_{f_1}(x1)) = x1
POL(g_{g_1}(x1)) = x1
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:
f_{f_1}(f_{f_1}(f_{f_1}(x))) → f_{f_1}(x)
f_{f_1}(f_{f_1}(f_{g_1}(x))) → f_{g_1}(x)
g_{f_1}(f_{f_1}(f_{f_1}(x))) → g_{f_1}(x)
g_{f_1}(f_{f_1}(f_{g_1}(x))) → g_{g_1}(x)
Rules from S:
f_{f_1}(x) → f_{g_1}(g_{f_1}(f_{g_1}(g_{f_1}(x))))
(8) Obligation:
Relative term rewrite system:
R is empty.
The relative TRS consists of the following S rules:
f_{g_1}(x) → f_{g_1}(g_{f_1}(f_{g_1}(g_{g_1}(x))))
(9) RIsEmptyProof (EQUIVALENT transformation)
The TRS R is empty. Hence, termination is trivially proven.
(10) YES