a(b(a(b(

TRS

↳Dependency Pair Analysis

A(b(a(b(x)))) -> A(b(a(a(b(x)))))

A(b(a(b(x)))) -> A(a(b(x)))

Furthermore,

TRS

↳DPs

→DP Problem 1

↳Non Termination

**A(b(a(b( x)))) -> A(a(b(x)))**

a(b(a(b(x)))) -> b(a(b(a(a(b(x))))))

Found an infinite P-chain over R:

P =

A(b(a(b(x)))) -> A(a(b(x)))

A(b(a(b(x)))) -> A(b(a(a(b(x)))))

R =

a(b(a(b(x)))) -> b(a(b(a(a(b(x))))))

s = A(b(a(a(b(a(b(

evaluates to t =A(b(a(a(b(a(b(a(a(b(

Thus, s starts an infinite chain as s matches t.

Duration:

0:01 minutes