Termination w.r.t. Q proof of /home/cern_httpd/provide/research/cycsrs/tpdb/TPDB-d9b80194f163/SRS_Standard/Mixed

Termination w.r.t. Q of the given QTRS could be disproven:

0 QTRS

↳1 NonTerminationProof (⇒, 1351 ms)

↳2 NO

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

a(b(c(x))) → c(b(a(x)))
a(c(x)) → a(a(d(a(x))))
d(a(b(x))) → b(a(d(x)))
d(a(c(x))) → b(c(c(x)))

Q is empty.

(1) NonTerminationProof (COMPLETE transformation)

We used the non-termination processor [OPPELT08] to show that the SRS problem is infinite.

Found the self-embedding DerivationStructure:

a (a b)^k+1 c c → a (a b)^k+2 c c

a (a b)^k+1 c c → a (a b)^k+2 c c
by Equivalent

a (a b)^k+1 c c → a a (b a)^k+1 b c c
by Overlap u with r (ol3)
a (a b)^k+1 c → a a (b a)^k+1 d a
by Overlapping Derivationstructures
a (a b)^k+1 c → a a d (a b)^k+1 a
by Equivalent
a (a b)^k+1 c → a a d a b (a b)^k a
by Overlap u with l (ol4)
(a b)^k+1 c → c b (a b)^k a
by Operation rotate
(a b)^k+1 c → c (b a)^k+1
by Operation lift
(a b)^k c → c (b a)^k
by Selfoverlapping OC am1
a b c → c b a
by original rule (OC 1)
a c → a a d a
by original rule (OC 1)
d (a b)^k+1 → (b a)^k+1 d
by Operation lift
d (a b)^k → (b a)^k d
by Selfoverlapping OC am2
d a b → b a d
by original rule (OC 1)
d a c → b c c
by original rule (OC 1)

(0) Obligation:

(1) NonTerminationProof (COMPLETE transformation)

(2) NO