(1) NonTerminationProof (COMPLETE transformation)
We used the non-termination processor [OPPELT08] to show that the SRS problem is infinite.
Found the self-embedding DerivationStructure:
Begin b a c End → Begin b a c End
Begin b a c End →
Begin b a c Endby OverlapClosure OC 3
Begin b a c End → Wait Left b a c End
by OverlapClosure OC 2Begin b → Wait Right3
by original rule (OC 1)
Right3 a c End → Left b a c End
by OverlapClosure OC 3Right3 a c End → Left a a End
by OverlapClosure OC 3Right3 a c End → Aa Left a End
by OverlapClosure OC 2Right3 a → Aa Right3
by original rule (OC 1)
Right3 c End → Left a End
by original rule (OC 1)
Aa Left → Left a
by original rule (OC 1)
a a → b a c
by original rule (OC 1)
Wait Left → Begin
by original rule (OC 1)