(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
a(a(x1)) → a(b(x1))
b(b(c(x1))) → c(c(a(a(a(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:
a(a(x)) → b(a(x))
c(b(b(x))) → a(a(a(c(c(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 b b b b b b b b → a a a c b b b b b b b b a c c a c c a a c c a c c
c b b b b b b b b →
a a a c b b b b b b b b a c c a c c a a c c a c cby OverlapClosure OC 2
c b b → a a a c c
by original rule (OC 1)
c b b b b b b → b b b b b b b b a c c a c c a a c c a c c
by OverlapClosure OC 3c b b b b b b → b b b b b b b a a c c a c c a a c c a c c
by OverlapClosure OC 3c b b b b b b → b b b b b b a a a c c a c c a a c c a c c
by OverlapClosure OC 3c b b b b b b → b b b b b a a a a c c a c c a a c c a c c
by OverlapClosure OC 3c b b b b b b → b b b b b a c b b a c c a a c c a c c
by OverlapClosure OC 3c b b b b b b → b b b b b a c b a a c c a a c c a c c
by OverlapClosure OC 3c b b b b b b → b b b b b a c a a a c c a a c c a c c
by OverlapClosure OC 3c b b b b b b → b b b b b a c c b b a a c c a c c
by OverlapClosure OC 3c b b b b b b → b b b b b a c c b a a a c c a c c
by OverlapClosure OC 3c b b b b b b → b b b b b a c c a a a a c c a c c
by OverlapClosure OC 3c b b b b b b → b b b b b a c c a c b b a c c
by OverlapClosure OC 2c b b b b → b b b b b a c c a c c
by OverlapClosure OC 3c b b b b → b b b b a a c c a c c
by OverlapClosure OC 3c b b b b → b b b a a a c c a c c
by OverlapClosure OC 3c b b b b → b b a a a a c c a c c
by OverlapClosure OC 3c b b b b → b b a c b b a c c
by OverlapClosure OC 2c b b → b b a c c
by OverlapClosure OC 3c b b → b a a c c
by OverlapClosure OC 3c b b → a a a c c
by original rule (OC 1)
a a → b a
by original rule (OC 1)
a a → b a
by original rule (OC 1)
c b b → b b a c c
by OverlapClosure OC 3c b b → b a a c c
by OverlapClosure OC 3c b b → a a a c c
by original rule (OC 1)
a a → b a
by original rule (OC 1)
a a → b a
by original rule (OC 1)
c b b → a a a c c
by original rule (OC 1)
a a → b a
by original rule (OC 1)
a a → b a
by original rule (OC 1)
a a → b a
by original rule (OC 1)
c b b → b b a c c
by OverlapClosure OC 3c b b → b a a c c
by OverlapClosure OC 3c b b → a a a c c
by original rule (OC 1)
a a → b a
by original rule (OC 1)
a a → b a
by original rule (OC 1)
c b b → a a a c c
by original rule (OC 1)
a a → b a
by original rule (OC 1)
a a → b a
by original rule (OC 1)
c b b → a a a c c
by original rule (OC 1)
a a → b a
by original rule (OC 1)
a a → b a
by original rule (OC 1)
c b b → a a a c c
by original rule (OC 1)
a a → b a
by original rule (OC 1)
a a → b a
by original rule (OC 1)
a a → b a
by original rule (OC 1)
(4) NO