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