(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 a a End → Wait Left b a a End
Wait Left b a a End →
Wait Left b a a Endby OverlapClosure OC 3
Wait Left b a a End → Wait Left b b a a End
by OverlapClosure OC 2Wait Left b → Wait Right1
by OverlapClosure OC 2Wait Left → Begin
by original rule (OC 1)
Begin b → Wait Right1
by original rule (OC 1)
Right1 a a End → Left b b a a End
by OverlapClosure OC 3Right1 a a End → Left b b a a c b c End
by OverlapClosure OC 3Right1 a a End → Left a b b c End
by OverlapClosure OC 3Right1 a a End → Aa Left b b c End
by OverlapClosure OC 3Right1 a a End → Aa Left b b a c End
by OverlapClosure OC 2Right1 a → Aa Right1
by original rule (OC 1)
Right1 a End → Left b b a c End
by OverlapClosure OC 3Right1 a End → Left b b a a c End
by original rule (OC 1)
a →
by original rule (OC 1)
a →
by original rule (OC 1)
Aa Left → Left a
by original rule (OC 1)
a b → b b a a c
by original rule (OC 1)
c b c →
by original rule (OC 1)
b →
by original rule (OC 1)