======================================================== The given Problem was: b a L -> L a L X b a b b b L -> L b ======================================================== A self-embedding rewrite structure for the given SRS is: ba (b)^k LaL --> LaLXba (b)^k+1 LaLXbabb (#51093) pattern overlapped by closure at r0 RP: ba (b)^k L --> LaLXba (b)^k+1 b (#3056) expand -> RP: ba (b)^k L --> LaLXba (b)^k+2 (#394) pattern overlapped by closure at l-2 RP: (b)^k L --> L (b)^k (#2) self-overlapping Closure at -1 OC: b L --(1)-> L b (#2) Rule OC: b a L --(1)-> L a L X b a b b (#1) Rule OC: b a L --(1)-> L a L X b a b b (#1) Rule Hence, the SRS is non-terminating.