========================================================
The given Problem was:
a l -> l a
r a -> a r
b l -> b a r
r b -> l b
========================================================
A self-embedding rewrite structure for the given SRS is:
b (a)^k lb --> b (a)^k+1 lb (#9734)
pattern overlapped by closure at r0
RP: b (a)^k l --> b (a)^k+1 r (#7233)
pattern overlapped by pattern
RP: b (a)^k l --> bar (a)^k (#130)
pattern overlapped by closure at l-1
RP: (a)^k l --> l (a)^k (#2)
self-overlapping Closure at -1
OC: a l --(1)-> l a (#1)
Rule
OC: b l --(1)-> b a r (#3)
Rule
RP: r (a)^k --> (a)^k r (#3)
self-overlapping Closure at 1
OC: r a --(1)-> a r (#2)
Rule
OC: r b --(1)-> l b (#4)
Rule
Hence, the SRS is non-terminating.