(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
a(a(b(x1))) → a(c(c(a(a(a(x1))))))
a(c(x1)) → b(x1)
Q is empty.
(1) QTRS Reverse (EQUIVALENT transformation)
We applied the QTRS Reverse Processor [REVERSE].
(2) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
b(a(a(x))) → a(a(a(c(c(a(x))))))
c(a(x)) → b(x)
Q is empty.
(3) NonTerminationProof (EQUIVALENT transformation)
We used the non-termination processor [OPPELT08] to show that the SRS problem is infinite.
Found the self-embedding DerivationStructure:
c a a a a a a a a a → a a a c a a a a a a a a a c c a c b a c b c b
c a a a a a a a a a →
a a a c a a a a a a a a a c c a c b a c b c bby OverlapClosure OC 3
c a a a a a a a a a → a a a c a a a a a a b a a c b a c b c b
by OverlapClosure OC 2c a a a → a a a c b
by OverlapClosure OC 2c a a a → a a a c c a
by OverlapClosure OC 2c a → b
by original rule (OC 1)
b a a → a a a c c a
by original rule (OC 1)
c a → b
by original rule (OC 1)
b a a a a a a → a a a a a a b a a c b a c b c b
by OverlapClosure OC 3b a a a a a a → a a a b a a a a a c b c b
by OverlapClosure OC 3b a a a a a a → a a a c a a a a a a c b c b
by OverlapClosure OC 2b a a → a a a c b
by OverlapClosure OC 2b a a → a a a c c a
by original rule (OC 1)
c a → b
by original rule (OC 1)
b a a a a → a a a a a a c b c b
by OverlapClosure OC 3b a a a a → a a a b a a c b
by OverlapClosure OC 3b a a a a → a a a c a a a c b
by OverlapClosure OC 2b a a → a a a c b
by OverlapClosure OC 2b a a → a a a c c a
by original rule (OC 1)
c a → b
by original rule (OC 1)
b a a → a a a c b
by OverlapClosure OC 2b a a → a a a c c a
by original rule (OC 1)
c a → b
by original rule (OC 1)
c a → b
by original rule (OC 1)
b a a → a a a c b
by OverlapClosure OC 2b a a → a a a c c a
by original rule (OC 1)
c a → b
by original rule (OC 1)
c a → b
by original rule (OC 1)
b a a a a → a a a b a a c b
by OverlapClosure OC 3b a a a a → a a a c a a a c b
by OverlapClosure OC 2b a a → a a a c b
by OverlapClosure OC 2b a a → a a a c c a
by original rule (OC 1)
c a → b
by original rule (OC 1)
b a a → a a a c b
by OverlapClosure OC 2b a a → a a a c c a
by original rule (OC 1)
c a → b
by original rule (OC 1)
c a → b
by original rule (OC 1)
b a a → a a a c c a
by original rule (OC 1)
(4) NO