(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 (b)k L c → a (b)k+1 L c
a (
b)
k L c →
a (
b)
k+1 L cby Overlap u with r (ol3)
a (b)k L → a (b)k+1 R
by Overlapping Derivationstructuresa (b)k L → a b R (b)k
by Overlap u with l (ol4)(b)k L → L (b)k
by Selfoverlapping OC am1b L → L b
by original rule (OC 1)
a L → a b R
by original rule (OC 1)
R (b)k → (b)k R
by Selfoverlapping OC am2R b → b R
by original rule (OC 1)
R c → L c
by original rule (OC 1)