(1) NonTerminationProof (EQUIVALENT transformation)
We used the non-termination processor [OPPELT08] to show that the SRS problem is infinite.
Found the self-embedding DerivationStructure:
a a b b a b b b b b b a b b b → b b b b b b b b b a a b b a b b b b b b a b b b a a a
a a b b a b b b b b b a b b b →
b b b b b b b b b a a b b a b b b b b b a b b b a a aby OverlapClosure OC 2
a a b b a b b b b b b a b b → b b b b b b b b b a a b b a b b b b b b a a a b
by OverlapClosure OC 3a a b b a b b b b b b a b b → b b b b b b b b b a a b b a b b b a a b b b
by OverlapClosure OC 2a a b b a b b b b b b → b b b b b b b b b a a b b a b b b a a a
by OverlapClosure OC 2a a b b a b b b b → b b b b b b b b b a a b b a a a
by OverlapClosure OC 3a a b b a b b b b → b b b b b b a a b b b b a a a
by OverlapClosure OC 3a a b b a b b b b → b b b b b b a a a b b b b a a a
by OverlapClosure OC 2a a b b a b b → b b b b b b a a a b a a
by OverlapClosure OC 3a a b b a b b → b b b a a b b b a a
by OverlapClosure OC 2a a b b → b b b a a a
by original rule (OC 1)
a a b b → b b b a a
by OverlapClosure OC 2a a b b → b b b a a a
by original rule (OC 1)
a →
by original rule (OC 1)
a a b b → b b b a a a
by original rule (OC 1)
a a b b → b b b a a a
by original rule (OC 1)
a →
by original rule (OC 1)
a a b b → b b b a a
by OverlapClosure OC 2a a b b → b b b a a a
by original rule (OC 1)
a →
by original rule (OC 1)
a a b b → b b b a a a
by original rule (OC 1)
a a b b → b b b
by OverlapClosure OC 2a a b b → b b b a
by OverlapClosure OC 2a a b b → b b b a a
by OverlapClosure OC 2a a b b → b b b a a a
by original rule (OC 1)
a →
by original rule (OC 1)
a →
by original rule (OC 1)
a →
by original rule (OC 1)
a a b b → b b b a a a
by original rule (OC 1)
a a b b → b b b a a a
by original rule (OC 1)