(1) NonTerminationProof (COMPLETE transformation)
We used the non-termination processor [OPPELT08] to show that the SRS problem is infinite.
Found the self-embedding DerivationStructure:
rotate finish2 c a end → rotate finish2 c a end
rotate finish2 c a end →
rotate finish2 c a endby OverlapClosure OC 3
rotate finish2 c a end → rotate Dc finish2 a end
by OverlapClosure OC 3rotate finish2 c a end → rotate Dc cut finish a end
by OverlapClosure OC 3rotate finish2 c a end → rotate Dc cut Ca finish end
by OverlapClosure OC 2rotate finish2 c a → rotate Dc cut Ca goright wait
by OverlapClosure OC 2rotate finish2 c a → begin a c
by OverlapClosure OC 2rotate finish2 → rewrite
by original rule (OC 1)
rewrite c a → begin a c
by original rule (OC 1)
begin a c → rotate Dc cut Ca goright wait
by OverlapClosure OC 3begin a c → rotate cut moveleft Bc Aa wait
by OverlapClosure OC 3begin a c → rotate cut Ca moveleft Bc wait
by OverlapClosure OC 2begin a → rotate cut Ca guess
by original rule (OC 1)
guess c → moveleft Bc wait
by original rule (OC 1)
Ca moveleft Bc → moveleft Bc Aa
by original rule (OC 1)
cut moveleft Bc Aa → Dc cut Ca goright
by OverlapClosure OC 2cut moveleft Bc → Dc cut goright
by original rule (OC 1)
goright Aa → Ca goright
by original rule (OC 1)
goright wait end → finish end
by original rule (OC 1)
Ca finish → finish a
by original rule (OC 1)
cut finish → finish2
by original rule (OC 1)
Dc finish2 → finish2 c
by original rule (OC 1)