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