(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 0 1 0 0 1 End → Begin 0 1 0 0 1 End
Begin 0 1 0 0 1 End →
Begin 0 1 0 0 1 Endby OverlapClosure OC 3
Begin 0 1 0 0 1 End → Wait Left 0 1 0 0 1 End
by OverlapClosure OC 3Begin 0 1 0 0 1 End → Wait Left 1 0 1 0 1 End
by OverlapClosure OC 3Begin 0 1 0 0 1 End → Wait A1 Left 0 1 0 1 End
by OverlapClosure OC 2Begin 0 1 0 0 1 End → Wait A1 Right2 0 0 End
by OverlapClosure OC 3Begin 0 1 0 0 1 End → Wait Right2 1 0 0 End
by OverlapClosure OC 3Begin 0 1 0 0 1 End → Begin 0 0 1 0 0 End
by OverlapClosure OC 3Begin 0 1 0 0 1 End → Wait Left 0 0 1 0 0 End
by OverlapClosure OC 2Begin 0 1 0 → Wait Right4
by original rule (OC 1)
Right4 0 1 End → Left 0 0 1 0 0 End
by OverlapClosure OC 3Right4 0 1 End → A0 Left 0 1 0 0 End
by OverlapClosure OC 2Right4 0 → A0 Right4
by original rule (OC 1)
Right4 1 End → Left 0 1 0 0 End
by original rule (OC 1)
A0 Left → Left 0
by original rule (OC 1)
Wait Left → Begin
by original rule (OC 1)
Begin 0 0 → Wait Right2
by original rule (OC 1)
Right2 1 → A1 Right2
by original rule (OC 1)
Right2 0 0 End → Left 0 1 0 1 End
by original rule (OC 1)
A1 Left → Left 1
by original rule (OC 1)
1 0 1 0 → 0 1 0 0
by original rule (OC 1)
Wait Left → Begin
by original rule (OC 1)