(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) RelTRSLoopFinderProof (COMPLETE transformation)
The following loop was found:
---------- Loop: ----------
b(a(x')) → b(a(a(x'))) with rule a(x'') → a(a(x'')) at position [0] and matcher [x'' / x']
b(a(a(x'))) → a(b(a(x'))) with rule b(a(x)) → a(b(x)) at position [] and matcher [x / a(x')]
Now an instance of the first term with Matcher [ ] occurs in the last term at position [0].
Context: a([])
Therefore, the relative TRS problem does not terminate.
(2) NO