Term Rewriting System R:
[x]
a(b(x)) -> b(b(a(a(x))))
Termination of R to be shown.
TRS
↳Reversing
↳Rev
↳DPs
Rule(s) before reversing:
a(b(x)) -> b(b(a(a(x))))
Rule(s) after reversing:
b'(a'(x)) -> a'(a'(b'(b'(x))))
Trying another alternative:
TRS
↳Rev
↳Reversing
↳DPs
Rule(s) before reversing:
a(b(x)) -> b(b(a(a(x))))
Rule(s) after reversing:
b'(a'(x)) -> a'(a'(b'(b'(x))))
Trying another alternative:
TRS
↳Rev
↳Rev
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
A(b(x)) -> A(a(x))
A(b(x)) -> A(x)
Furthermore, R contains one SCC.
TRS
↳Rev
↳Rev
↳DPs
→DP Problem 1
↳Non Termination
Dependency Pairs:
A(b(x)) -> A(x)
A(b(x)) -> A(a(x))
Rule:
a(b(x)) -> b(b(a(a(x))))
Found an infinite P-chain over R:
P =
A(b(x)) -> A(x)
A(b(x)) -> A(a(x))
R =
a(b(x)) -> b(b(a(a(x))))
s = A(a(b(x'')))
evaluates to t =A(a(b(a(a(x'')))))
Thus, s starts an infinite chain as s matches t.
Non-Termination of R could be shown.
Duration:
0:00 minutes