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