(0) Obligation:
Relative term rewrite system:
The relative TRS consists of the following R rules:
b(a(x)) → a(b(x))
The relative TRS consists of the following S rules:
b(x) → b(b(x))
a(x) → a(a(x))
(1) RelTRS Reverse (EQUIVALENT transformation)
We have reversed the following relative TRS [REVERSE]:
The set of rules R is
b(a(x)) → a(b(x))
The set of rules S is
b(x) → b(b(x))
a(x) → a(a(x))
We have obtained the following relative TRS:
The set of rules R is
a(b(x)) → b(a(x))
The set of rules S is
b(x) → b(b(x))
a(x) → a(a(x))
(2) Obligation:
Relative term rewrite system:
The relative TRS consists of the following R rules:
a(b(x)) → b(a(x))
The relative TRS consists of the following S rules:
b(x) → b(b(x))
a(x) → a(a(x))
(3) RelTRSLoopFinderProof (COMPLETE transformation)
The following loop was found:
---------- Loop: ----------
a(b(x')) → a(b(b(x'))) with rule b(x'') → b(b(x'')) at position [0] and matcher [x'' / x']
a(b(b(x'))) → b(a(b(x'))) with rule a(b(x)) → b(a(x)) at position [] and matcher [x / b(x')]
Now an instance of the first term with Matcher [ ] occurs in the last term at position [0].
Context: b([])
Therefore, the relative TRS problem does not terminate.
(4) NO