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