======================================================== The given Problem was: R b -> b R R c -> L c b L -> L b a L -> a b R ======================================================== A self-embedding rewrite structure for the given SRS is: a (b)^k Lc --> a (b)^k+1 Lc (#8052) pattern overlapped by closure at r0 RP: a (b)^k L --> a (b)^k+1 R (#6118) pattern overlapped by pattern RP: a (b)^k L --> abR (b)^k (#130) pattern overlapped by closure at l-1 RP: (b)^k L --> L (b)^k (#4) self-overlapping Closure at -1 OC: b L --(1)-> L b (#3) Rule OC: a L --(1)-> a b R (#4) Rule RP: R (b)^k --> (b)^k R (#1) self-overlapping Closure at 1 OC: R b --(1)-> b R (#1) Rule OC: R c --(1)-> L c (#2) Rule Hence, the SRS is non-terminating.