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